Merge remote-tracking branch 'origin/master' into adomani/use_cdots_a…

…gain

Archive/Imo/Imo1972Q5.lean

@@ -53,8 +53,8 @@ theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y
         0 < ‖f x‖ := norm_pos_iff.mpr hx
         _ ≤ k := hk₁ x
     rw [div_lt_iff]
-    apply lt_mul_of_one_lt_right h₁ hneg
-    exact zero_lt_one.trans hneg
+    · apply lt_mul_of_one_lt_right h₁ hneg
+    · exact zero_lt_one.trans hneg
   -- Demonstrate that `k ≤ k'` using `hk₂`.
   have H₂ : k ≤ k' := by
     have h₁ : ∃ x : ℝ, x ∈ S := by use ‖f 0‖; exact Set.mem_range_self 0

Archive/Imo/Imo2008Q2.lean

@@ -103,9 +103,9 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
         set z : ℚ := -t * (t + 1) with hz_def
         simp only [t, W, K, g, Set.mem_image, Prod.exists]
         use x, y, z; constructor
-        simp only [Set.mem_setOf_eq]
-        · use x, y, z; constructor
-          rfl
+        · simp only [Set.mem_setOf_eq]
+          use x, y, z; constructor
+          · rfl
           · use t; constructor
             · simp only [t, gt_iff_lt, lt_max_iff]; right; trivial
             exact ⟨rfl, rfl, rfl⟩

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -85,21 +85,22 @@ theorem monic_Phi : (Φ R a b).Monic :=
 theorem irreducible_Phi (p : ℕ) (hp : p.Prime) (hpa : p ∣ a) (hpb : p ∣ b) (hp2b : ¬p ^ 2 ∣ b) :
     Irreducible (Φ ℚ a b) := by
   rw [← map_Phi a b (Int.castRingHom ℚ), ← IsPrimitive.Int.irreducible_iff_irreducible_map_cast]
-  apply irreducible_of_eisenstein_criterion
-  · rwa [span_singleton_prime (Int.natCast_ne_zero.mpr hp.ne_zero), Int.prime_iff_natAbs_prime]
-  · rw [leadingCoeff_Phi, mem_span_singleton]
-    exact mod_cast mt Nat.dvd_one.mp hp.ne_one
-  · intro n hn
-    rw [mem_span_singleton]
-    rw [degree_Phi] at hn; norm_cast at hn
-    interval_cases hn : n <;>
-    simp (config := {decide := true}) only [Φ, coeff_X_pow, coeff_C, Int.natCast_dvd_natCast.mpr,
-      hpb, if_true, coeff_C_mul, if_false, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero,
-      coeff_sub, add_zero, zero_sub, dvd_neg, neg_zero, dvd_mul_of_dvd_left]
-  · simp only [degree_Phi, ← WithBot.coe_zero, WithBot.coe_lt_coe, Nat.succ_pos']
-    decide
-  · rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton]
-    exact mt Int.natCast_dvd_natCast.mp hp2b
+  on_goal 1 =>
+    apply irreducible_of_eisenstein_criterion
+    · rwa [span_singleton_prime (Int.natCast_ne_zero.mpr hp.ne_zero), Int.prime_iff_natAbs_prime]
+    · rw [leadingCoeff_Phi, mem_span_singleton]
+      exact mod_cast mt Nat.dvd_one.mp hp.ne_one
+    · intro n hn
+      rw [mem_span_singleton]
+      rw [degree_Phi] at hn; norm_cast at hn
+      interval_cases hn : n <;>
+      simp (config := {decide := true}) only [Φ, coeff_X_pow, coeff_C, Int.natCast_dvd_natCast.mpr,
+        hpb, if_true, coeff_C_mul, if_false, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero,
+        coeff_sub, add_zero, zero_sub, dvd_neg, neg_zero, dvd_mul_of_dvd_left]
+    · simp only [degree_Phi, ← WithBot.coe_zero, WithBot.coe_lt_coe, Nat.succ_pos']
+      decide
+    · rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton]
+      exact mt Int.natCast_dvd_natCast.mp hp2b
   all_goals exact Monic.isPrimitive (monic_Phi a b)
 #align abel_ruffini.irreducible_Phi AbelRuffini.irreducible_Phi
 

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -387,8 +387,8 @@ theorem ballot_problem' :
       ring
     all_goals
       refine' (ENNReal.mul_lt_top _ _).ne
-      exact (measure_lt_top _ _).ne
-      simp [Ne, ENNReal.div_eq_top]
+      · exact (measure_lt_top _ _).ne
+      · simp [Ne, ENNReal.div_eq_top]
 #align ballot.ballot_problem' Ballot.ballot_problem'
 
 /-- The ballot problem. -/

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -182,8 +182,8 @@ theorem zero_le_b {i j} : 0 ≤ (cs i).b j :=
 theorem b_add_w_le_one {j} : (cs i).b j + (cs i).w ≤ 1 := by
   have : side (cs i) j ⊆ Ico 0 1 := side_subset h
   rw [side, Ico_subset_Ico_iff] at this
-  convert this.2
-  simp [hw]
+  · convert this.2
+  · simp [hw]
 #align theorems_100.«82».correct.b_add_w_le_one Theorems100.«82».Correct.b_add_w_le_one
 
 theorem nontrivial_fin : Nontrivial (Fin n) :=
@@ -198,11 +198,11 @@ theorem w_ne_one [Nontrivial ι] (i : ι) : (cs i).w ≠ 1 := by
   have hp : p ∈ (cs i').toSet := (cs i').b_mem_toSet
   have h2p : p ∈ (cs i).toSet := by
     intro j; constructor
-    · trans (0 : ℝ)
-      · rw [← add_le_add_iff_right (1 : ℝ)]; convert b_add_w_le_one h
-        · rw [hi]
-        · rw [zero_add]
-      · apply zero_le_b h
+    trans (0 : ℝ)
+    · rw [← add_le_add_iff_right (1 : ℝ)]; convert b_add_w_le_one h
+      · rw [hi]
+      · rw [zero_add]
+    · apply zero_le_b h
     · apply lt_of_lt_of_le (side_subset h <| (cs i').b_mem_side j).2
       simp [hi, zero_le_b h]
   exact (h.PairwiseDisjoint hi').le_bot ⟨hp, h2p⟩
@@ -216,7 +216,9 @@ theorem shiftUp_bottom_subset_bottoms (hc : (cs i).xm ≠ 1) :
   have : p ∈ (unitCube : Cube (n + 1)).toSet := by
     simp only [toSet, forall_fin_succ, hp0, side_unitCube, mem_setOf_eq, mem_Ico, head_shiftUp]
     refine' ⟨⟨_, _⟩, _⟩
-    · rw [← zero_add (0 : ℝ)]; apply add_le_add; apply zero_le_b h; apply (cs i).hw'
+    · rw [← zero_add (0 : ℝ)]; apply add_le_add
+      · apply zero_le_b h
+      · apply (cs i).hw'
     · exact lt_of_le_of_ne (b_add_w_le_one h) hc
     intro j; exact side_subset h (hps j)
   rw [← h.2, mem_iUnion] at this; rcases this with ⟨i', hi'⟩
@@ -225,9 +227,9 @@ theorem shiftUp_bottom_subset_bottoms (hc : (cs i).xm ≠ 1) :
   have := h.1 this
   rw [onFun, comp_apply, comp_apply, toSet_disjoint, exists_fin_succ] at this
   rcases this with (h0 | ⟨j, hj⟩)
-  rw [hp0]; symm; apply eq_of_Ico_disjoint h0 (by simp [hw]) _
-  convert hi' 0; rw [hp0]; rfl
-  exfalso; apply not_disjoint_iff.mpr ⟨tail p j, hps j, hi' j.succ⟩ hj
+  · rw [hp0]; symm; apply eq_of_Ico_disjoint h0 (by simp [hw]) _
+    convert hi' 0; rw [hp0]; rfl
+  · exfalso; apply not_disjoint_iff.mpr ⟨tail p j, hps j, hi' j.succ⟩ hj
 #align theorems_100.«82».correct.shift_up_bottom_subset_bottoms Theorems100.«82».Correct.shiftUp_bottom_subset_bottoms
 
 end Correct
@@ -258,11 +260,15 @@ theorem valley_unitCube [Nontrivial ι] (h : Correct cs) : Valley cs unitCube :=
     intro h0 hv
     have : v ∈ (unitCube : Cube (n + 1)).toSet := by
       dsimp only [toSet, unitCube, mem_setOf_eq]
-      rw [forall_fin_succ, h0]; constructor; norm_num [side, unitCube]; exact hv
+      rw [forall_fin_succ, h0]; constructor
+      · norm_num [side, unitCube]
+      · exact hv
     rw [← h.2, mem_iUnion] at this; rcases this with ⟨i, hi⟩
     use i
     constructor
-    · apply le_antisymm; rw [h0]; exact h.zero_le_b; exact (hi 0).1
+    · apply le_antisymm
+      · rw [h0]; exact h.zero_le_b
+      · exact (hi 0).1
     intro j; exact hi _
   · intro i _ _; rw [toSet_subset]; intro j; convert h.side_subset using 1; simp [side_tail]
   · intro i _; exact h.w_ne_one i
@@ -293,7 +299,8 @@ theorem b_le_b (hi : i ∈ bcubes cs c) (j : Fin n) : c.b j.succ ≤ (cs i).b j.
 theorem t_le_t (hi : i ∈ bcubes cs c) (j : Fin n) :
     (cs i).b j.succ + (cs i).w ≤ c.b j.succ + c.w := by
   have h' := tail_sub hi j; dsimp only [side] at h'; rw [Ico_subset_Ico_iff] at h'
-  exact h'.2; simp [hw]
+  · exact h'.2
+  · simp [hw]
 #align theorems_100.«82».t_le_t Theorems100.«82».t_le_t
 
 /-- Every cube in the valley must be smaller than it -/
@@ -365,9 +372,11 @@ theorem mi_strict_minimal (hii' : mi h v ≠ i) (hi : i ∈ bcubes cs c) :
 /-- The top of `mi` cannot be 1, since there is a larger cube in the valley -/
 theorem mi_xm_ne_one : (cs <| mi h v).xm ≠ 1 := by
   apply ne_of_lt; rcases (nontrivial_bcubes h v).exists_ne (mi h v) with ⟨i, hi, h2i⟩
-  apply lt_of_lt_of_le _ h.b_add_w_le_one; exact i; exact 0
-  rw [xm, mi_mem_bcubes.1, hi.1, _root_.add_lt_add_iff_left]
-  exact mi_strict_minimal h2i.symm hi
+  · apply lt_of_lt_of_le _ h.b_add_w_le_one
+    · exact i
+    · exact 0
+    rw [xm, mi_mem_bcubes.1, hi.1, _root_.add_lt_add_iff_left]
+    exact mi_strict_minimal h2i.symm hi
 #align theorems_100.«82».mi_xm_ne_one Theorems100.«82».mi_xm_ne_one
 
 /-- If `mi` lies on the boundary of the valley in dimension j, then this lemma expresses that all
@@ -385,8 +394,8 @@ theorem smallest_onBoundary {j} (bi : OnBoundary (mi_mem_bcubes : mi h v ∈ _)
     · simp [side, bi, hw', w_lt_w h v hi]
     · intro h'; simpa [lt_irrefl] using h'.2
     intro i' hi' i'_i h2i'; constructor
-    apply le_trans h2i'.1
-    · simp [hw']
+    · apply le_trans h2i'.1
+      simp [hw']
     apply lt_of_lt_of_le (add_lt_add_left (mi_strict_minimal i'_i.symm hi') _)
     simp [bi.symm, b_le_b hi']
   let s := bcubes cs c \ {i}
@@ -404,7 +413,7 @@ theorem smallest_onBoundary {j} (bi : OnBoundary (mi_mem_bcubes : mi h v ∈ _)
     rw [add_assoc, le_add_iff_nonneg_right, ← sub_eq_add_neg, sub_nonneg]
     apply le_of_lt (w_lt_w h v hi')
   · simp only [side, not_and_or, not_lt, not_le, mem_Ico]; left; exact hx
-  intro i'' hi'' h2i'' h3i''; constructor; swap; apply lt_trans hx h3i''.2
+  intro i'' hi'' h2i'' h3i''; constructor; swap; · apply lt_trans hx h3i''.2
   rw [le_sub_iff_add_le]
   refine' le_trans _ (t_le_t hi'' j); rw [add_le_add_iff_left]; apply h3i' i'' ⟨hi'', _⟩
   simp [mem_singleton, h2i'']
@@ -432,14 +441,16 @@ theorem mi_not_onBoundary (j : Fin n) : ¬OnBoundary (mi_mem_bcubes : mi h v ∈
   have h2i' : i' ∈ bcubes cs c := ⟨hi'.1.symm, v.2.1 i' hi'.1.symm ⟨tail p, hi'.2, hp.2⟩⟩
   have i_i' : i ≠ i' := by rintro rfl; simpa [p, side_tail, h2x] using hi'.2 j
   have : Nonempty (↥((cs i').tail.side j' \ (cs i).tail.side j')) := by
-    apply nonempty_Ico_sdiff; apply mi_strict_minimal i_i' h2i'; apply hw
+    apply nonempty_Ico_sdiff
+    · apply mi_strict_minimal i_i' h2i'
+    · apply hw
   rcases this with ⟨⟨x', hx'⟩⟩
   let p' : Fin (n + 1) → ℝ := cons (c.b 0) fun j₂ => if j₂ = j' then x' else (cs i).b j₂.succ
   have hp' : p' ∈ c.bottom := by
     suffices ∀ j : Fin n, ite (j = j') x' ((cs i).b j.succ) ∈ c.side j.succ by
       simpa [p', bottom, toSet, tail, side_tail]
     intro j₂
-    by_cases hj₂ : j₂ = j'; simp [hj₂]; apply tail_sub h2i'; apply hx'.1
+    by_cases hj₂ : j₂ = j'; · simp [hj₂]; apply tail_sub h2i'; apply hx'.1
     simp only [if_congr, if_false, hj₂]; apply tail_sub hi; apply b_mem_side
   rcases v.1 hp' with ⟨_, ⟨i'', rfl⟩, hi''⟩
   have h2i'' : i'' ∈ bcubes cs c := ⟨hi''.1.symm, v.2.1 i'' hi''.1.symm ⟨tail p', hi''.2, hp'.2⟩⟩
@@ -477,7 +488,7 @@ theorem mi_not_onBoundary' (j : Fin n) :
   have := mi_not_onBoundary h v j
   simp only [OnBoundary, not_or] at this; cases' this with h1 h2
   constructor
-  apply lt_of_le_of_ne (b_le_b mi_mem_bcubes _) h1
+  · apply lt_of_le_of_ne (b_le_b mi_mem_bcubes _) h1
   apply lt_of_le_of_ne _ h2
   apply ((Ico_subset_Ico_iff _).mp (tail_sub mi_mem_bcubes j)).2
   simp [hw]
@@ -515,7 +526,9 @@ theorem valley_mi : Valley cs (cs (mi h v)).shiftUp := by
     rcases v.1 hp with ⟨_, ⟨i'', rfl⟩, hi''⟩
     have h2i'' : i'' ∈ bcubes cs c := by
       use hi''.1.symm; apply v.2.1 i'' hi''.1.symm
-      use tail p; constructor; exact hi''.2; rw [tail_cons]; exact h3p3
+      use tail p; constructor
+      · exact hi''.2
+      · rw [tail_cons]; exact h3p3
     have h3i'' : (cs i).w < (cs i'').w := by
       apply mi_strict_minimal _ h2i''; rintro rfl; apply h2p3; convert hi''.2
     let p' := @cons n (fun _ => ℝ) (cs i).xm p3

Archive/Wiedijk100Theorems/Partition.lean

@@ -215,7 +215,7 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ)
       exact fun hi _ => ha.2 i hi
     · conv_rhs => simp [← a.parts_sum]
       rw [sum_multiset_count_of_subset _ s]
-      simp only [smul_eq_mul]
+      · simp only [smul_eq_mul]
       · intro i
         simp only [Multiset.mem_toFinset, not_not, mem_filter]
         apply ha.2
@@ -229,8 +229,8 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ)
     by_cases hi : i = 0
     · rw [hi]
       rw [Multiset.count_eq_zero_of_not_mem]
-      rw [Multiset.count_eq_zero_of_not_mem]
-      intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₂.2 0 a))
+      · rw [Multiset.count_eq_zero_of_not_mem]
+        intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₂.2 0 a))
       intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₁.2 0 a))
     · rw [← mul_left_inj' hi]
       rw [Function.funext_iff] at h

Archive/Wiedijk100Theorems/SolutionOfCubic.lean

@@ -137,7 +137,7 @@ theorem cubic_eq_zero_iff_of_p_eq_zero (ha : a ≠ 0) (hω : IsPrimitiveRoot ω
       a * (x + b / (3 * a)) ^ 3 + (c - b ^ 2 / (3 * a)) * x + (d - b ^ 3 * a / (3 * a) ^ 3) := by
         field_simp; ring
       _ = a * (x + b / (3 * a)) ^ 3 + (d - (9 * a * b * c - 2 * b ^ 3) * a / (3 * a) ^ 3) := by
-        simp only [hb2, hb3]; field_simp; ring
+        simp only [hb2, hb3]; field_simp [ha]; ring
       _ = a * ((x + b / (3 * a)) ^ 3 - s ^ 3) := by rw [hs3, hq]; field_simp [h54]; ring
   have h₃ : ∀ x, a * x = 0 ↔ x = 0 := by intro x; simp [ha]
   have h₄ : ∀ x : K, x ^ 3 - s ^ 3 = (x - s) * (x - s * ω) * (x - s * ω ^ 2) := by

Counterexamples/Cyclotomic105.lean

@@ -70,7 +70,7 @@ theorem cyclotomic_15 : cyclotomic 15 ℤ = 1 - X + X ^ 3 - X ^ 4 + X ^ 5 - X ^
   refine' ((eq_cyclotomic_iff (by norm_num) _).2 _).symm
   rw [properDivisors_15, Finset.prod_insert _, Finset.prod_insert _, Finset.prod_singleton,
     cyclotomic_one, cyclotomic_3, cyclotomic_5]
-  ring
+  · ring
   repeat' norm_num
 #align counterexample.cyclotomic_15 Counterexample.cyclotomic_15
 
@@ -79,7 +79,7 @@ theorem cyclotomic_21 :
   refine' ((eq_cyclotomic_iff (by norm_num) _).2 _).symm
   rw [properDivisors_21, Finset.prod_insert _, Finset.prod_insert _, Finset.prod_singleton,
     cyclotomic_one, cyclotomic_3, cyclotomic_7]
-  ring
+  · ring
   repeat' norm_num
 #align counterexample.cyclotomic_21 Counterexample.cyclotomic_21
 
@@ -90,7 +90,7 @@ theorem cyclotomic_35 :
   refine' ((eq_cyclotomic_iff (by norm_num) _).2 _).symm
   rw [properDivisors_35, Finset.prod_insert _, Finset.prod_insert _, Finset.prod_singleton,
     cyclotomic_one, cyclotomic_5, cyclotomic_7]
-  ring
+  · ring
   repeat' norm_num
 #align counterexample.cyclotomic_35 Counterexample.cyclotomic_35
 
@@ -102,10 +102,10 @@ theorem cyclotomic_105 :
         X ^ 46 + X ^ 47 + X ^ 48 := by
   refine' ((eq_cyclotomic_iff (by norm_num) _).2 _).symm
   rw [properDivisors_105]
-  repeat' rw [Finset.prod_insert (α := ℕ) (β := ℤ[X])]
-  rw [Finset.prod_singleton, cyclotomic_one, cyclotomic_3, cyclotomic_5, cyclotomic_7,
-    cyclotomic_15, cyclotomic_21, cyclotomic_35]
-  ring
+  repeat rw [Finset.prod_insert (α := ℕ) (β := ℤ[X])]
+  · rw [Finset.prod_singleton, cyclotomic_one, cyclotomic_3, cyclotomic_5, cyclotomic_7,
+      cyclotomic_15, cyclotomic_21, cyclotomic_35]
+    ring
   repeat' norm_num
 #align counterexample.cyclotomic_105 Counterexample.cyclotomic_105
 

Counterexamples/DirectSumIsInternal.lean

@@ -60,8 +60,8 @@ theorem withSign.isCompl : IsCompl ℤ≥0 ℤ≤0 := by
   · rw [codisjoint_iff_le_sup]
     intro x _hx
     obtain hp | hn := (le_refl (0 : ℤ)).le_or_le x
-    exact Submodule.mem_sup_left (mem_withSign_one.mpr hp)
-    exact Submodule.mem_sup_right (mem_withSign_neg_one.mpr hn)
+    · exact Submodule.mem_sup_left (mem_withSign_one.mpr hp)
+    · exact Submodule.mem_sup_right (mem_withSign_neg_one.mpr hn)
 #align counterexample.with_sign.is_compl Counterexample.withSign.isCompl
 
 def withSign.independent : CompleteLattice.Independent withSign := by