chore: adapt to multiple goal linter 1 (#12338)

A PR accompanying #12339.

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20against.20.22multi-goal.20proofs.22)

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) :=
@@ -199,9 +199,12 @@ theorem w_ne_one [Nontrivial ι] (i : ι) : (cs i).w ≠ 1 := by
   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; apply lt_of_lt_of_le (side_subset h <| (cs i').b_mem_side j).2
-    simp [hi, zero_le_b h]
+    · 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⟩
 #align theorems_100.«82».correct.w_ne_one Theorems100.«82».Correct.w_ne_one
 
@@ -213,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'⟩
@@ -222,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
@@ -255,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
@@ -290,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 -/
@@ -362,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
@@ -382,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}
@@ -401,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'']
@@ -429,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⟩⟩
@@ -474,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]
@@ -512,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

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

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -1033,9 +1033,9 @@ theorem finprod_subtype_eq_finprod_cond (p : α → Prop) :
 theorem finprod_mem_inter_mul_diff' (t : Set α) (h : (s ∩ mulSupport f).Finite) :
     ((∏ᶠ i ∈ s ∩ t, f i) * ∏ᶠ i ∈ s \ t, f i) = ∏ᶠ i ∈ s, f i := by
   rw [← finprod_mem_union', inter_union_diff]
-  rw [disjoint_iff_inf_le]
-  exacts [fun x hx => hx.2.2 hx.1.2, h.subset fun x hx => ⟨hx.1.1, hx.2⟩,
-    h.subset fun x hx => ⟨hx.1.1, hx.2⟩]
+  · rw [disjoint_iff_inf_le]
+    exact fun x hx => hx.2.2 hx.1.2
+  exacts [h.subset fun x hx => ⟨hx.1.1, hx.2⟩, h.subset fun x hx => ⟨hx.1.1, hx.2⟩]
 #align finprod_mem_inter_mul_diff' finprod_mem_inter_mul_diff'
 #align finsum_mem_inter_add_diff' finsum_mem_inter_add_diff'
 

Mathlib/Algebra/BigOperators/List/Basic.lean

@@ -106,7 +106,8 @@ theorem prod_cons : (a :: l).prod = a * l.prod :=
 lemma prod_induction
     (p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ l, p x) :
     p l.prod := by
-  induction' l with a l ih; simpa
+  induction' l with a l ih
+  · simpa
   rw [List.prod_cons]
   simp only [Bool.not_eq_true, List.mem_cons, forall_eq_or_imp] at base
   exact hom _ _ (base.1) (ih base.2)

Mathlib/Algebra/Category/Ring/Constructions.lean

@@ -42,13 +42,13 @@ def pushoutCocone : Limits.PushoutCocone f g := by
   letI := RingHom.toAlgebra f
   letI := RingHom.toAlgebra g
   fapply Limits.PushoutCocone.mk
-  show CommRingCat; exact CommRingCat.of (A ⊗[R] B)
-  show A ⟶ _; exact Algebra.TensorProduct.includeLeftRingHom
-  show B ⟶ _; exact Algebra.TensorProduct.includeRight.toRingHom
-  ext r
-  trans algebraMap R (A ⊗[R] B) r
-  · exact Algebra.TensorProduct.includeLeft.commutes (R := R) r
-  · exact (Algebra.TensorProduct.includeRight.commutes (R := R) r).symm
+  · show CommRingCat; exact CommRingCat.of (A ⊗[R] B)
+  · show A ⟶ _; exact Algebra.TensorProduct.includeLeftRingHom
+  · show B ⟶ _; exact Algebra.TensorProduct.includeRight.toRingHom
+  · ext r
+    trans algebraMap R (A ⊗[R] B) r
+    · exact Algebra.TensorProduct.includeLeft.commutes (R := R) r
+    · exact (Algebra.TensorProduct.includeRight.commutes (R := R) r).symm
 set_option linter.uppercaseLean3 false in
 #align CommRing.pushout_cocone CommRingCat.pushoutCocone
 

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -97,7 +97,7 @@ theorem one_le_succ_nth_stream_b {ifp_succ_n : IntFractPair K}
   obtain ⟨ifp_n, nth_stream_eq, stream_nth_fr_ne_zero, ⟨-⟩⟩ :
     ∃ ifp_n,
       IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
-  exact succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
+  · exact succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
   suffices 1 ≤ ifp_n.fr⁻¹ by rwa [IntFractPair.of, le_floor, cast_one]
   suffices ifp_n.fr ≤ 1 by
     have h : 0 < ifp_n.fr :=
@@ -474,7 +474,7 @@ theorem abs_sub_convergents_le (not_terminated_at_n : ¬(of v).TerminatedAt n) :
   obtain ⟨ifp_n, stream_nth_eq, stream_nth_fr_ne_zero, if_of_eq_ifp_succ_n⟩ :
     ∃ ifp_n,
       IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
-  exact IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
+  · exact IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
   let denom' := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
   -- now we can use `sub_convergents_eq` to simplify our goal
   suffices |(-1) ^ n / denom'| ≤ 1 / denom by

Mathlib/Algebra/GCDMonoid/Finset.lean

@@ -275,7 +275,7 @@ theorem extract_gcd (f : β → α) (hs : s.Nonempty) :
       push_neg at h
       refine' ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ _,
           extract_gcd' f _ h fun b hb ↦ _⟩
-      simp only [hb, hg, dite_true]
+      · simp only [hb, hg, dite_true]
       rw [dif_pos hb, hg hb]
 #align finset.extract_gcd Finset.extract_gcd
 

Mathlib/Algebra/GeomSum.lean

@@ -507,8 +507,8 @@ theorem geom_sum_alternating_of_lt_neg_one [StrictOrderedRing α] (hx : x + 1 <
   by_cases hn' : Even n
   · rw [if_pos hn'] at ihn
     rw [if_neg, lt_add_iff_pos_left]
-    exact mul_pos_of_neg_of_neg hx0 ihn
-    exact not_not_intro hn'
+    · exact mul_pos_of_neg_of_neg hx0 ihn
+    · exact not_not_intro hn'
   · rw [if_neg hn'] at ihn
     rw [if_pos]
     swap

Mathlib/Algebra/GroupPower/Order.lean

@@ -436,7 +436,11 @@ protected lemma Even.add_pow_le (hn : ∃ k, 2 * k = n) :
         rw [Commute.mul_pow]; simp [Commute, SemiconjBy, two_mul, mul_two]
     _ ≤ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) := mul_le_mul_of_nonneg_left
           (add_pow_le (sq_nonneg _) (sq_nonneg _) _) $ pow_nonneg (zero_le_two (α := R)) _
-    _ = _ := by simp only [← mul_assoc, ← pow_add, ← pow_mul]; cases n; rfl; simp [Nat.two_mul]
+    _ = _ := by
+      simp only [← mul_assoc, ← pow_add, ← pow_mul]
+      cases n
+      · rfl
+      · simp [Nat.two_mul]
 
 end LinearOrderedSemiring