Skip to content

Commit 72f529a

Browse files
adomaniadomani
committed
another batch of cdot usage
1 parent 54ea495 commit 72f529a

50 files changed

Lines changed: 225 additions & 221 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Archive/Imo/Imo1972Q5.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -53,8 +53,8 @@ theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y
5353
0 < ‖f x‖ := norm_pos_iff.mpr hx
5454
_ ≤ k := hk₁ x
5555
rw [div_lt_iff]
56-
apply lt_mul_of_one_lt_right h₁ hneg
57-
exact zero_lt_one.trans hneg
56+
· apply lt_mul_of_one_lt_right h₁ hneg
57+
· exact zero_lt_one.trans hneg
5858
-- Demonstrate that `k ≤ k'` using `hk₂`.
5959
have H₂ : k ≤ k' := by
6060
have h₁ : ∃ x : ℝ, x ∈ S := by use ‖f 0‖; exact Set.mem_range_self 0

‎Archive/Imo/Imo2008Q2.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -103,9 +103,9 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
103103
set z : ℚ := -t * (t + 1) with hz_def
104104
simp only [t, W, K, g, Set.mem_image, Prod.exists]
105105
use x, y, z; constructor
106-
simp only [Set.mem_setOf_eq]
107-
· use x, y, z; constructor
108-
rfl
106+
· simp only [Set.mem_setOf_eq]
107+
use x, y, z; constructor
108+
· rfl
109109
· use t; constructor
110110
· simp only [t, gt_iff_lt, lt_max_iff]; right; trivial
111111
exact ⟨rfl, rfl, rfl⟩

‎Archive/Wiedijk100Theorems/AbelRuffini.lean‎

Lines changed: 16 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -85,21 +85,22 @@ theorem monic_Phi : (Φ R a b).Monic :=
8585
theorem irreducible_Phi (p : ℕ) (hp : p.Prime) (hpa : p ∣ a) (hpb : p ∣ b) (hp2b : ¬p ^ 2 ∣ b) :
8686
Irreducible (Φ ℚ a b) := by
8787
rw [← map_Phi a b (Int.castRingHom ℚ), ← IsPrimitive.Int.irreducible_iff_irreducible_map_cast]
88-
apply irreducible_of_eisenstein_criterion
89-
· rwa [span_singleton_prime (Int.natCast_ne_zero.mpr hp.ne_zero), Int.prime_iff_natAbs_prime]
90-
· rw [leadingCoeff_Phi, mem_span_singleton]
91-
exact mod_cast mt Nat.dvd_one.mp hp.ne_one
92-
· intro n hn
93-
rw [mem_span_singleton]
94-
rw [degree_Phi] at hn; norm_cast at hn
95-
interval_cases hn : n <;>
96-
simp (config := {decide := true}) only [Φ, coeff_X_pow, coeff_C, Int.natCast_dvd_natCast.mpr,
97-
hpb, if_true, coeff_C_mul, if_false, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero,
98-
coeff_sub, add_zero, zero_sub, dvd_neg, neg_zero, dvd_mul_of_dvd_left]
99-
· simp only [degree_Phi, ← WithBot.coe_zero, WithBot.coe_lt_coe, Nat.succ_pos']
100-
decide
101-
· rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton]
102-
exact mt Int.natCast_dvd_natCast.mp hp2b
88+
on_goal 1 =>
89+
apply irreducible_of_eisenstein_criterion
90+
· rwa [span_singleton_prime (Int.natCast_ne_zero.mpr hp.ne_zero), Int.prime_iff_natAbs_prime]
91+
· rw [leadingCoeff_Phi, mem_span_singleton]
92+
exact mod_cast mt Nat.dvd_one.mp hp.ne_one
93+
· intro n hn
94+
rw [mem_span_singleton]
95+
rw [degree_Phi] at hn; norm_cast at hn
96+
interval_cases hn : n <;>
97+
simp (config := {decide := true}) only [Φ, coeff_X_pow, coeff_C, Int.natCast_dvd_natCast.mpr,
98+
hpb, if_true, coeff_C_mul, if_false, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero,
99+
coeff_sub, add_zero, zero_sub, dvd_neg, neg_zero, dvd_mul_of_dvd_left]
100+
· simp only [degree_Phi, ← WithBot.coe_zero, WithBot.coe_lt_coe, Nat.succ_pos']
101+
decide
102+
· rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton]
103+
exact mt Int.natCast_dvd_natCast.mp hp2b
103104
all_goals exact Monic.isPrimitive (monic_Phi a b)
104105
#align abel_ruffini.irreducible_Phi AbelRuffini.irreducible_Phi
105106

‎Archive/Wiedijk100Theorems/BallotProblem.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -387,8 +387,8 @@ theorem ballot_problem' :
387387
ring
388388
all_goals
389389
refine' (ENNReal.mul_lt_top _ _).ne
390-
exact (measure_lt_top _ _).ne
391-
simp [Ne, ENNReal.div_eq_top]
390+
· exact (measure_lt_top _ _).ne
391+
· simp [Ne, ENNReal.div_eq_top]
392392
#align ballot.ballot_problem' Ballot.ballot_problem'
393393

394394
/-- The ballot problem. -/

‎Archive/Wiedijk100Theorems/CubingACube.lean‎

Lines changed: 26 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -182,8 +182,8 @@ theorem zero_le_b {i j} : 0 ≤ (cs i).b j :=
182182
theorem b_add_w_le_one {j} : (cs i).b j + (cs i).w ≤ 1 := by
183183
have : side (cs i) j ⊆ Ico 0 1 := side_subset h
184184
rw [side, Ico_subset_Ico_iff] at this
185-
convert this.2
186-
simp [hw]
185+
· convert this.2
186+
· simp [hw]
187187
#align theorems_100.«82».correct.b_add_w_le_one Theorems100.«82».Correct.b_add_w_le_one
188188

189189
theorem nontrivial_fin : Nontrivial (Fin n) :=
@@ -199,9 +199,10 @@ theorem w_ne_one [Nontrivial ι] (i : ι) : (cs i).w ≠ 1 := by
199199
have h2p : p ∈ (cs i).toSet := by
200200
intro j; constructor
201201
trans (0 : ℝ)
202-
· rw [← add_le_add_iff_right (1 : ℝ)]; convert b_add_w_le_one h; rw [hi]; rw [zero_add]
203-
apply zero_le_b h; apply lt_of_lt_of_le (side_subset h <| (cs i').b_mem_side j).2
204-
simp [hi, zero_le_b h]
202+
· rw [← add_le_add_iff_right (1 : ℝ)]; convert b_add_w_le_one h; (· rw [hi]); rw [zero_add]
203+
· apply zero_le_b h
204+
· apply lt_of_lt_of_le (side_subset h <| (cs i').b_mem_side j).2
205+
simp [hi, zero_le_b h]
205206
exact (h.PairwiseDisjoint hi').le_bot ⟨hp, h2p⟩
206207
#align theorems_100.«82».correct.w_ne_one Theorems100.«82».Correct.w_ne_one
207208

@@ -213,7 +214,7 @@ theorem shiftUp_bottom_subset_bottoms (hc : (cs i).xm ≠ 1) :
213214
have : p ∈ (unitCube : Cube (n + 1)).toSet := by
214215
simp only [toSet, forall_fin_succ, hp0, side_unitCube, mem_setOf_eq, mem_Ico, head_shiftUp]
215216
refine' ⟨⟨_, _⟩, _⟩
216-
· rw [← zero_add (0 : ℝ)]; apply add_le_add; apply zero_le_b h; apply (cs i).hw'
217+
· rw [← zero_add (0 : ℝ)]; apply add_le_add; (· apply zero_le_b h); apply (cs i).hw'
217218
· exact lt_of_le_of_ne (b_add_w_le_one h) hc
218219
intro j; exact side_subset h (hps j)
219220
rw [← h.2, mem_iUnion] at this; rcases this with ⟨i', hi'⟩
@@ -222,9 +223,9 @@ theorem shiftUp_bottom_subset_bottoms (hc : (cs i).xm ≠ 1) :
222223
have := h.1 this
223224
rw [onFun, comp_apply, comp_apply, toSet_disjoint, exists_fin_succ] at this
224225
rcases this with (h0 | ⟨j, hj⟩)
225-
rw [hp0]; symm; apply eq_of_Ico_disjoint h0 (by simp [hw]) _
226-
convert hi' 0; rw [hp0]; rfl
227-
exfalso; apply not_disjoint_iff.mpr ⟨tail p j, hps j, hi' j.succ⟩ hj
226+
· rw [hp0]; symm; apply eq_of_Ico_disjoint h0 (by simp [hw]) _
227+
convert hi' 0; rw [hp0]; rfl
228+
· exfalso; apply not_disjoint_iff.mpr ⟨tail p j, hps j, hi' j.succ⟩ hj
228229
#align theorems_100.«82».correct.shift_up_bottom_subset_bottoms Theorems100.«82».Correct.shiftUp_bottom_subset_bottoms
229230

230231
end Correct
@@ -255,11 +256,11 @@ theorem valley_unitCube [Nontrivial ι] (h : Correct cs) : Valley cs unitCube :=
255256
intro h0 hv
256257
have : v ∈ (unitCube : Cube (n + 1)).toSet := by
257258
dsimp only [toSet, unitCube, mem_setOf_eq]
258-
rw [forall_fin_succ, h0]; constructor; norm_num [side, unitCube]; exact hv
259+
rw [forall_fin_succ, h0]; constructor; (· norm_num [side, unitCube]); exact hv
259260
rw [← h.2, mem_iUnion] at this; rcases this with ⟨i, hi⟩
260261
use i
261262
constructor
262-
· apply le_antisymm; rw [h0]; exact h.zero_le_b; exact (hi 0).1
263+
· apply le_antisymm; (· rw [h0]; exact h.zero_le_b); exact (hi 0).1
263264
intro j; exact hi _
264265
· intro i _ _; rw [toSet_subset]; intro j; convert h.side_subset using 1; simp [side_tail]
265266
· intro i _; exact h.w_ne_one i
@@ -290,7 +291,7 @@ theorem b_le_b (hi : i ∈ bcubes cs c) (j : Fin n) : c.b j.succ ≤ (cs i).b j.
290291
theorem t_le_t (hi : i ∈ bcubes cs c) (j : Fin n) :
291292
(cs i).b j.succ + (cs i).w ≤ c.b j.succ + c.w := by
292293
have h' := tail_sub hi j; dsimp only [side] at h'; rw [Ico_subset_Ico_iff] at h'
293-
exact h'.2; simp [hw]
294+
(· exact h'.2); simp [hw]
294295
#align theorems_100.«82».t_le_t Theorems100.«82».t_le_t
295296

296297
/-- Every cube in the valley must be smaller than it -/
@@ -362,9 +363,9 @@ theorem mi_strict_minimal (hii' : mi h v ≠ i) (hi : i ∈ bcubes cs c) :
362363
/-- The top of `mi` cannot be 1, since there is a larger cube in the valley -/
363364
theorem mi_xm_ne_one : (cs <| mi h v).xm ≠ 1 := by
364365
apply ne_of_lt; rcases (nontrivial_bcubes h v).exists_ne (mi h v) with ⟨i, hi, h2i⟩
365-
apply lt_of_lt_of_le _ h.b_add_w_le_one; exact i; exact 0
366-
rw [xm, mi_mem_bcubes.1, hi.1, _root_.add_lt_add_iff_left]
367-
exact mi_strict_minimal h2i.symm hi
366+
· apply lt_of_lt_of_le _ h.b_add_w_le_one; (· exact i); (· exact 0)
367+
rw [xm, mi_mem_bcubes.1, hi.1, _root_.add_lt_add_iff_left]
368+
exact mi_strict_minimal h2i.symm hi
368369
#align theorems_100.«82».mi_xm_ne_one Theorems100.«82».mi_xm_ne_one
369370

370371
/-- If `mi` lies on the boundary of the valley in dimension j, then this lemma expresses that all
@@ -382,8 +383,8 @@ theorem smallest_onBoundary {j} (bi : OnBoundary (mi_mem_bcubes : mi h v ∈ _)
382383
· simp [side, bi, hw', w_lt_w h v hi]
383384
· intro h'; simpa [lt_irrefl] using h'.2
384385
intro i' hi' i'_i h2i'; constructor
385-
apply le_trans h2i'.1
386-
· simp [hw']
386+
· apply le_trans h2i'.1
387+
simp [hw']
387388
apply lt_of_lt_of_le (add_lt_add_left (mi_strict_minimal i'_i.symm hi') _)
388389
simp [bi.symm, b_le_b hi']
389390
let s := bcubes cs c \ {i}
@@ -401,7 +402,7 @@ theorem smallest_onBoundary {j} (bi : OnBoundary (mi_mem_bcubes : mi h v ∈ _)
401402
rw [add_assoc, le_add_iff_nonneg_right, ← sub_eq_add_neg, sub_nonneg]
402403
apply le_of_lt (w_lt_w h v hi')
403404
· simp only [side, not_and_or, not_lt, not_le, mem_Ico]; left; exact hx
404-
intro i'' hi'' h2i'' h3i''; constructor; swap; apply lt_trans hx h3i''.2
405+
intro i'' hi'' h2i'' h3i''; constructor; swap; · apply lt_trans hx h3i''.2
405406
rw [le_sub_iff_add_le]
406407
refine' le_trans _ (t_le_t hi'' j); rw [add_le_add_iff_left]; apply h3i' i'' ⟨hi'', _⟩
407408
simp [mem_singleton, h2i'']
@@ -429,14 +430,14 @@ theorem mi_not_onBoundary (j : Fin n) : ¬OnBoundary (mi_mem_bcubes : mi h v ∈
429430
have h2i' : i' ∈ bcubes cs c := ⟨hi'.1.symm, v.2.1 i' hi'.1.symm ⟨tail p, hi'.2, hp.2⟩⟩
430431
have i_i' : i ≠ i' := by rintro rfl; simpa [p, side_tail, h2x] using hi'.2 j
431432
have : Nonempty (↥((cs i').tail.side j' \ (cs i).tail.side j')) := by
432-
apply nonempty_Ico_sdiff; apply mi_strict_minimal i_i' h2i'; apply hw
433+
apply nonempty_Ico_sdiff; (· apply mi_strict_minimal i_i' h2i'); apply hw
433434
rcases this with ⟨⟨x', hx'⟩⟩
434435
let p' : Fin (n + 1) → ℝ := cons (c.b 0) fun j₂ => if j₂ = j' then x' else (cs i).b j₂.succ
435436
have hp' : p' ∈ c.bottom := by
436437
suffices ∀ j : Fin n, ite (j = j') x' ((cs i).b j.succ) ∈ c.side j.succ by
437438
simpa [p', bottom, toSet, tail, side_tail]
438439
intro j₂
439-
by_cases hj₂ : j₂ = j'; simp [hj₂]; apply tail_sub h2i'; apply hx'.1
440+
by_cases hj₂ : j₂ = j'; · simp [hj₂]; apply tail_sub h2i'; apply hx'.1
440441
simp only [if_congr, if_false, hj₂]; apply tail_sub hi; apply b_mem_side
441442
rcases v.1 hp' with ⟨_, ⟨i'', rfl⟩, hi''⟩
442443
have h2i'' : i'' ∈ bcubes cs c := ⟨hi''.1.symm, v.2.1 i'' hi''.1.symm ⟨tail p', hi''.2, hp'.2⟩⟩
@@ -474,10 +475,10 @@ theorem mi_not_onBoundary' (j : Fin n) :
474475
have := mi_not_onBoundary h v j
475476
simp only [OnBoundary, not_or] at this; cases' this with h1 h2
476477
constructor
477-
apply lt_of_le_of_ne (b_le_b mi_mem_bcubes _) h1
478-
apply lt_of_le_of_ne _ h2
479-
apply ((Ico_subset_Ico_iff _).mp (tail_sub mi_mem_bcubes j)).2
480-
simp [hw]
478+
· apply lt_of_le_of_ne (b_le_b mi_mem_bcubes _) h1
479+
· apply lt_of_le_of_ne _ h2
480+
apply ((Ico_subset_Ico_iff _).mp (tail_sub mi_mem_bcubes j)).2
481+
simp [hw]
481482
#align theorems_100.«82».mi_not_on_boundary' Theorems100.«82».mi_not_onBoundary'
482483

483484
/-- The top of `mi` gives rise to a new valley, since the neighbouring cubes extend further upward
@@ -512,7 +513,7 @@ theorem valley_mi : Valley cs (cs (mi h v)).shiftUp := by
512513
rcases v.1 hp with ⟨_, ⟨i'', rfl⟩, hi''⟩
513514
have h2i'' : i'' ∈ bcubes cs c := by
514515
use hi''.1.symm; apply v.2.1 i'' hi''.1.symm
515-
use tail p; constructor; exact hi''.2; rw [tail_cons]; exact h3p3
516+
use tail p; constructor; (· exact hi''.2); rw [tail_cons]; exact h3p3
516517
have h3i'' : (cs i).w < (cs i'').w := by
517518
apply mi_strict_minimal _ h2i''; rintro rfl; apply h2p3; convert hi''.2
518519
let p' := @cons n (fun _ => ℝ) (cs i).xm p3

‎Archive/Wiedijk100Theorems/Partition.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -215,7 +215,7 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ)
215215
exact fun hi _ => ha.2 i hi
216216
· conv_rhs => simp [← a.parts_sum]
217217
rw [sum_multiset_count_of_subset _ s]
218-
simp only [smul_eq_mul]
218+
· simp only [smul_eq_mul]
219219
· intro i
220220
simp only [Multiset.mem_toFinset, not_not, mem_filter]
221221
apply ha.2
@@ -229,8 +229,8 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ)
229229
by_cases hi : i = 0
230230
· rw [hi]
231231
rw [Multiset.count_eq_zero_of_not_mem]
232-
rw [Multiset.count_eq_zero_of_not_mem]
233-
intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₂.2 0 a))
232+
· rw [Multiset.count_eq_zero_of_not_mem]
233+
intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₂.2 0 a))
234234
intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₁.2 0 a))
235235
· rw [← mul_left_inj' hi]
236236
rw [Function.funext_iff] at h

‎Counterexamples/Cyclotomic105.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ theorem cyclotomic_15 : cyclotomic 15 ℤ = 1 - X + X ^ 3 - X ^ 4 + X ^ 5 - X ^
7070
refine' ((eq_cyclotomic_iff (by norm_num) _).2 _).symm
7171
rw [properDivisors_15, Finset.prod_insert _, Finset.prod_insert _, Finset.prod_singleton,
7272
cyclotomic_one, cyclotomic_3, cyclotomic_5]
73-
ring
73+
· ring
7474
repeat' norm_num
7575
#align counterexample.cyclotomic_15 Counterexample.cyclotomic_15
7676

@@ -79,7 +79,7 @@ theorem cyclotomic_21 :
7979
refine' ((eq_cyclotomic_iff (by norm_num) _).2 _).symm
8080
rw [properDivisors_21, Finset.prod_insert _, Finset.prod_insert _, Finset.prod_singleton,
8181
cyclotomic_one, cyclotomic_3, cyclotomic_7]
82-
ring
82+
· ring
8383
repeat' norm_num
8484
#align counterexample.cyclotomic_21 Counterexample.cyclotomic_21
8585

@@ -90,7 +90,7 @@ theorem cyclotomic_35 :
9090
refine' ((eq_cyclotomic_iff (by norm_num) _).2 _).symm
9191
rw [properDivisors_35, Finset.prod_insert _, Finset.prod_insert _, Finset.prod_singleton,
9292
cyclotomic_one, cyclotomic_5, cyclotomic_7]
93-
ring
93+
· ring
9494
repeat' norm_num
9595
#align counterexample.cyclotomic_35 Counterexample.cyclotomic_35
9696

@@ -102,10 +102,10 @@ theorem cyclotomic_105 :
102102
X ^ 46 + X ^ 47 + X ^ 48 := by
103103
refine' ((eq_cyclotomic_iff (by norm_num) _).2 _).symm
104104
rw [properDivisors_105]
105-
repeat' rw [Finset.prod_insert (α := ℕ) (β := ℤ[X])]
106-
rw [Finset.prod_singleton, cyclotomic_one, cyclotomic_3, cyclotomic_5, cyclotomic_7,
107-
cyclotomic_15, cyclotomic_21, cyclotomic_35]
108-
ring
105+
repeat rw [Finset.prod_insert (α := ℕ) (β := ℤ[X])]
106+
· rw [Finset.prod_singleton, cyclotomic_one, cyclotomic_3, cyclotomic_5, cyclotomic_7,
107+
cyclotomic_15, cyclotomic_21, cyclotomic_35]
108+
ring
109109
repeat' norm_num
110110
#align counterexample.cyclotomic_105 Counterexample.cyclotomic_105
111111

‎Counterexamples/DirectSumIsInternal.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -60,8 +60,8 @@ theorem withSign.isCompl : IsCompl ℤ≥0 ℤ≤0 := by
6060
· rw [codisjoint_iff_le_sup]
6161
intro x _hx
6262
obtain hp | hn := (le_refl (0 : ℤ)).le_or_le x
63-
exact Submodule.mem_sup_left (mem_withSign_one.mpr hp)
64-
exact Submodule.mem_sup_right (mem_withSign_neg_one.mpr hn)
63+
· exact Submodule.mem_sup_left (mem_withSign_one.mpr hp)
64+
· exact Submodule.mem_sup_right (mem_withSign_neg_one.mpr hn)
6565
#align counterexample.with_sign.is_compl Counterexample.withSign.isCompl
6666

6767
def withSign.independent : CompleteLattice.Independent withSign := by

‎Mathlib/Algebra/Category/Ring/Constructions.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -42,13 +42,13 @@ def pushoutCocone : Limits.PushoutCocone f g := by
4242
letI := RingHom.toAlgebra f
4343
letI := RingHom.toAlgebra g
4444
fapply Limits.PushoutCocone.mk
45-
show CommRingCat; exact CommRingCat.of (A ⊗[R] B)
46-
show A ⟶ _; exact Algebra.TensorProduct.includeLeftRingHom
47-
show B ⟶ _; exact Algebra.TensorProduct.includeRight.toRingHom
48-
ext r
49-
trans algebraMap R (A ⊗[R] B) r
50-
· exact Algebra.TensorProduct.includeLeft.commutes (R := R) r
51-
· exact (Algebra.TensorProduct.includeRight.commutes (R := R) r).symm
45+
· show CommRingCat; exact CommRingCat.of (A ⊗[R] B)
46+
· show A ⟶ _; exact Algebra.TensorProduct.includeLeftRingHom
47+
· show B ⟶ _; exact Algebra.TensorProduct.includeRight.toRingHom
48+
· ext r
49+
trans algebraMap R (A ⊗[R] B) r
50+
· exact Algebra.TensorProduct.includeLeft.commutes (R := R) r
51+
· exact (Algebra.TensorProduct.includeRight.commutes (R := R) r).symm
5252
set_option linter.uppercaseLean3 false in
5353
#align CommRing.pushout_cocone CommRingCat.pushoutCocone
5454

‎Mathlib/Algebra/Lie/DirectSum.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -166,16 +166,16 @@ def lieAlgebraOf [DecidableEq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i :=
166166
-- with `simp [of, singleAddHom]`
167167
simp only [of, singleAddHom, bracket_apply]
168168
erw [AddHom.coe_mk, single_apply, single_apply]
169-
simp? [h] says simp only [h, ↓reduceDite, single_apply]
170-
intros
171-
erw [single_add]
169+
· simp? [h] says simp only [h, ↓reduceDite, single_apply]
170+
· intros
171+
erw [single_add]
172172
· -- This used to be the end of the proof before leanprover/lean4#2644
173173
-- with `simp [of, singleAddHom]`
174174
simp only [of, singleAddHom, bracket_apply]
175175
erw [AddHom.coe_mk, single_apply, single_apply]
176-
simp only [h, dite_false, single_apply, lie_self]
177-
intros
178-
erw [single_add] }
176+
· simp only [h, dite_false, single_apply, lie_self]
177+
· intros
178+
erw [single_add] }
179179
#align direct_sum.lie_algebra_of DirectSum.lieAlgebraOf
180180

181181
/-- The projection map onto one component, as a morphism of Lie algebras. -/

0 commit comments

Comments
 (0)