diff --git a/Mathlib/Algebra/Category/GroupCat/Colimits.lean b/Mathlib/Algebra/Category/GroupCat/Colimits.lean
index b2293ea9476069..5dd0ab37b2ba62 100644
--- a/Mathlib/Algebra/Category/GroupCat/Colimits.lean
+++ b/Mathlib/Algebra/Category/GroupCat/Colimits.lean
@@ -296,8 +296,8 @@ noncomputable def cokernelIsoQuotient {G H : AddCommGroupCat.{u}} (f : G ⟶ H)
         apply Quotient.sound
         apply leftRel_apply.mpr
         fconstructor
-        exact -x
-        simp only [add_zero, AddMonoidHom.map_neg]
+        · exact -x
+        · simp only [add_zero, AddMonoidHom.map_neg]
   inv :=
     QuotientAddGroup.lift _ (cokernel.π f) <| by
       rintro _ ⟨x, rfl⟩
diff --git a/Mathlib/Algebra/Homology/Exact.lean b/Mathlib/Algebra/Homology/Exact.lean
index ba09c7fbfc2f22..2cb30ad79dc645 100644
--- a/Mathlib/Algebra/Homology/Exact.lean
+++ b/Mathlib/Algebra/Homology/Exact.lean
@@ -190,8 +190,8 @@ theorem exact_comp_hom_inv_comp_iff (i : B ≅ D) : Exact (f ≫ i.hom) (i.inv 
 theorem exact_epi_comp (hgh : Exact g h) [Epi f] : Exact (f ≫ g) h := by
   refine' ⟨by simp [hgh.w], _⟩
   rw [imageToKernel_comp_left]
-  haveI := hgh.epi
-  infer_instance
+  · haveI := hgh.epi
+    infer_instance
 #align category_theory.exact_epi_comp CategoryTheory.exact_epi_comp
 
 @[simp]
diff --git a/Mathlib/Algebra/Homology/LocalCohomology.lean b/Mathlib/Algebra/Homology/LocalCohomology.lean
index a9373ea015d77c..0a8faf4c39ee50 100644
--- a/Mathlib/Algebra/Homology/LocalCohomology.lean
+++ b/Mathlib/Algebra/Homology/LocalCohomology.lean
@@ -250,8 +250,8 @@ instance ideal_powers_initial [hR : IsNoetherian R R] :
       -- The inclusions `J^n1 ≤ J'` and `J^n2 ≤ J'` always form a triangle, based on
       -- which exponent is larger.
       rcases le_total (unop j1.left) (unop j2.left) with h | h
-      right; exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
-      left; exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
+      · right; exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
+      · left; exact ⟨CostructuredArrow.homMk (homOfLE h).op (AsTrue.get trivial)⟩
 #align local_cohomology.ideal_powers_initial localCohomology.ideal_powers_initial
 
 example : HasColimitsOfSize.{0, 0, u, u + 1} (ModuleCat.{u, u} R) := inferInstance
diff --git a/Mathlib/Algebra/Lie/Nilpotent.lean b/Mathlib/Algebra/Lie/Nilpotent.lean
index 9c0042693b4905..c8aa6be02e89ff 100644
--- a/Mathlib/Algebra/Lie/Nilpotent.lean
+++ b/Mathlib/Algebra/Lie/Nilpotent.lean
@@ -175,7 +175,8 @@ theorem iterate_toEndomorphism_mem_lowerCentralSeries (x : L) (m : M) (k : ℕ)
 theorem iterate_toEndomorphism_mem_lowerCentralSeries₂ (x y : L) (m : M) (k : ℕ) :
     (toEndomorphism R L M x ∘ₗ toEndomorphism R L M y)^[k] m ∈
       lowerCentralSeries R L M (2 * k) := by
-  induction' k with k ih; simp
+  induction' k with k ih
+  · simp
   have hk : 2 * k.succ = (2 * k + 1) + 1 := rfl
   simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk,
       toEndomorphism_apply_apply, LinearMap.coe_comp, toEndomorphism_apply_apply]
@@ -860,7 +861,8 @@ variable (R A L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
 lemma LieSubmodule.lowerCentralSeries_tensor_eq_baseChange (k : ℕ) :
     lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k =
     (lowerCentralSeries R L M k).baseChange A := by
-  induction' k with k ih; simp
+  induction' k with k ih
+  · simp
   simp only [lowerCentralSeries_succ, ih, ← baseChange_top, lie_baseChange]
 
 instance LieModule.instIsNilpotentTensor [IsNilpotent R L M] :
diff --git a/Mathlib/Algebra/Module/PID.lean b/Mathlib/Algebra/Module/PID.lean
index c7effdb2cf6366..bb0192637d78ef 100644
--- a/Mathlib/Algebra/Module/PID.lean
+++ b/Mathlib/Algebra/Module/PID.lean
@@ -93,7 +93,7 @@ theorem Submodule.exists_isInternal_prime_power_torsion_of_pid [Module.Finite R
     ∃ (ι : Type u) (_ : Fintype ι) (_ : DecidableEq ι) (p : ι → R) (_ : ∀ i, Irreducible <| p i)
         (e : ι → ℕ), DirectSum.IsInternal fun i => torsionBy R M <| p i ^ e i := by
   refine' ⟨_, _, _, _, _, _, Submodule.isInternal_prime_power_torsion_of_pid hM⟩
-  exact Finset.fintypeCoeSort _
+  · exact Finset.fintypeCoeSort _
   · rintro ⟨p, hp⟩
     have hP := prime_of_factor p (Multiset.mem_toFinset.mp hp)
     haveI := Ideal.isPrime_of_prime hP
@@ -131,17 +131,18 @@ theorem p_pow_smul_lift {x y : M} {k : ℕ} (hM' : Module.IsTorsionBy R M (p ^ p
   · let f :=
       ((R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq _ ?_).trans
         (quotTorsionOfEquivSpanSingleton R M y)
-    have : f.symm ⟨p ^ k • x, h⟩ ∈
-        R ∙ Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) (p ^ k) := by
-      rw [← Quotient.torsionBy_eq_span_singleton, mem_torsionBy_iff, ← f.symm.map_smul]
-      convert f.symm.map_zero; ext
-      rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk, @hM' x]
-      · exact mem_nonZeroDivisors_of_ne_zero (pow_ne_zero _ hp.ne_zero)
-    rw [Submodule.mem_span_singleton] at this; obtain ⟨a, ha⟩ := this; use a
-    rw [f.eq_symm_apply, ← Ideal.Quotient.mk_eq_mk, ← Quotient.mk_smul] at ha
-    dsimp only [smul_eq_mul, LinearEquiv.trans_apply, Submodule.quotEquivOfEq_mk,
-      quotTorsionOfEquivSpanSingleton_apply_mk] at ha
-    rw [smul_smul, mul_comm]; exact congr_arg ((↑) : _ → M) ha.symm
+    · have : f.symm ⟨p ^ k • x, h⟩ ∈
+          R ∙ Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k) (p ^ k) := by
+        rw [← Quotient.torsionBy_eq_span_singleton, mem_torsionBy_iff, ← f.symm.map_smul]
+        · convert f.symm.map_zero; ext
+          rw [coe_smul_of_tower, coe_mk, coe_zero, smul_smul, ← pow_add, Nat.sub_add_cancel hk,
+            @hM' x]
+        · exact mem_nonZeroDivisors_of_ne_zero (pow_ne_zero _ hp.ne_zero)
+      rw [Submodule.mem_span_singleton] at this; obtain ⟨a, ha⟩ := this; use a
+      rw [f.eq_symm_apply, ← Ideal.Quotient.mk_eq_mk, ← Quotient.mk_smul] at ha
+      dsimp only [smul_eq_mul, LinearEquiv.trans_apply, Submodule.quotEquivOfEq_mk,
+        quotTorsionOfEquivSpanSingleton_apply_mk] at ha
+      rw [smul_smul, mul_comm]; exact congr_arg ((↑) : _ → M) ha.symm
     · symm; convert Ideal.torsionOf_eq_span_pow_pOrder hp hM y
       rw [← pow_add, Nat.sub_add_cancel hk]
   · use 0
@@ -188,9 +189,9 @@ theorem torsion_by_prime_power_decomposition (hN : Module.IsTorsion' N (Submonoi
     -- Porting note(https://github.com/leanprover-community/mathlib4/issues/5732):
     -- `obtain` doesn't work with placeholders.
     have := IH ?_ s' ?_
-    obtain ⟨k, ⟨f⟩⟩ := this
-    clear IH
-    · have : ∀ i : Fin d,
+    · obtain ⟨k, ⟨f⟩⟩ := this
+      clear IH
+      have : ∀ i : Fin d,
           ∃ x : N, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = DirectSum.lof R _ _ i 1 := by
         intro i
         let fi := f.symm.toLinearMap.comp (DirectSum.lof _ _ _ i)
diff --git a/Mathlib/Algebra/Module/Torsion.lean b/Mathlib/Algebra/Module/Torsion.lean
index dadc048824a923..6b6adb40c05d62 100644
--- a/Mathlib/Algebra/Module/Torsion.lean
+++ b/Mathlib/Algebra/Module/Torsion.lean
@@ -442,11 +442,11 @@ theorem iSup_torsionBy_eq_torsionBy_prod :
   rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ←
     Ideal.finset_inf_span_singleton _ _ hq, Finset.inf_eq_iInf, ←
     iSup_torsionBySet_ideal_eq_torsionBySet_iInf]
-  congr
-  ext : 1
-  congr
-  ext : 1
-  exact (torsionBySet_span_singleton_eq _).symm
+  · congr
+    ext : 1
+    congr
+    ext : 1
+    exact (torsionBySet_span_singleton_eq _).symm
   exact fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime _ _).mpr (hq hi hj ij)
 #align submodule.supr_torsion_by_eq_torsion_by_prod Submodule.iSup_torsionBy_eq_torsionBy_prod
 
diff --git a/Mathlib/Algebra/Order/Archimedean.lean b/Mathlib/Algebra/Order/Archimedean.lean
index e9ed5a15df6c55..070cc16eb39aab 100644
--- a/Mathlib/Algebra/Order/Archimedean.lean
+++ b/Mathlib/Algebra/Order/Archimedean.lean
@@ -291,10 +291,10 @@ theorem exists_rat_btwn {x y : α} (h : x < y) : ∃ q : ℚ, x < q ∧ (q : α)
   have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh
   have n0 := Nat.cast_pos.1 n0'
   rw [Rat.cast_div_of_ne_zero, Rat.cast_natCast, Rat.cast_intCast, div_lt_iff n0']
-  refine' ⟨(lt_div_iff n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), _⟩
-  rw [Int.cast_add, Int.cast_one]
-  refine' lt_of_le_of_lt (add_le_add_right ((zh _).1 le_rfl) _) _
-  rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff' (sub_pos.2 h), one_div]
+  · refine' ⟨(lt_div_iff n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), _⟩
+    rw [Int.cast_add, Int.cast_one]
+    refine' lt_of_le_of_lt (add_le_add_right ((zh _).1 le_rfl) _) _
+    rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff' (sub_pos.2 h), one_div]
   · rw [Rat.den_intCast, Nat.cast_one]
     exact one_ne_zero
   · intro H
diff --git a/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/StructureSheaf.lean
index 702d6574f92c38..9a5ae653ca4165 100644
--- a/Mathlib/AlgebraicGeometry/StructureSheaf.lean
+++ b/Mathlib/AlgebraicGeometry/StructureSheaf.lean
@@ -762,12 +762,13 @@ theorem normalize_finite_fraction_representation (U : Opens (PrimeSpectrum.Top R
     simp only []
     -- Here, both sides of the equation are equal to a restriction of `s`
     trans
-    convert congr_arg ((structureSheaf R).1.map iDj.op) (hs j).symm using 1
-    convert congr_arg ((structureSheaf R).1.map iDi.op) (hs i) using 1; swap
+    on_goal 1 =>
+      convert congr_arg ((structureSheaf R).1.map iDj.op) (hs j).symm using 1
+      convert congr_arg ((structureSheaf R).1.map iDi.op) (hs i) using 1
     all_goals rw [res_const]; apply const_ext; ring
     -- The remaining two goals were generated during the rewrite of `res_const`
     -- These can be solved immediately
-    exacts [PrimeSpectrum.basicOpen_mul_le_right _ _, PrimeSpectrum.basicOpen_mul_le_left _ _]
+    exacts [PrimeSpectrum.basicOpen_mul_le_left _ _, PrimeSpectrum.basicOpen_mul_le_right _ _]
   -- From the equality in the localization, we obtain for each `(i,j)` some power `(h i * h j) ^ n`
   -- which equalizes `a i * h j` and `h i * a j`
   have exists_power :
diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean
index f2f22ce6cbb44f..fd006ed9fa98fd 100644
--- a/Mathlib/Analysis/Analytic/Composition.lean
+++ b/Mathlib/Analysis/Analytic/Composition.lean
@@ -391,18 +391,18 @@ theorem comp_id (p : FormalMultilinearSeries 𝕜 E F) : p.comp (id 𝕜 E) = p
   ext1 n
   dsimp [FormalMultilinearSeries.comp]
   rw [Finset.sum_eq_single (Composition.ones n)]
-  show compAlongComposition p (id 𝕜 E) (Composition.ones n) = p n
-  · ext v
+  · show compAlongComposition p (id 𝕜 E) (Composition.ones n) = p n
+    ext v
     rw [compAlongComposition_apply]
     apply p.congr (Composition.ones_length n)
     intros
     rw [applyComposition_ones]
     refine' congr_arg v _
     rw [Fin.ext_iff, Fin.coe_castLE, Fin.val_mk]
-  show
+  · show
     ∀ b : Composition n,
       b ∈ Finset.univ → b ≠ Composition.ones n → compAlongComposition p (id 𝕜 E) b = 0
-  · intro b _ hb
+    intro b _ hb
     obtain ⟨k, hk, lt_k⟩ : ∃ (k : ℕ), k ∈ Composition.blocks b ∧ 1 < k :=
       Composition.ne_ones_iff.1 hb
     obtain ⟨i, hi⟩ : ∃ (i : Fin b.blocks.length), b.blocks.get i = k :=
@@ -430,16 +430,16 @@ theorem id_comp (p : FormalMultilinearSeries 𝕜 E F) (h : p 0 = 0) : (id 𝕜
   · dsimp [FormalMultilinearSeries.comp]
     have n_pos : 0 < n := bot_lt_iff_ne_bot.mpr hn
     rw [Finset.sum_eq_single (Composition.single n n_pos)]
-    show compAlongComposition (id 𝕜 F) p (Composition.single n n_pos) = p n
-    · ext v
+    · show compAlongComposition (id 𝕜 F) p (Composition.single n n_pos) = p n
+      ext v
       rw [compAlongComposition_apply, id_apply_one' _ _ (Composition.single_length n_pos)]
       dsimp [applyComposition]
       refine' p.congr rfl fun i him hin => congr_arg v <| _
       ext; simp
-    show
+    · show
       ∀ b : Composition n,
         b ∈ Finset.univ → b ≠ Composition.single n n_pos → compAlongComposition (id 𝕜 F) p b = 0
-    · intro b _ hb
+      intro b _ hb
       have A : b.length ≠ 1 := by simpa [Composition.eq_single_iff_length] using hb
       ext v
       rw [compAlongComposition_apply, id_apply_ne_one _ _ A]
@@ -1144,14 +1144,14 @@ def sigmaEquivSigmaPi (n : ℕ) :
       simp only [map_ofFn]
       rfl
     · rw [Fin.heq_fun_iff]
-      intro i
-      dsimp [Composition.sigmaCompositionAux]
-      rw [get_of_eq (splitWrtComposition_join _ _ _)]
-      · simp only [get_ofFn]
-        rfl
-      · simp only [map_ofFn]
-        rfl
-      · congr
+      · intro i
+        dsimp [Composition.sigmaCompositionAux]
+        rw [get_of_eq (splitWrtComposition_join _ _ _)]
+        · simp only [get_ofFn]
+          rfl
+        · simp only [map_ofFn]
+          rfl
+        · congr
 #align composition.sigma_equiv_sigma_pi Composition.sigmaEquivSigmaPi
 
 end Composition
diff --git a/Mathlib/Analysis/Calculus/Deriv/Slope.lean b/Mathlib/Analysis/Calculus/Deriv/Slope.lean
index 5ea9342815b0de..ad64511be5dcac 100644
--- a/Mathlib/Analysis/Calculus/Deriv/Slope.lean
+++ b/Mathlib/Analysis/Calculus/Deriv/Slope.lean
@@ -129,7 +129,7 @@ theorem range_derivWithin_subset_closure_span_image
     suffices A : f x ∈ closure (f '' (s ∩ t)) from
       closure_mono (image_subset _ (inter_subset_right _ _)) A
     apply ContinuousWithinAt.mem_closure_image
-    apply H'.continuousWithinAt.mono (inter_subset_left _ _)
+    · apply H'.continuousWithinAt.mono (inter_subset_left _ _)
     rw [mem_closure_iff_nhdsWithin_neBot]
     exact I.mono (nhdsWithin_mono _ (diff_subset _ _))
 
diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
index 87269d6ea78c22..25e1c935f8c857 100644
--- a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
+++ b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
@@ -236,7 +236,10 @@ theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f
         _ ≤ f'symm.nnnorm * dist (f (u n)) y + dist (u n) b := add_le_add (A _) le_rfl
         _ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) +
               f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n) / (1 - c * f'symm.nnnorm) *
-                dist (f b) y := by gcongr; exact IH.1; exact IH.2
+                dist (f b) y := by
+                  gcongr
+                  · exact IH.1
+                  · exact IH.2
         _ = f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n.succ) /
               (1 - (c : ℝ) * f'symm.nnnorm) * dist (f b) y := by
           field_simp [Jcf', pow_succ]; ring
diff --git a/Mathlib/Analysis/Calculus/LocalExtr/Basic.lean b/Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
index 8980e514563af9..0eb32006f00b3a 100644
--- a/Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
+++ b/Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
@@ -88,12 +88,12 @@ theorem mem_posTangentConeAt_of_segment_subset {s : Set E} {x y : E} (h : segmen
   let c := fun n : ℕ => (2 : ℝ) ^ n
   let d := fun n : ℕ => (c n)⁻¹ • (y - x)
   refine' ⟨c, d, Filter.univ_mem' fun n => h _, tendsto_pow_atTop_atTop_of_one_lt one_lt_two, _⟩
-  show x + d n ∈ segment ℝ x y
-  · rw [segment_eq_image']
+  · show x + d n ∈ segment ℝ x y
+    rw [segment_eq_image']
     refine' ⟨(c n)⁻¹, ⟨_, _⟩, rfl⟩
     exacts [inv_nonneg.2 (pow_nonneg zero_le_two _), inv_le_one (one_le_pow_of_one_le one_le_two _)]
-  show Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
-  · exact tendsto_const_nhds.congr fun n ↦ (smul_inv_smul₀ (pow_ne_zero _ two_ne_zero) _).symm
+  · show Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
+    exact tendsto_const_nhds.congr fun n ↦ (smul_inv_smul₀ (pow_ne_zero _ two_ne_zero) _).symm
 #align mem_pos_tangent_cone_at_of_segment_subset mem_posTangentConeAt_of_segment_subset
 
 theorem mem_posTangentConeAt_of_segment_subset' {s : Set E} {x y : E}
diff --git a/Mathlib/Analysis/Calculus/TangentCone.lean b/Mathlib/Analysis/Calculus/TangentCone.lean
index 6d4e1530318b0e..2af9b04d5162f1 100644
--- a/Mathlib/Analysis/Calculus/TangentCone.lean
+++ b/Mathlib/Analysis/Calculus/TangentCone.lean
@@ -150,8 +150,8 @@ theorem subset_tangentCone_prod_left {t : Set F} {y : F} (ht : y ∈ closure t)
     exact ⟨z - y, by simpa using hzt, by simpa using hz⟩
   choose d' hd' using this
   refine' ⟨c, fun n => (d n, d' n), _, hc, _⟩
-  show ∀ᶠ n in atTop, (x, y) + (d n, d' n) ∈ s ×ˢ t
-  · filter_upwards [hd] with n hn
+  · show ∀ᶠ n in atTop, (x, y) + (d n, d' n) ∈ s ×ˢ t
+    filter_upwards [hd] with n hn
     simp [hn, (hd' n).1]
   · apply Tendsto.prod_mk_nhds hy _
     refine' squeeze_zero_norm (fun n => (hd' n).2.le) _
@@ -170,8 +170,8 @@ theorem subset_tangentCone_prod_right {t : Set F} {y : F} (hs : x ∈ closure s)
     exact ⟨z - x, by simpa using hzs, by simpa using hz⟩
   choose d' hd' using this
   refine' ⟨c, fun n => (d' n, d n), _, hc, _⟩
-  show ∀ᶠ n in atTop, (x, y) + (d' n, d n) ∈ s ×ˢ t
-  · filter_upwards [hd] with n hn
+  · show ∀ᶠ n in atTop, (x, y) + (d' n, d n) ∈ s ×ˢ t
+    filter_upwards [hd] with n hn
     simp [hn, (hd' n).1]
   · apply Tendsto.prod_mk_nhds _ hy
     refine' squeeze_zero_norm (fun n => (hd' n).2.le) _
diff --git a/Mathlib/Analysis/InnerProductSpace/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Basic.lean
index 032b89cafff7d5..965460e6380fc4 100644
--- a/Mathlib/Analysis/InnerProductSpace/Basic.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Basic.lean
@@ -1590,7 +1590,8 @@ theorem norm_inner_eq_norm_tfae (x y : E) :
       sub_eq_zero] at h
     rw [div_eq_inv_mul, mul_smul, h, inv_smul_smul₀]
     rwa [inner_self_ne_zero]
-  tfae_have 2 → 3; exact fun h => h.imp_right fun h' => ⟨_, h'⟩
+  tfae_have 2 → 3
+  · exact fun h => h.imp_right fun h' => ⟨_, h'⟩
   tfae_have 3 → 1
   · rintro (rfl | ⟨r, rfl⟩) <;>
     simp [inner_smul_right, norm_smul, inner_self_eq_norm_sq_to_K, inner_self_eq_norm_mul_norm,
diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean
index 33ae59da7eccd9..36c9b0547d3100 100644
--- a/Mathlib/Analysis/InnerProductSpace/Projection.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean
@@ -98,69 +98,69 @@ theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h
     use fun n => √(b n)
     constructor
     -- first goal :  `∀ (n : ℕ), 0 ≤ √(b n)`
-    intro n
-    exact sqrt_nonneg _
+    · intro n
+      exact sqrt_nonneg _
     constructor
     -- second goal : `∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ √(b N)`
-    intro p q N hp hq
-    let wp := (w p : F)
-    let wq := (w q : F)
-    let a := u - wq
-    let b := u - wp
-    let half := 1 / (2 : ℝ)
-    let div := 1 / ((N : ℝ) + 1)
-    have :
-      4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ =
-        2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) :=
-      calc
+    · intro p q N hp hq
+      let wp := (w p : F)
+      let wq := (w q : F)
+      let a := u - wq
+      let b := u - wp
+      let half := 1 / (2 : ℝ)
+      let div := 1 / ((N : ℝ) + 1)
+      have :
         4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ =
-            2 * ‖u - half • (wq + wp)‖ * (2 * ‖u - half • (wq + wp)‖) + ‖wp - wq‖ * ‖wp - wq‖ :=
-          by ring
-        _ =
-            absR (2 : ℝ) * ‖u - half • (wq + wp)‖ * (absR (2 : ℝ) * ‖u - half • (wq + wp)‖) +
-              ‖wp - wq‖ * ‖wp - wq‖ := by
-          rw [_root_.abs_of_nonneg]
-          exact zero_le_two
-        _ =
-            ‖(2 : ℝ) • (u - half • (wq + wp))‖ * ‖(2 : ℝ) • (u - half • (wq + wp))‖ +
-              ‖wp - wq‖ * ‖wp - wq‖ :=
-          by simp [norm_smul]
-        _ = ‖a + b‖ * ‖a + b‖ + ‖a - b‖ * ‖a - b‖ := by
-          rw [smul_sub, smul_smul, mul_one_div_cancel (_root_.two_ne_zero : (2 : ℝ) ≠ 0), ←
-            one_add_one_eq_two, add_smul]
-          simp only [one_smul]
-          have eq₁ : wp - wq = a - b := (sub_sub_sub_cancel_left _ _ _).symm
-          have eq₂ : u + u - (wq + wp) = a + b := by
-            show u + u - (wq + wp) = u - wq + (u - wp)
-            abel
-          rw [eq₁, eq₂]
-        _ = 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) := parallelogram_law_with_norm ℝ _ _
-    have eq : δ ≤ ‖u - half • (wq + wp)‖ := by
-      rw [smul_add]
-      apply δ_le'
-      apply h₂
-      repeat' exact Subtype.mem _
-      repeat' exact le_of_lt one_half_pos
-      exact add_halves 1
-    have eq₁ : 4 * δ * δ ≤ 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ := by
-      simp_rw [mul_assoc]
-      gcongr
-    have eq₂ : ‖a‖ ≤ δ + div :=
-        le_trans (le_of_lt <| hw q) (add_le_add_left (Nat.one_div_le_one_div hq) _)
-    have eq₂' : ‖b‖ ≤ δ + div :=
-        le_trans (le_of_lt <| hw p) (add_le_add_left (Nat.one_div_le_one_div hp) _)
-    rw [dist_eq_norm]
-    apply nonneg_le_nonneg_of_sq_le_sq
-    · exact sqrt_nonneg _
-    rw [mul_self_sqrt]
-    calc
-      ‖wp - wq‖ * ‖wp - wq‖ =
-          2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) - 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ := by
-        simp [← this]
-      _ ≤ 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) - 4 * δ * δ := by gcongr
-      _ ≤ 2 * ((δ + div) * (δ + div) + (δ + div) * (δ + div)) - 4 * δ * δ := by gcongr
-      _ = 8 * δ * div + 4 * div * div := by ring
-    positivity
+          2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) :=
+        calc
+          4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ =
+              2 * ‖u - half • (wq + wp)‖ * (2 * ‖u - half • (wq + wp)‖) + ‖wp - wq‖ * ‖wp - wq‖ :=
+            by ring
+          _ =
+              absR (2 : ℝ) * ‖u - half • (wq + wp)‖ * (absR (2 : ℝ) * ‖u - half • (wq + wp)‖) +
+                ‖wp - wq‖ * ‖wp - wq‖ := by
+            rw [_root_.abs_of_nonneg]
+            exact zero_le_two
+          _ =
+              ‖(2 : ℝ) • (u - half • (wq + wp))‖ * ‖(2 : ℝ) • (u - half • (wq + wp))‖ +
+                ‖wp - wq‖ * ‖wp - wq‖ :=
+            by simp [norm_smul]
+          _ = ‖a + b‖ * ‖a + b‖ + ‖a - b‖ * ‖a - b‖ := by
+            rw [smul_sub, smul_smul, mul_one_div_cancel (_root_.two_ne_zero : (2 : ℝ) ≠ 0), ←
+              one_add_one_eq_two, add_smul]
+            simp only [one_smul]
+            have eq₁ : wp - wq = a - b := (sub_sub_sub_cancel_left _ _ _).symm
+            have eq₂ : u + u - (wq + wp) = a + b := by
+              show u + u - (wq + wp) = u - wq + (u - wp)
+              abel
+            rw [eq₁, eq₂]
+          _ = 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) := parallelogram_law_with_norm ℝ _ _
+      have eq : δ ≤ ‖u - half • (wq + wp)‖ := by
+        rw [smul_add]
+        apply δ_le'
+        apply h₂
+        repeat' exact Subtype.mem _
+        repeat' exact le_of_lt one_half_pos
+        exact add_halves 1
+      have eq₁ : 4 * δ * δ ≤ 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ := by
+        simp_rw [mul_assoc]
+        gcongr
+      have eq₂ : ‖a‖ ≤ δ + div :=
+          le_trans (le_of_lt <| hw q) (add_le_add_left (Nat.one_div_le_one_div hq) _)
+      have eq₂' : ‖b‖ ≤ δ + div :=
+          le_trans (le_of_lt <| hw p) (add_le_add_left (Nat.one_div_le_one_div hp) _)
+      rw [dist_eq_norm]
+      apply nonneg_le_nonneg_of_sq_le_sq
+      · exact sqrt_nonneg _
+      rw [mul_self_sqrt]
+      · calc
+        ‖wp - wq‖ * ‖wp - wq‖ =
+            2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) - 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ := by
+          simp [← this]
+        _ ≤ 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) - 4 * δ * δ := by gcongr
+        _ ≤ 2 * ((δ + div) * (δ + div) + (δ + div) * (δ + div)) - 4 * δ * δ := by gcongr
+        _ = 8 * δ * div + 4 * div * div := by ring
+      positivity
     -- third goal : `Tendsto (fun (n : ℕ) => √(b n)) atTop (𝓝 0)`
     suffices Tendsto (fun x ↦ √(8 * δ * x + 4 * x * x) : ℝ → ℝ) (𝓝 0) (𝓝 0)
       from this.comp tendsto_one_div_add_atTop_nhds_zero_nat
@@ -578,7 +578,7 @@ theorem LinearIsometry.map_orthogonalProjection {E E' : Type*} [NormedAddCommGro
     (p : Submodule 𝕜 E) [HasOrthogonalProjection p] [HasOrthogonalProjection (p.map f.toLinearMap)]
     (x : E) : f (orthogonalProjection p x) = orthogonalProjection (p.map f.toLinearMap) (f x) := by
   refine' (eq_orthogonalProjection_of_mem_of_inner_eq_zero _ fun y hy => _).symm
-  refine' Submodule.apply_coe_mem_map _ _
+  · refine' Submodule.apply_coe_mem_map _ _
   rcases hy with ⟨x', hx', rfl : f x' = y⟩
   rw [← f.map_sub, f.inner_map_map, orthogonalProjection_inner_eq_zero x x' hx']
 #align linear_isometry.map_orthogonal_projection LinearIsometry.map_orthogonalProjection
diff --git a/Mathlib/Analysis/MeanInequalitiesPow.lean b/Mathlib/Analysis/MeanInequalitiesPow.lean
index 1bf3e34cfabc77..be858d3ede55ae 100644
--- a/Mathlib/Analysis/MeanInequalitiesPow.lean
+++ b/Mathlib/Analysis/MeanInequalitiesPow.lean
@@ -103,7 +103,7 @@ theorem arith_mean_le_rpow_mean (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
     ∑ i in s, w i * z i ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p) := by
   have : 0 < p := by positivity
   rw [← rpow_le_rpow_iff _ _ this, ← rpow_mul, one_div_mul_cancel (ne_of_gt this), rpow_one]
-  exact rpow_arith_mean_le_arith_mean_rpow s w z hw hw' hz hp
+  · exact rpow_arith_mean_le_arith_mean_rpow s w z hw hw' hz hp
   all_goals
     apply_rules [sum_nonneg, rpow_nonneg]
     intro i hi
diff --git a/Mathlib/Analysis/Normed/Group/ControlledClosure.lean b/Mathlib/Analysis/Normed/Group/ControlledClosure.lean
index bcafee048f5f88..197154a8883ae5 100644
--- a/Mathlib/Analysis/Normed/Group/ControlledClosure.lean
+++ b/Mathlib/Analysis/Normed/Group/ControlledClosure.lean
@@ -57,12 +57,12 @@ theorem controlled_closure_of_complete {f : NormedAddGroupHom G H} {K : AddSubgr
   set s : ℕ → G := fun n => ∑ k in range (n + 1), u k
   have : CauchySeq s := by
     apply NormedAddCommGroup.cauchy_series_of_le_geometric'' (by norm_num) one_half_lt_one
-    rintro n (hn : n ≥ 1)
-    calc
-      ‖u n‖ ≤ C * ‖v n‖ := hnorm_u n
-      _ ≤ C * b n := by gcongr; exact (hv _ <| Nat.succ_le_iff.mp hn).le
-      _ = (1 / 2) ^ n * (ε * ‖h‖ / 2) := by simp [mul_div_cancel₀ _ hC.ne.symm]
-      _ = ε * ‖h‖ / 2 * (1 / 2) ^ n := mul_comm _ _
+    · rintro n (hn : n ≥ 1)
+      calc
+        ‖u n‖ ≤ C * ‖v n‖ := hnorm_u n
+        _ ≤ C * b n := by gcongr; exact (hv _ <| Nat.succ_le_iff.mp hn).le
+        _ = (1 / 2) ^ n * (ε * ‖h‖ / 2) := by simp [mul_div_cancel₀ _ hC.ne.symm]
+        _ = ε * ‖h‖ / 2 * (1 / 2) ^ n := mul_comm _ _
   -- We now show that the limit `g` of `s` is the desired preimage.
   obtain ⟨g : G, hg⟩ := cauchySeq_tendsto_of_complete this
   refine' ⟨g, _, _⟩
diff --git a/Mathlib/Analysis/Normed/Group/Pointwise.lean b/Mathlib/Analysis/Normed/Group/Pointwise.lean
index ad7ecb024ec7e9..693348aba2a9c8 100644
--- a/Mathlib/Analysis/Normed/Group/Pointwise.lean
+++ b/Mathlib/Analysis/Normed/Group/Pointwise.lean
@@ -221,7 +221,7 @@ theorem smul_closedBall_one : x • closedBall (1 : E) δ = closedBall x δ := b
 theorem mul_ball_one : s * ball 1 δ = thickening δ s := by
   rw [thickening_eq_biUnion_ball]
   convert iUnion₂_mul (fun x (_ : x ∈ s) => {x}) (ball (1 : E) δ)
-  exact s.biUnion_of_singleton.symm
+  · exact s.biUnion_of_singleton.symm
   ext x
   simp_rw [singleton_mul_ball, mul_one]
 #align mul_ball_one mul_ball_one
diff --git a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean
index 38fd38c9c53920..967f2a8a2a1e5e 100644
--- a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean
+++ b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean
@@ -466,7 +466,10 @@ theorem FiniteDimensional.of_isCompact_closedBall₀ {r : ℝ} (rpos : 0 < r)
     intro n
     simp only [g, norm_smul, dist_zero_right, Metric.mem_closedBall]
     calc
-      ‖c‖ * ‖f n‖ ≤ r / R * R := by gcongr; exact hc.2.le; apply fle
+      ‖c‖ * ‖f n‖ ≤ r / R * R := by
+        gcongr
+        · exact hc.2.le
+        · apply fle
       _ = r := by field_simp [(zero_lt_one.trans Rgt).ne']
   -- Porting note: moved type ascriptions because of exists_prop changes
   obtain ⟨x : E, _ : x ∈ Metric.closedBall (0 : E) r, φ : ℕ → ℕ, φmono : StrictMono φ,
diff --git a/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean b/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
index 4da5ec28f5b95f..6835d9ce767868 100644
--- a/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
+++ b/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
@@ -50,13 +50,13 @@ theorem separate_convex_open_set [TopologicalSpace E] [AddCommGroup E] [Topologi
   let f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (ne_of_mem_of_not_mem hs₀ hx₀).symm
   have := exists_extension_of_le_sublinear f (gauge s) (fun c hc => gauge_smul_of_nonneg hc.le)
     (gauge_add_le hs₁ <| absorbent_nhds_zero <| hs₂.mem_nhds hs₀) ?_
-  obtain ⟨φ, hφ₁, hφ₂⟩ := this
-  have hφ₃ : φ x₀ = 1 := by
-    rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁,
-      LinearPMap.mkSpanSingleton'_apply_self]
-  have hφ₄ : ∀ x ∈ s, φ x < 1 := fun x hx =>
-    (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_isOpen hs₂ hx)
-  · refine' ⟨⟨φ, _⟩, hφ₃, hφ₄⟩
+  · obtain ⟨φ, hφ₁, hφ₂⟩ := this
+    have hφ₃ : φ x₀ = 1 := by
+      rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁,
+        LinearPMap.mkSpanSingleton'_apply_self]
+    have hφ₄ : ∀ x ∈ s, φ x < 1 := fun x hx =>
+      (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_isOpen hs₂ hx)
+    refine' ⟨⟨φ, _⟩, hφ₃, hφ₄⟩
     refine'
       φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (Nonempty.vadd_set ⟨0, hs₀⟩)
         (vadd_set_subset_iff.mpr fun x hx => _)
diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
index 6d55de83b5bf46..1b26bc627a2742 100644
--- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
+++ b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
@@ -139,8 +139,7 @@ theorem exists_bound_of_continuous (hf : Continuous f) :
     ∃ C : ℝ, 0 < C ∧ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖ := by
   cases isEmpty_or_nonempty ι
   · refine' ⟨‖f 0‖ + 1, add_pos_of_nonneg_of_pos (norm_nonneg _) zero_lt_one, fun m => _⟩
-    obtain rfl : m = 0
-    exact funext (IsEmpty.elim ‹_›)
+    obtain rfl : m = 0 := funext (IsEmpty.elim ‹_›)
     simp [univ_eq_empty, zero_le_one]
   obtain ⟨ε : ℝ, ε0 : 0 < ε, hε : ∀ m : ∀ i, E i, ‖m - 0‖ < ε → ‖f m - f 0‖ < 1⟩ :=
     NormedAddCommGroup.tendsto_nhds_nhds.1 (hf.tendsto 0) 1 zero_lt_one
diff --git a/Mathlib/Analysis/NormedSpace/Star/Basic.lean b/Mathlib/Analysis/NormedSpace/Star/Basic.lean
index 157131d0c829a6..627e818de6a336 100644
--- a/Mathlib/Analysis/NormedSpace/Star/Basic.lean
+++ b/Mathlib/Analysis/NormedSpace/Star/Basic.lean
@@ -173,8 +173,8 @@ instance _root_.Prod.cstarRing : CstarRing (R₁ × R₂) where
     simp only [Prod.fst_mul, Prod.fst_star, Prod.snd_mul, Prod.snd_star, norm_star_mul_self, ← sq]
     refine' le_antisymm _ _
     · refine' max_le _ _ <;> rw [sq_le_sq, abs_of_nonneg (norm_nonneg _)]
-      exact (le_max_left _ _).trans (le_abs_self _)
-      exact (le_max_right _ _).trans (le_abs_self _)
+      · exact (le_max_left _ _).trans (le_abs_self _)
+      · exact (le_max_right _ _).trans (le_abs_self _)
     · rw [le_sup_iff]
       rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h) <;> simp [h]
 #align prod.cstar_ring Prod.cstarRing
diff --git a/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean b/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean
index 2b61f71325f165..0b0a4daabd908c 100644
--- a/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean
+++ b/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean
@@ -576,9 +576,9 @@ instance [CompleteSpace A] : CompleteSpace 𝓜(𝕜, A) := by
   apply IsClosed.isComplete
   simp only [range_toProdMulOpposite, Set.setOf_forall]
   refine' isClosed_iInter fun x => isClosed_iInter fun y => isClosed_eq _ _
-  exact
-    ((ContinuousLinearMap.apply 𝕜 A _).continuous.comp <| continuous_unop.comp continuous_snd).mul
-      continuous_const
+  · exact
+      ((ContinuousLinearMap.apply 𝕜 A _).continuous.comp <| continuous_unop.comp continuous_snd).mul
+        continuous_const
   exact continuous_const.mul ((ContinuousLinearMap.apply 𝕜 A _).continuous.comp continuous_fst)
 
 variable [StarRing A] [CstarRing A]
diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean
index 5c05129be253ef..e51b92179f6eef 100644
--- a/Mathlib/Analysis/NormedSpace/lpSpace.lean
+++ b/Mathlib/Analysis/NormedSpace/lpSpace.lean
@@ -1239,7 +1239,8 @@ theorem LipschitzOnWith.coordinate [PseudoMetricSpace α] (f : α → ℓ^∞(ι
       dist (f x i) (f y i) ≤ dist (f x) (f y) := lp.norm_apply_le_norm top_ne_zero (f x - f y) i
       _ ≤ K * dist x y := hfl x hx y hy
   · intro hgl x hx y hy
-    apply lp.norm_le_of_forall_le; positivity
+    apply lp.norm_le_of_forall_le
+    · positivity
     intro i
     apply hgl i x hx y hy
 
diff --git a/Mathlib/Analysis/PSeries.lean b/Mathlib/Analysis/PSeries.lean
index 50bac381f1bd26..ba4f732fd37a47 100644
--- a/Mathlib/Analysis/PSeries.lean
+++ b/Mathlib/Analysis/PSeries.lean
@@ -51,7 +51,7 @@ theorem le_sum_condensed' (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m
   · simp
   suffices (∑ k in Ico (2 ^ n) (2 ^ (n + 1)), f k) ≤ 2 ^ n • f (2 ^ n) by
     rw [sum_range_succ, ← sum_Ico_consecutive]
-    exact add_le_add ihn this
+    · exact add_le_add ihn this
     exacts [n.one_le_two_pow, Nat.pow_le_pow_of_le_right zero_lt_two n.le_succ]
   have : ∀ k ∈ Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ f (2 ^ n) := fun k hk =>
     hf (pow_pos zero_lt_two _) (mem_Ico.mp hk).1
diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean
index 256681352ca566..37c2c5873bf44d 100644
--- a/Mathlib/Analysis/RCLike/Basic.lean
+++ b/Mathlib/Analysis/RCLike/Basic.lean
@@ -398,8 +398,10 @@ theorem is_real_TFAE (z : K) : TFAE [conj z = z, ∃ r : ℝ, (r : K) = z, ↑(r
   tfae_have 4 → 3
   · intro h
     conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]
-  tfae_have 3 → 2; exact fun h => ⟨_, h⟩
-  tfae_have 2 → 1; exact fun ⟨r, hr⟩ => hr ▸ conj_ofReal _
+  tfae_have 3 → 2
+  · exact fun h => ⟨_, h⟩
+  tfae_have 2 → 1
+  · exact fun ⟨r, hr⟩ => hr ▸ conj_ofReal _
   tfae_finish
 #align is_R_or_C.is_real_tfae RCLike.is_real_TFAE
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
index 3e3f58c652e615..dcdbf66345e7ba 100644
--- a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
@@ -142,7 +142,8 @@ theorem ext_abs_arg_iff {x y : ℂ} : x = y ↔ abs x = abs y ∧ arg x = arg y
 
 theorem arg_mem_Ioc (z : ℂ) : arg z ∈ Set.Ioc (-π) π := by
   have hπ : 0 < π := Real.pi_pos
-  rcases eq_or_ne z 0 with (rfl | hz); simp [hπ, hπ.le]
+  rcases eq_or_ne z 0 with (rfl | hz)
+  · simp [hπ, hπ.le]
   rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos (arg z) (-π) with ⟨N, hN, -⟩
   rw [two_mul, neg_add_cancel_left, ← two_mul, zsmul_eq_mul] at hN
   rw [← abs_mul_cos_add_sin_mul_I z, ← cos_add_int_mul_two_pi _ N, ← sin_add_int_mul_two_pi _ N]
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Base.lean b/Mathlib/Analysis/SpecialFunctions/Log/Base.lean
index 705ac1af4a420b..eef0d8828b36b8 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/Base.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/Base.lean
@@ -136,9 +136,9 @@ theorem logb_rpow : logb b (b ^ x) = x := by
 
 theorem rpow_logb_eq_abs (hx : x ≠ 0) : b ^ logb b x = |x| := by
   apply log_injOn_pos
-  simp only [Set.mem_Ioi]
-  apply rpow_pos_of_pos b_pos
-  simp only [abs_pos, mem_Ioi, Ne, hx, not_false_iff]
+  · simp only [Set.mem_Ioi]
+    apply rpow_pos_of_pos b_pos
+  · simp only [abs_pos, mem_Ioi, Ne, hx, not_false_iff]
   rw [log_rpow b_pos, logb, log_abs]
   field_simp [log_b_ne_zero b_pos b_ne_one]
 #align real.rpow_logb_eq_abs Real.rpow_logb_eq_abs
@@ -399,8 +399,8 @@ theorem tendsto_logb_atTop_of_base_lt_one : Tendsto (logb b) atTop atBot := by
   simp only [and_imp, sup_le_iff]
   intro ha
   rw [logb_le_iff_le_rpow_of_base_lt_one b_pos b_lt_one]
-  tauto
-  exact lt_of_lt_of_le zero_lt_one ha
+  · tauto
+  · exact lt_of_lt_of_le zero_lt_one ha
 #align real.tendsto_logb_at_top_of_base_lt_one Real.tendsto_logb_atTop_of_base_lt_one
 
 end BPosAndBLtOne
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean b/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
index 0e2c1a3df52423..f618e53d3c14ab 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
@@ -66,20 +66,20 @@ theorem log_div_self_rpow_antitoneOn {a : ℝ} (ha : 0 < a) :
   rw [← div_self (ne_of_lt ha).symm, div_eq_mul_one_div a a, rpow_mul y_nonneg, rpow_mul x_nonneg,
     log_rpow (rpow_pos_of_pos y_pos a), log_rpow (rpow_pos_of_pos x_pos a), mul_div_assoc,
     mul_div_assoc, mul_le_mul_left (one_div_pos.mpr ha)]
-  · refine' log_div_self_antitoneOn _ _ _
-    · simp only [Set.mem_setOf_eq]
-      convert rpow_le_rpow _ hex (le_of_lt ha) using 1
-      rw [← exp_mul]
+  refine' log_div_self_antitoneOn _ _ _
+  · simp only [Set.mem_setOf_eq]
+    convert rpow_le_rpow _ hex (le_of_lt ha) using 1
+    · rw [← exp_mul]
       simp only [Real.exp_eq_exp]
       field_simp [(ne_of_lt ha).symm]
-      exact le_of_lt (exp_pos (1 / a))
-    · simp only [Set.mem_setOf_eq]
-      convert rpow_le_rpow _ (_root_.trans hex hxy) (le_of_lt ha) using 1
-      rw [← exp_mul]
+    exact le_of_lt (exp_pos (1 / a))
+  · simp only [Set.mem_setOf_eq]
+    convert rpow_le_rpow _ (_root_.trans hex hxy) (le_of_lt ha) using 1
+    · rw [← exp_mul]
       simp only [Real.exp_eq_exp]
       field_simp [(ne_of_lt ha).symm]
-      exact le_of_lt (exp_pos (1 / a))
-    gcongr
+    exact le_of_lt (exp_pos (1 / a))
+  gcongr
 #align real.log_div_self_rpow_antitone_on Real.log_div_self_rpow_antitoneOn
 
 theorem log_div_sqrt_antitoneOn : AntitoneOn (fun x : ℝ => log x / √x) { x | exp 2 ≤ x } := by
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
index ebb7b7ccfe54cb..321a6fa33f40eb 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@@ -186,7 +186,8 @@ theorem _root_.Real.list_prod_map_rpow (l : List ℝ) (hl : ∀ x ∈ l, (0 : 
 theorem _root_.Real.list_prod_map_rpow' {ι} (l : List ι) (f : ι → ℝ)
     (hl : ∀ i ∈ l, (0 : ℝ) ≤ f i) (r : ℝ) :
     (l.map (f · ^ r)).prod = (l.map f).prod ^ r := by
-  rw [← Real.list_prod_map_rpow (l.map f) _ r, List.map_map]; rfl
+  rw [← Real.list_prod_map_rpow (l.map f) _ r, List.map_map]
+  · rfl
   simpa using hl
 
 /-- `rpow` version of `Multiset.prod_map_pow`. -/
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
index c0205bd48d209e..9755e288f3d47c 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
@@ -93,11 +93,11 @@ open Real
 
 theorem rpow_def_of_neg {x : ℝ} (hx : x < 0) (y : ℝ) : x ^ y = exp (log x * y) * cos (y * π) := by
   rw [rpow_def, Complex.cpow_def, if_neg]
-  have : Complex.log x * y = ↑(log (-x) * y) + ↑(y * π) * Complex.I := by
-    simp only [Complex.log, abs_of_neg hx, Complex.arg_ofReal_of_neg hx, Complex.abs_ofReal,
-      Complex.ofReal_mul]
-    ring
-  · rw [this, Complex.exp_add_mul_I, ← Complex.ofReal_exp, ← Complex.ofReal_cos, ←
+  · have : Complex.log x * y = ↑(log (-x) * y) + ↑(y * π) * Complex.I := by
+      simp only [Complex.log, abs_of_neg hx, Complex.arg_ofReal_of_neg hx, Complex.abs_ofReal,
+        Complex.ofReal_mul]
+      ring
+    rw [this, Complex.exp_add_mul_I, ← Complex.ofReal_exp, ← Complex.ofReal_cos, ←
       Complex.ofReal_sin, mul_add, ← Complex.ofReal_mul, ← mul_assoc, ← Complex.ofReal_mul,
       Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.ofReal_im,
       Real.log_neg_eq_log]
@@ -549,13 +549,13 @@ theorem monotoneOn_rpow_Ici_of_exponent_nonneg {r : ℝ} (hr : 0 ≤ r) :
 lemma rpow_lt_rpow_of_neg (hx : 0 < x) (hxy : x < y) (hz : z < 0) : y ^ z < x ^ z := by
   have := hx.trans hxy
   rw [← inv_lt_inv, ← rpow_neg, ← rpow_neg]
-  refine rpow_lt_rpow ?_ hxy (neg_pos.2 hz)
+  on_goal 1 => refine rpow_lt_rpow ?_ hxy (neg_pos.2 hz)
   all_goals positivity
 
 lemma rpow_le_rpow_of_nonpos (hx : 0 < x) (hxy : x ≤ y) (hz : z ≤ 0) : y ^ z ≤ x ^ z := by
   have := hx.trans_le hxy
   rw [← inv_le_inv, ← rpow_neg, ← rpow_neg]
-  refine rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)
+  on_goal 1 => refine rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)
   all_goals positivity
 
 theorem rpow_lt_rpow_iff (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 < z) : x ^ z < y ^ z ↔ x < y :=
diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean
index 94a6f47d7eac2f..375aaf6ec292fc 100644
--- a/Mathlib/Analysis/SpecificLimits/Normed.lean
+++ b/Mathlib/Analysis/SpecificLimits/Normed.lean
@@ -140,18 +140,18 @@ theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) :
   have B : Ioo 0 R ⊆ Ioo (-R) R := Subset.trans Ioo_subset_Ico_self A
   -- First we prove that 1-4 are equivalent using 2 → 3 → 4, 1 → 3, and 2 → 1
   tfae_have 1 → 3
-  exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
+  · exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
   tfae_have 2 → 1
-  exact fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
+  · exact fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
   tfae_have 3 → 2
   · rintro ⟨a, ha, H⟩
     rcases exists_between (abs_lt.2 ha) with ⟨b, hab, hbR⟩
     exact ⟨b, ⟨(abs_nonneg a).trans_lt hab, hbR⟩,
       H.trans_isLittleO (isLittleO_pow_pow_of_abs_lt_left (hab.trans_le (le_abs_self b)))⟩
   tfae_have 2 → 4
-  exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
+  · exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
   tfae_have 4 → 3
-  exact fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
+  · exact fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
   -- Add 5 and 6 using 4 → 6 → 5 → 3
   tfae_have 4 → 6
   · rintro ⟨a, ha, H⟩
@@ -159,7 +159,7 @@ theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) :
     refine' ⟨a, ha, C, hC₀, fun n ↦ _⟩
     simpa only [Real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le] using hC (pow_ne_zero n ha.1.ne')
   tfae_have 6 → 5
-  exact fun ⟨a, ha, C, H₀, H⟩ ↦ ⟨a, ha.2, C, Or.inl H₀, H⟩
+  · exact fun ⟨a, ha, C, H₀, H⟩ ↦ ⟨a, ha.2, C, Or.inl H₀, H⟩
   tfae_have 5 → 3
   · rintro ⟨a, ha, C, h₀, H⟩
     rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ (abs_nonneg _).trans (H n) with (rfl | ⟨hC₀, ha₀⟩)
@@ -176,7 +176,7 @@ theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) :
     refine' ⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ _⟩
     rwa [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn
   tfae_have 8 → 7
-  exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, H⟩
+  · exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, H⟩
   tfae_have 7 → 3
   · rintro ⟨a, ha, H⟩
     have : 0 ≤ a := nonneg_of_eventually_pow_nonneg (H.mono fun n ↦ (abs_nonneg _).trans)
diff --git a/Mathlib/CategoryTheory/Abelian/Basic.lean b/Mathlib/CategoryTheory/Abelian/Basic.lean
index 715352974bcdc2..493a8b288a9c87 100644
--- a/Mathlib/CategoryTheory/Abelian/Basic.lean
+++ b/Mathlib/CategoryTheory/Abelian/Basic.lean
@@ -202,8 +202,8 @@ def normalMonoCategory : NormalMonoCategory C where
         have aux : ∀ (s : KernelFork (cokernel.π f)), (limit.lift (parallelPair (cokernel.π f) 0) s
           ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f (by simp))
             = Fork.ι s := ?_
-        refine' isLimitAux _ (fun A => limit.lift _ _ ≫ inv (imageMonoFactorisation f).e) aux _
-        · intro A g hg
+        · refine' isLimitAux _ (fun A => limit.lift _ _ ≫ inv (imageMonoFactorisation f).e) aux _
+          intro A g hg
           rw [KernelFork.ι_ofι] at hg
           rw [← cancel_mono f, hg, ← aux, KernelFork.ι_ofι]
         · intro A
@@ -228,9 +228,9 @@ def normalEpiCategory : NormalEpiCategory C where
         have aux : ∀ (s : CokernelCofork (kernel.ι f)), Cofork.π (CokernelCofork.ofπ f (by simp)) ≫
           inv (imageMonoFactorisation f).m ≫ inv (Abelian.coimageImageComparison f) ≫
           colimit.desc (parallelPair (kernel.ι f) 0) s = Cofork.π s := ?_
-        refine' isColimitAux _ (fun A => inv (imageMonoFactorisation f).m ≫
-                inv (Abelian.coimageImageComparison f) ≫ colimit.desc _ _) aux _
-        · intro A g hg
+        · refine' isColimitAux _ (fun A => inv (imageMonoFactorisation f).m ≫
+                  inv (Abelian.coimageImageComparison f) ≫ colimit.desc _ _) aux _
+          intro A g hg
           rw [CokernelCofork.π_ofπ] at hg
           rw [← cancel_epi f, hg, ← aux, CokernelCofork.π_ofπ]
         · intro A
diff --git a/Mathlib/CategoryTheory/Action.lean b/Mathlib/CategoryTheory/Action.lean
index 9d2c6dc848bcd0..463c093c8d90fe 100644
--- a/Mathlib/CategoryTheory/Action.lean
+++ b/Mathlib/CategoryTheory/Action.lean
@@ -201,13 +201,13 @@ def curry (F : ActionCategory G X ⥤ SingleObj H) : G →* (X → H) ⋊[mulAut
     map_one' := by
       dsimp
       ext1
-      ext b
-      exact F_map_eq.symm.trans (F.map_id b)
+      · ext b
+        exact F_map_eq.symm.trans (F.map_id b)
       rfl
     map_mul' := by
       intro g h
       ext b
-      exact F_map_eq.symm.trans (F.map_comp (homOfPair (g⁻¹ • b) h) (homOfPair b g))
+      · exact F_map_eq.symm.trans (F.map_comp (homOfPair (g⁻¹ • b) h) (homOfPair b g))
       rfl }
 #align category_theory.action_category.curry CategoryTheory.ActionCategory.curry
 
diff --git a/Mathlib/CategoryTheory/Bicategory/NaturalTransformation.lean b/Mathlib/CategoryTheory/Bicategory/NaturalTransformation.lean
index d0b66122aa597a..7be2eed86697d5 100644
--- a/Mathlib/CategoryTheory/Bicategory/NaturalTransformation.lean
+++ b/Mathlib/CategoryTheory/Bicategory/NaturalTransformation.lean
@@ -176,11 +176,11 @@ def vcomp (η : OplaxNatTrans F G) (θ : OplaxNatTrans G H) : OplaxNatTrans F H
                         ?_ ≫ η.app a ◁ θ.naturality f ▷ H.map g ≫ ?_ :=
         ?_
       _ = _ := ?_
-    exact (α_ _ _ _).inv
-    exact (α_ _ _ _).hom ▷ _ ≫ (α_ _ _ _).hom
-    exact _ ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv
-    exact (α_ _ _ _).hom ≫ _ ◁ (α_ _ _ _).inv
-    exact _ ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv
+    · exact (α_ _ _ _).inv
+    · exact (α_ _ _ _).hom ▷ _ ≫ (α_ _ _ _).hom
+    · exact _ ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv
+    · exact (α_ _ _ _).hom ≫ _ ◁ (α_ _ _ _).inv
+    · exact _ ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv
     · rw [whisker_exchange_assoc]
       simp
     · simp
diff --git a/Mathlib/CategoryTheory/Category/Cat/Limit.lean b/Mathlib/CategoryTheory/Category/Cat/Limit.lean
index 7e7c336d3907ec..078c3d0e4bb45e 100644
--- a/Mathlib/CategoryTheory/Category/Cat/Limit.lean
+++ b/Mathlib/CategoryTheory/Category/Cat/Limit.lean
@@ -49,8 +49,8 @@ def homDiagram {F : J ⥤ Cat.{v, v}} (X Y : limit (F ⋙ Cat.objects.{v, v})) :
   obj j := limit.π (F ⋙ Cat.objects) j X ⟶ limit.π (F ⋙ Cat.objects) j Y
   map f g := by
     refine' eqToHom _ ≫ (F.map f).map g ≫ eqToHom _
-    exact (congr_fun (limit.w (F ⋙ Cat.objects) f) X).symm
-    exact congr_fun (limit.w (F ⋙ Cat.objects) f) Y
+    · exact (congr_fun (limit.w (F ⋙ Cat.objects) f) X).symm
+    · exact congr_fun (limit.w (F ⋙ Cat.objects) f) Y
   map_id X := by
     funext f
     letI : Category (objects.obj (F.obj X)) := (inferInstance : Category (F.obj X))
diff --git a/Mathlib/CategoryTheory/Category/PartialFun.lean b/Mathlib/CategoryTheory/Category/PartialFun.lean
index 8c48484f14e32c..3ad583e91c5622 100644
--- a/Mathlib/CategoryTheory/Category/PartialFun.lean
+++ b/Mathlib/CategoryTheory/Category/PartialFun.lean
@@ -161,7 +161,7 @@ noncomputable def partialFunEquivPointed : PartialFun.{u} ≌ Pointed :=
       (fun X ↦ Pointed.Iso.mk (by classical exact Equiv.optionSubtypeNe X.point) (by rfl))
       fun {X Y} f ↦ Pointed.Hom.ext _ _ <| funext fun a ↦ by
         obtain _ | ⟨a, ha⟩ := a
-        exact f.map_point.symm
+        · exact f.map_point.symm
         classical
         simp [Option.casesOn'_eq_elim, -Option.elim,
           @Part.elim_toOption _ _ _ (Classical.propDecidable _), ha]
diff --git a/Mathlib/CategoryTheory/Category/RelCat.lean b/Mathlib/CategoryTheory/Category/RelCat.lean
index 6a7d3569fb68b4..e50236890bb848 100644
--- a/Mathlib/CategoryTheory/Category/RelCat.lean
+++ b/Mathlib/CategoryTheory/Category/RelCat.lean
@@ -145,7 +145,6 @@ def unopFunctor : RelCatᵒᵖ ⥤ RelCat where
   obj X := unop X
   map {X Y} r x y := unop r y x
   map_id X := by
-    congr
     dsimp
     ext x y
     exact Eq.comm
diff --git a/Mathlib/CategoryTheory/Category/TwoP.lean b/Mathlib/CategoryTheory/Category/TwoP.lean
index 7c98b17d957b49..c69d3de3be4bb2 100644
--- a/Mathlib/CategoryTheory/Category/TwoP.lean
+++ b/Mathlib/CategoryTheory/Category/TwoP.lean
@@ -164,8 +164,8 @@ noncomputable def pointedToTwoPFstForgetCompBipointedToPointedFstAdjunction :
             apply Bipointed.Hom.ext
             funext x
             cases x
-            exact f.map_snd.symm
-            rfl
+            · exact f.map_snd.symm
+            · rfl
           right_inv := fun f => Pointed.Hom.ext _ _ rfl }
       homEquiv_naturality_left_symm := fun f g => by
         apply Bipointed.Hom.ext
@@ -184,8 +184,8 @@ noncomputable def pointedToTwoPSndForgetCompBipointedToPointedSndAdjunction :
             apply Bipointed.Hom.ext
             funext x
             cases x
-            exact f.map_fst.symm
-            rfl
+            · exact f.map_fst.symm
+            · rfl
           right_inv := fun f => Pointed.Hom.ext _ _ rfl }
       homEquiv_naturality_left_symm := fun f g => by
         apply Bipointed.Hom.ext
diff --git a/Mathlib/CategoryTheory/Closed/Cartesian.lean b/Mathlib/CategoryTheory/Closed/Cartesian.lean
index e25e074b8aff13..2b4b97544d0fe2 100644
--- a/Mathlib/CategoryTheory/Closed/Cartesian.lean
+++ b/Mathlib/CategoryTheory/Closed/Cartesian.lean
@@ -361,13 +361,13 @@ def prodCoprodDistrib [HasBinaryCoproducts C] [CartesianClosed C] (X Y Z : C) :
       (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr))
   hom_inv_id := by
     ext
-    rw [coprod.inl_desc_assoc, comp_id, ← uncurry_natural_left, coprod.inl_desc, uncurry_curry]
+    · rw [coprod.inl_desc_assoc, comp_id, ← uncurry_natural_left, coprod.inl_desc, uncurry_curry]
     rw [coprod.inr_desc_assoc, comp_id, ← uncurry_natural_left, coprod.inr_desc, uncurry_curry]
   inv_hom_id := by
     rw [← uncurry_natural_right, ← eq_curry_iff]
     ext
-    rw [coprod.inl_desc_assoc, ← curry_natural_right, coprod.inl_desc, ← curry_natural_left,
-      comp_id]
+    · rw [coprod.inl_desc_assoc, ← curry_natural_right, coprod.inl_desc, ← curry_natural_left,
+        comp_id]
     rw [coprod.inr_desc_assoc, ← curry_natural_right, coprod.inr_desc, ← curry_natural_left,
       comp_id]
 #align category_theory.prod_coprod_distrib CategoryTheory.prodCoprodDistrib
diff --git a/Mathlib/CategoryTheory/Functor/Flat.lean b/Mathlib/CategoryTheory/Functor/Flat.lean
index 04f66b1b913bbb..dfe6d5aa51de7d 100644
--- a/Mathlib/CategoryTheory/Functor/Flat.lean
+++ b/Mathlib/CategoryTheory/Functor/Flat.lean
@@ -200,8 +200,8 @@ noncomputable def preservesFiniteLimitsOfFlat (F : C ⥤ D) [RepresentablyFlat F
       fac := PreservesFiniteLimitsOfFlat.fac F hc
       uniq := fun s m h => by
         apply PreservesFiniteLimitsOfFlat.uniq F hc
-        exact h
-        exact PreservesFiniteLimitsOfFlat.fac F hc s }
+        · exact h
+        · exact PreservesFiniteLimitsOfFlat.fac F hc s }
 #align category_theory.preserves_finite_limits_of_flat CategoryTheory.preservesFiniteLimitsOfFlat
 
 /-- If `C` is finitely cocomplete, then `F : C ⥤ D` is representably flat iff it preserves
diff --git a/Mathlib/CategoryTheory/Galois/GaloisObjects.lean b/Mathlib/CategoryTheory/Galois/GaloisObjects.lean
index 20f39f764653d4..8e2f74f4b1df17 100644
--- a/Mathlib/CategoryTheory/Galois/GaloisObjects.lean
+++ b/Mathlib/CategoryTheory/Galois/GaloisObjects.lean
@@ -68,8 +68,8 @@ noncomputable def quotientByAutTerminalEquivUniqueQuotient
     preservesColimitIso (F ⋙ FintypeCat.incl) J ≪≫
     (Equiv.toIso <| SingleObj.Types.colimitEquivQuotient (J ⋙ F ⋙ FintypeCat.incl))
   apply Equiv.trans
-  apply (IsTerminal.isTerminalIffObj (F ⋙ FintypeCat.incl) _).trans
-    (isLimitEmptyConeEquiv _ (asEmptyCone _) (asEmptyCone _) e)
+  · apply (IsTerminal.isTerminalIffObj (F ⋙ FintypeCat.incl) _).trans
+      (isLimitEmptyConeEquiv _ (asEmptyCone _) (asEmptyCone _) e)
   exact Types.isTerminalEquivUnique _
 
 lemma isGalois_iff_aux (X : C) [IsConnected X] :
diff --git a/Mathlib/CategoryTheory/Limits/Over.lean b/Mathlib/CategoryTheory/Limits/Over.lean
index 7711bad009ad43..4d8af86f7b3e66 100644
--- a/Mathlib/CategoryTheory/Limits/Over.lean
+++ b/Mathlib/CategoryTheory/Limits/Over.lean
@@ -110,7 +110,7 @@ def mapPullbackAdj {A B : C} (f : A ⟶ B) : Over.map f ⊣ pullback f :=
             Over.homMk (pullback.lift X.left g.hom (Over.w X)) (pullback.lift_snd _ _ _)
           invFun := fun Y => by
             refine' Over.homMk _ _
-            refine' Y.left ≫ pullback.fst
+            · refine' Y.left ≫ pullback.fst
             dsimp
             rw [← Over.w Y, Category.assoc, pullback.condition, Category.assoc]; rfl
           left_inv := fun X => by
diff --git a/Mathlib/CategoryTheory/Limits/VanKampen.lean b/Mathlib/CategoryTheory/Limits/VanKampen.lean
index 143536dd6b7e6b..458548946fd99b 100644
--- a/Mathlib/CategoryTheory/Limits/VanKampen.lean
+++ b/Mathlib/CategoryTheory/Limits/VanKampen.lean
@@ -359,7 +359,7 @@ theorem IsUniversalColimit.map_reflective
         exact c.w _
   let cf : (Cocones.precompose β.hom).obj c' ⟶ Gl.mapCocone c'' := by
     refine { hom := pullback.lift ?_ f ?_ ≫ (PreservesPullback.iso _ _ _).inv, w := ?_ }
-    exact inv <| adj.counit.app c'.pt
+    · exact inv <| adj.counit.app c'.pt
     · rw [IsIso.inv_comp_eq, ← adj.counit_naturality_assoc f, ← cancel_mono (adj.counit.app <|
         Gl.obj c.pt), Category.assoc, Category.assoc, adj.left_triangle_components]
       erw [Category.comp_id]
@@ -456,10 +456,10 @@ theorem IsVanKampenColimit.map_reflective [HasColimitsOfShape J C]
   have := ((H (colimit.cocone <| F' ⋙ Gr) (whiskerRight α' Gr)
     (colimit.desc _ ⟨_, whiskerRight α' Gr ≫ c.2⟩) ?_ (hα'.whiskerRight Gr)).mp
     ⟨(getColimitCocone <| F' ⋙ Gr).2⟩ j).map Gl
-  convert IsPullback.paste_vert _ this
-  refine IsPullback.of_vert_isIso ⟨?_⟩
-  rw [← IsIso.inv_comp_eq, ← Category.assoc, NatIso.inv_inv_app]
-  exact IsColimit.comp_coconePointUniqueUpToIso_hom hl hr _
+  · convert IsPullback.paste_vert _ this
+    refine IsPullback.of_vert_isIso ⟨?_⟩
+    rw [← IsIso.inv_comp_eq, ← Category.assoc, NatIso.inv_inv_app]
+    exact IsColimit.comp_coconePointUniqueUpToIso_hom hl hr _
   · clear_value α'
     ext j
     simp
diff --git a/Mathlib/CategoryTheory/Localization/Predicate.lean b/Mathlib/CategoryTheory/Localization/Predicate.lean
index 403bc4c27ff50d..fdb3448de144e1 100644
--- a/Mathlib/CategoryTheory/Localization/Predicate.lean
+++ b/Mathlib/CategoryTheory/Localization/Predicate.lean
@@ -246,13 +246,13 @@ theorem whiskeringLeftFunctor'_obj (F : D ⥤ E) : (whiskeringLeftFunctor' L W E
 instance : (whiskeringLeftFunctor' L W E).Full := by
   rw [whiskeringLeftFunctor'_eq]
   apply @Functor.Full.comp _ _ _ _ _ _ _ _ ?_ ?_
-  infer_instance
+  · infer_instance
   apply InducedCategory.full -- why is it not found automatically ???
 
 instance : (whiskeringLeftFunctor' L W E).Faithful := by
   rw [whiskeringLeftFunctor'_eq]
   apply @Functor.Faithful.comp _ _ _ _ _ _ _ _ ?_ ?_
-  infer_instance
+  · infer_instance
   apply InducedCategory.faithful -- why is it not found automatically ???
 
 lemma full_whiskeringLeft : ((whiskeringLeft C D E).obj L).Full :=
diff --git a/Mathlib/CategoryTheory/Monad/Coequalizer.lean b/Mathlib/CategoryTheory/Monad/Coequalizer.lean
index 809d99ee36c582..96cb69e0a4a492 100644
--- a/Mathlib/CategoryTheory/Monad/Coequalizer.lean
+++ b/Mathlib/CategoryTheory/Monad/Coequalizer.lean
@@ -66,7 +66,7 @@ theorem FreeCoequalizer.condition :
 
 instance : IsReflexivePair (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X) := by
   apply IsReflexivePair.mk' _ _ _
-  apply (free T).map (T.η.app X.A)
+  · apply (free T).map (T.η.app X.A)
   · ext
     dsimp
     rw [← Functor.map_comp, X.unit, Functor.map_id]
diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean
index 1f92ed000fbae8..8f5814174e77fb 100644
--- a/Mathlib/CategoryTheory/Pi/Basic.lean
+++ b/Mathlib/CategoryTheory/Pi/Basic.lean
@@ -236,8 +236,8 @@ end EqToHom
 @[simp]
 theorem pi'_eval (f : ∀ i, A ⥤ C i) (i : I) : pi' f ⋙ Pi.eval C i = f i := by
   apply Functor.ext
-  intro _ _ _
-  · simp
+  · intro _ _ _
+    simp
   · intro _
     rfl
 #align category_theory.functor.pi'_eval CategoryTheory.Functor.pi'_eval
diff --git a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
index 8acbfa849b19cb..ba156154181fec 100644
--- a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
+++ b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
@@ -324,7 +324,7 @@ noncomputable def sheafCoyonedaHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) :
         f.unop ≫ appHom (homOver α (unop X)) (unop U) x
     symm
     apply sheaf_eq_amalgamation
-    apply G.is_cover_of_isCoverDense
+    · apply G.is_cover_of_isCoverDense
     -- Porting note: the following line closes a goal which didn't exist before reenableeta
     · exact pushforwardFamily_compatible (homOver α Y.unop) (f.unop ≫ x)
     intro Y' f' hf'
diff --git a/Mathlib/CategoryTheory/Sites/InducedTopology.lean b/Mathlib/CategoryTheory/Sites/InducedTopology.lean
index 10add06579dcd5..6c45dd89bf395d 100644
--- a/Mathlib/CategoryTheory/Sites/InducedTopology.lean
+++ b/Mathlib/CategoryTheory/Sites/InducedTopology.lean
@@ -117,8 +117,8 @@ theorem Functor.locallyCoverDense_of_isCoverDense [Full G] [G.IsCoverDense K] :
   rintro Y _ ⟨Z, _, f, hf, ⟨W, g, f', rfl : _ = _⟩, rfl⟩
   use W; use G.preimage (f' ≫ f); use g
   constructor
-  simpa using T.val.downward_closed hf f'
-  simp
+  · simpa using T.val.downward_closed hf f'
+  · simp
 #align category_theory.cover_dense.locally_cover_dense CategoryTheory.Functor.locallyCoverDense_of_isCoverDense
 
 /-- Given a fully faithful cover-dense functor `G : C ⥤ (D, K)`, we may induce a topology on `C`.
diff --git a/Mathlib/CategoryTheory/Subobject/Lattice.lean b/Mathlib/CategoryTheory/Subobject/Lattice.lean
index 5bf2ae855f7128..e118870de48388 100644
--- a/Mathlib/CategoryTheory/Subobject/Lattice.lean
+++ b/Mathlib/CategoryTheory/Subobject/Lattice.lean
@@ -146,8 +146,8 @@ def inf {A : C} : MonoOver A ⥤ MonoOver A ⥤ MonoOver A where
   map k :=
     { app := fun g => by
         apply homMk _ _
-        apply pullback.lift pullback.fst (pullback.snd ≫ k.left) _
-        rw [pullback.condition, assoc, w k]
+        · apply pullback.lift pullback.fst (pullback.snd ≫ k.left) _
+          rw [pullback.condition, assoc, w k]
         dsimp
         rw [pullback.lift_snd_assoc, assoc, w k] }
 #align category_theory.mono_over.inf CategoryTheory.MonoOver.inf
@@ -166,8 +166,8 @@ def infLERight {A : C} (f g : MonoOver A) : (inf.obj f).obj g ⟶ g :=
 def leInf {A : C} (f g h : MonoOver A) : (h ⟶ f) → (h ⟶ g) → (h ⟶ (inf.obj f).obj g) := by
   intro k₁ k₂
   refine' homMk (pullback.lift k₂.left k₁.left _) _
-  rw [w k₁, w k₂]
-  erw [pullback.lift_snd_assoc, w k₁]
+  · rw [w k₁, w k₂]
+  · erw [pullback.lift_snd_assoc, w k₁]
 #align category_theory.mono_over.le_inf CategoryTheory.MonoOver.leInf
 
 end Inf
@@ -201,8 +201,8 @@ def leSupRight {A : C} (f g : MonoOver A) : g ⟶ (sup.obj f).obj g := by
 def supLe {A : C} (f g h : MonoOver A) : (f ⟶ h) → (g ⟶ h) → ((sup.obj f).obj g ⟶ h) := by
   intro k₁ k₂
   refine' homMk _ _
-  apply image.lift ⟨_, h.arrow, coprod.desc k₁.left k₂.left, _⟩
-  · ext
+  · apply image.lift ⟨_, h.arrow, coprod.desc k₁.left k₂.left, _⟩
+    ext
     · simp [w k₁]
     · simp [w k₂]
   · apply image.lift_fac
diff --git a/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean b/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
index 7fee3853cf91ae..1f00237a4bda63 100644
--- a/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
+++ b/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
@@ -195,7 +195,8 @@ theorem card_add_nsmul_le {α : Type*} [AddCommGroup α] [DecidableEq α] {A B :
   · simp
   rw [succ_nsmul', ← add_assoc, _root_.pow_succ', mul_assoc, ← mul_div_right_comm, le_div_iff,
     ← cast_mul]
-  swap; exact cast_pos.2 hA.card_pos
+  swap
+  · exact cast_pos.2 hA.card_pos
   refine' (cast_le.2 <| add_pluennecke_petridis _ hAB).trans _
   rw [cast_mul]
   gcongr
@@ -210,7 +211,8 @@ theorem card_mul_pow_le (hAB : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B)
   · simp
   rw [_root_.pow_succ', ← mul_assoc, _root_.pow_succ', @mul_assoc ℚ≥0, ← mul_div_right_comm,
     le_div_iff, ← cast_mul]
-  swap; exact cast_pos.2 hA.card_pos
+  swap
+  · exact cast_pos.2 hA.card_pos
   refine' (cast_le.2 <| mul_pluennecke_petridis _ hAB).trans _
   rw [cast_mul]
   gcongr
diff --git a/Mathlib/Combinatorics/HalesJewett.lean b/Mathlib/Combinatorics/HalesJewett.lean
index 7a872c31598597..c9a0ad2fd807e6 100644
--- a/Mathlib/Combinatorics/HalesJewett.lean
+++ b/Mathlib/Combinatorics/HalesJewett.lean
@@ -300,8 +300,8 @@ private theorem exists_mono_in_high_dimension' :
     · obtain ⟨p, p_mem, hp⟩ := h
       refine' Or.inr (mono_of_mono ⟨p.line, p.color, _⟩)
       rintro (_ | _)
-      rw [hp, s.is_focused p p_mem]
-      apply p.has_color
+      · rw [hp, s.is_focused p p_mem]
+      · apply p.has_color
     -- If not, we get `r+1` color focused lines by taking the product of the `r` lines with `l'`
     -- and adding to this the vertical line obtained by the focus point and `l`.
     refine' Or.inl ⟨⟨(s.lines.map _).cons ⟨(l'.map some).vertical s.focus, C' s.focus, fun x => _⟩,
diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
index d68bfbda945e7c..896bae1b79f810 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
@@ -131,7 +131,7 @@ private theorem one_sub_eps_mul_card_nonuniformWitness_le_card_star (hV : V ∈
   have : (↑2 ^ P.parts.card : ℝ) * m / (U.card * ε) ≤ ε / 10 := by
     rw [← div_div, div_le_iff']
     swap
-    sz_positivity
+    · sz_positivity
     refine' le_of_mul_le_mul_left _ (pow_pos zero_lt_two P.parts.card)
     calc
       ↑2 ^ P.parts.card * ((↑2 ^ P.parts.card * m : ℝ) / U.card) =
@@ -163,9 +163,9 @@ private theorem one_sub_eps_mul_card_nonuniformWitness_le_card_star (hV : V ∈
       have : (2 : ℝ) ^ P.parts.card = ↑2 ^ (P.parts.card - 1) * 2 := by
         rw [← _root_.pow_succ, tsub_add_cancel_of_le (succ_le_iff.2 hP₁)]
       rw [← mul_div_right_comm, this, mul_right_comm _ (2 : ℝ), mul_assoc, le_div_iff]
-      refine' mul_le_mul_of_nonneg_left _ (by positivity)
-      exact (G.le_card_nonuniformWitness hunif).trans
-        (le_mul_of_one_le_left (cast_nonneg _) one_le_two)
+      · refine' mul_le_mul_of_nonneg_left _ (by positivity)
+        exact (G.le_card_nonuniformWitness hunif).trans
+          (le_mul_of_one_le_left (cast_nonneg _) one_le_two)
       have := Finset.card_pos.mpr (P.nonempty_of_mem_parts hU)
       sz_positivity
     _ ≤ ((star hP G ε hU V).biUnion id).card := by
@@ -232,9 +232,9 @@ private theorem one_sub_le_m_div_m_add_one_sq [Nonempty α]
   refine' le_trans _ (le_add_of_nonneg_right <| sq_nonneg _)
   rw [sub_le_sub_iff_left, ← le_div_iff' (show (0 : ℝ) < 2 by norm_num), div_div,
     one_div_le coe_m_add_one_pos, one_div_div]
-  refine' le_trans _ (le_add_of_nonneg_right zero_le_one)
-  set_option tactic.skipAssignedInstances false in norm_num
-  apply hundred_div_ε_pow_five_le_m hPα hPε
+  · refine' le_trans _ (le_add_of_nonneg_right zero_le_one)
+    set_option tactic.skipAssignedInstances false in norm_num
+    apply hundred_div_ε_pow_five_le_m hPα hPε
   sz_positivity
 
 private theorem m_add_one_div_m_le_one_add [Nonempty α]
@@ -285,9 +285,9 @@ private theorem density_sub_eps_le_sum_density_div_card [Nonempty α]
     · exact mod_cast _root_.zero_le _
     rw [sq, mul_mul_mul_comm, mul_comm ((m : ℝ) / _), mul_comm ((m : ℝ) / _)]
     refine' mul_le_mul _ _ _ (cast_nonneg _)
-    apply le_sum_card_subset_chunk_parts hA hx
-    apply le_sum_card_subset_chunk_parts hB hy
-    positivity
+    · apply le_sum_card_subset_chunk_parts hA hx
+    · apply le_sum_card_subset_chunk_parts hB hy
+    · positivity
   refine' mul_pos (mul_pos _ _) (mul_pos _ _) <;> rw [cast_pos, Finset.card_pos]
   exacts [⟨_, hx⟩, nonempty_of_mem_parts _ (hA hx), ⟨_, hy⟩, nonempty_of_mem_parts _ (hB hy)]
 
@@ -317,11 +317,11 @@ private theorem sum_density_div_card_le_density_add_eps [Nonempty α]
   rw [mul_mul_mul_comm, mul_comm (x.card : ℝ), mul_comm (y.card : ℝ), div_le_iff, mul_assoc]
   · refine' le_mul_of_one_le_right (cast_nonneg _) _
     rw [div_mul_eq_mul_div, one_le_div]
-    refine' le_trans _ (mul_le_mul_of_nonneg_right (m_add_one_div_m_le_one_add hPα hPε hε₁) _)
-    · rw [sq, mul_mul_mul_comm, mul_comm (_ / (m : ℝ)), mul_comm (_ / (m : ℝ))]
-      exact mul_le_mul (sum_card_subset_chunk_parts_le (by sz_positivity) hA hx)
-        (sum_card_subset_chunk_parts_le (by sz_positivity) hB hy) (by positivity) (by positivity)
-    · exact mod_cast _root_.zero_le _
+    · refine' le_trans _ (mul_le_mul_of_nonneg_right (m_add_one_div_m_le_one_add hPα hPε hε₁) _)
+      · rw [sq, mul_mul_mul_comm, mul_comm (_ / (m : ℝ)), mul_comm (_ / (m : ℝ))]
+        exact mul_le_mul (sum_card_subset_chunk_parts_le (by sz_positivity) hA hx)
+          (sum_card_subset_chunk_parts_le (by sz_positivity) hB hy) (by positivity) (by positivity)
+      · exact mod_cast _root_.zero_le _
     rw [← cast_mul, cast_pos]
     apply mul_pos <;> rw [Finset.card_pos, sup_eq_biUnion, biUnion_nonempty]
     · exact ⟨_, hx, nonempty_of_mem_parts _ (hA hx)⟩
@@ -464,8 +464,8 @@ private theorem edgeDensity_star_not_uniform [Nonempty α]
   rw [abs_sub_le_iff] at hrs hpr hqt
   rw [le_abs] at hst ⊢
   cases hst
-  left; linarith
-  right; linarith
+  · left; linarith
+  · right; linarith
 
 set_option tactic.skipAssignedInstances false in
 /-- Lower bound on the edge densities between non-uniform parts of `SzemerediRegularity.increment`.
@@ -516,8 +516,9 @@ theorem edgeDensity_chunk_not_uniform [Nonempty α] (hPα : P.parts.card * 16 ^
         exact edgeDensity_star_not_uniform hPα hPε hε₁ hUVne hUV
       · rw [sp, card_product]
         apply (edgeDensity_chunk_aux hPα hPε hU hV).trans
-        rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← mul_pow]
-        norm_num; rfl
+        · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← mul_pow]
+          · norm_num
+            rfl
 #align szemeredi_regularity.edge_density_chunk_not_uniform SzemerediRegularity.edgeDensity_chunk_not_uniform
 
 /-- Lower bound on the edge densities between parts of `SzemerediRegularity.increment`. This is the
diff --git a/Mathlib/Computability/Reduce.lean b/Mathlib/Computability/Reduce.lean
index 2f66c560058f0f..f667220d422e76 100644
--- a/Mathlib/Computability/Reduce.lean
+++ b/Mathlib/Computability/Reduce.lean
@@ -395,8 +395,8 @@ protected def liftOn₂ {φ} (d₁ d₂ : ManyOneDegree) (f : Set ℕ → Set 
       intro p₁ p₂ hp
       induction d₂ using ManyOneDegree.ind_on
       apply h
-      assumption
-      rfl)
+      · assumption
+      · rfl)
 #align many_one_degree.lift_on₂ ManyOneDegree.liftOn₂
 
 @[simp]
diff --git a/Mathlib/Data/Holor.lean b/Mathlib/Data/Holor.lean
index 3a3a61217d97e6..4d7ac2dc779f78 100644
--- a/Mathlib/Data/Holor.lean
+++ b/Mathlib/Data/Holor.lean
@@ -198,7 +198,7 @@ theorem mul_assoc0 [Semigroup α] (x : Holor α ds₁) (y : Holor α ds₂) (z :
     unfold mul
     rw [mul_assoc, ← HolorIndex.take_take, ← HolorIndex.drop_take, ← HolorIndex.drop_drop,
       cast_type]
-    rfl
+    · rfl
     rw [append_assoc]
 #align holor.mul_assoc0 Holor.mul_assoc0
 
diff --git a/Mathlib/Data/Nat/Multiplicity.lean b/Mathlib/Data/Nat/Multiplicity.lean
index 45d3127f429b68..4cedb5192c63b3 100644
--- a/Mathlib/Data/Nat/Multiplicity.lean
+++ b/Mathlib/Data/Nat/Multiplicity.lean
@@ -295,8 +295,8 @@ theorem multiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), multiplicit
       simp only [ne_eq, bit_eq_zero, true_and, Bool.not_eq_false] at h
       simp only [h, bit_true, bit1_zero, factorial, mul_one, Nat.isUnit_iff, cast_one]
       rw [Prime.multiplicity_one]
-      simp only [zero_lt_one]
-      decide
+      · simp only [zero_lt_one]
+      · decide
     have : multiplicity 2 (2 * n)! < (2 * n : ℕ) := by
       rw [prime_two.multiplicity_factorial_mul]
       refine' (PartENat.add_lt_add_right (ih hn) (PartENat.natCast_ne_top _)).trans_le _
diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean
index d9c55a22faa14e..8442e372b8c6be 100644
--- a/Mathlib/Data/Rat/Defs.lean
+++ b/Mathlib/Data/Rat/Defs.lean
@@ -385,7 +385,7 @@ instance commRing : CommRing ℚ where
   npow_succ n q := by
     dsimp
     rw [← q.mk'_num_den, mk'_pow, mk'_mul_mk']
-    congr
+    · congr
     · rw [mk'_pow, Int.natAbs_pow]
       exact q.reduced.pow_left _
     · rw [mk'_pow]
diff --git a/Mathlib/Data/Real/Cardinality.lean b/Mathlib/Data/Real/Cardinality.lean
index c54a4dafccbafd..968f330830448c 100644
--- a/Mathlib/Data/Real/Cardinality.lean
+++ b/Mathlib/Data/Real/Cardinality.lean
@@ -105,7 +105,8 @@ def cantorFunction (c : ℝ) (f : ℕ → Bool) : ℝ :=
 theorem cantorFunction_le (h1 : 0 ≤ c) (h2 : c < 1) (h3 : ∀ n, f n → g n) :
     cantorFunction c f ≤ cantorFunction c g := by
   apply tsum_le_tsum _ (summable_cantor_function f h1 h2) (summable_cantor_function g h1 h2)
-  intro n; cases h : f n; simp [h, cantorFunctionAux_nonneg h1]
+  intro n; cases h : f n
+  · simp [h, cantorFunctionAux_nonneg h1]
   replace h3 : g n = true := h3 n h; simp [h, h3]
 #align cardinal.cantor_function_le Cardinal.cantorFunction_le
 
@@ -130,14 +131,14 @@ theorem increasing_cantorFunction (h1 : 0 < c) (h2 : c < 1 / 2) {n : ℕ} {f g :
     have hf_max : ∀ n, f n → f_max n := by
       intro n hn
       cases n
-      rw [fn] at hn
-      contradiction
+      · rw [fn] at hn
+        contradiction
       apply rfl
     let g_min : ℕ → Bool := fun n => Nat.rec true (fun _ _ => false) n
     have hg_min : ∀ n, g_min n → g n := by
       intro n hn
       cases n
-      rw [gn]
+      · rw [gn]
       simp at hn
     apply (cantorFunction_le (le_of_lt h1) h3 hf_max).trans_lt
     refine' lt_of_lt_of_le _ (cantorFunction_le (le_of_lt h1) h3 hg_min)
@@ -153,7 +154,7 @@ theorem increasing_cantorFunction (h1 : 0 < c) (h2 : c < 1 / 2) {n : ℕ} {f g :
     · refine' (tsum_eq_single 0 _).trans _
       · intro n hn
         cases n
-        contradiction
+        · contradiction
         rfl
       · exact cantorFunctionAux_zero _
   rw [cantorFunction_succ f (le_of_lt h1) h3, cantorFunction_succ g (le_of_lt h1) h3]
@@ -204,10 +205,10 @@ theorem mk_real : #ℝ = 𝔠 := by
     apply (mk_subtype_le _).trans_eq
     rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
   · convert mk_le_of_injective (cantorFunction_injective _ _)
-    rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
-    exact 1 / 3
-    norm_num
-    norm_num
+    · rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
+    · exact 1 / 3
+    · norm_num
+    · norm_num
 #align cardinal.mk_real Cardinal.mk_real
 
 /-- The cardinality of the reals, as a set. -/
diff --git a/Mathlib/Data/Real/Hyperreal.lean b/Mathlib/Data/Real/Hyperreal.lean
index 96135c525ba9f1..9f0407c934368b 100644
--- a/Mathlib/Data/Real/Hyperreal.lean
+++ b/Mathlib/Data/Real/Hyperreal.lean
@@ -793,11 +793,11 @@ theorem IsSt.inv {x : ℝ*} {r : ℝ} (hi : ¬Infinitesimal x) (hr : IsSt x r) :
 
 theorem st_inv (x : ℝ*) : st x⁻¹ = (st x)⁻¹ := by
   by_cases h0 : x = 0
-  rw [h0, inv_zero, ← coe_zero, st_id_real, inv_zero]
+  · rw [h0, inv_zero, ← coe_zero, st_id_real, inv_zero]
   by_cases h1 : Infinitesimal x
-  rw [((infinitesimal_iff_infinite_inv h0).mp h1).st_eq, h1.st_eq, inv_zero]
+  · rw [((infinitesimal_iff_infinite_inv h0).mp h1).st_eq, h1.st_eq, inv_zero]
   by_cases h2 : Infinite x
-  rw [(infinitesimal_inv_of_infinite h2).st_eq, h2.st_eq, inv_zero]
+  · rw [(infinitesimal_inv_of_infinite h2).st_eq, h2.st_eq, inv_zero]
   exact ((isSt_st' h2).inv h1).st_eq
 #align hyperreal.st_inv Hyperreal.st_inv
 
diff --git a/Mathlib/Data/Real/Irrational.lean b/Mathlib/Data/Real/Irrational.lean
index 0c0475e8ad248d..ff52e79171f801 100644
--- a/Mathlib/Data/Real/Irrational.lean
+++ b/Mathlib/Data/Real/Irrational.lean
@@ -503,9 +503,9 @@ theorem one_lt_natDegree_of_irrational_root (hx : Irrational x) (p_nonzero : p 
   · obtain rfl : b = 0 := by simpa
     simp at p_nonzero
   · rw [mul_comm, ← eq_div_iff_mul_eq, eq_comm] at this
-    refine' hx ⟨-b / a, _⟩
-    assumption_mod_cast
-    assumption_mod_cast
+    · refine' hx ⟨-b / a, _⟩
+      assumption_mod_cast
+    · assumption_mod_cast
 #align one_lt_nat_degree_of_irrational_root one_lt_natDegree_of_irrational_root
 
 end Polynomial
diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean
index 27171948b87d58..bb8543374366fb 100644
--- a/Mathlib/Data/Set/Card.lean
+++ b/Mathlib/Data/Set/Card.lean
@@ -436,7 +436,9 @@ theorem Finite.exists_injOn_of_encard_le [Nonempty β] {s : Set α} {t : Set β}
     mem_image, ite_eq_left_iff, not_exists, not_and, not_forall, exists_prop, and_iff_right hbt]
 
   refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
-  · rintro x hx; split_ifs with h; assumption; exact (hf₀s x hx h).1
+  · rintro x hx; split_ifs with h
+    · assumption
+    · exact (hf₀s x hx h).1
   exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_noteq])
 termination_by encard s
 
diff --git a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
index b055590be4486e..a27e73f0538db2 100644
--- a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
+++ b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
@@ -917,8 +917,8 @@ theorem translationNumber_lt_of_forall_lt_add (hf : Continuous f) {z : ℝ} (hz
 theorem lt_translationNumber_of_forall_add_lt (hf : Continuous f) {z : ℝ} (hz : ∀ x, x + z < f x) :
     z < τ f := by
   obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f x - x ≤ f y - y
-  exact isCompact_Icc.exists_isMinOn (nonempty_Icc.2 zero_le_one)
-    (hf.sub continuous_id).continuousOn
+  · exact isCompact_Icc.exists_isMinOn (nonempty_Icc.2 zero_le_one)
+      (hf.sub continuous_id).continuousOn
   refine' lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) _
   apply le_translationNumber_of_add_le
   simp only [← le_sub_iff_add_le']
diff --git a/Mathlib/FieldTheory/Finite/Polynomial.lean b/Mathlib/FieldTheory/Finite/Polynomial.lean
index a86ade7187d217..e66ae9bd25dbf9 100644
--- a/Mathlib/FieldTheory/Finite/Polynomial.lean
+++ b/Mathlib/FieldTheory/Finite/Polynomial.lean
@@ -96,10 +96,10 @@ theorem indicator_mem_restrictDegree (c : σ → K) :
   simp_rw [← Multiset.coe_countAddMonoidHom, map_sum,
     AddMonoidHom.map_nsmul, Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
   trans
-  refine' Finset.sum_eq_single n _ _
-  · intro b _ ne
-    simp [Multiset.count_singleton, ne, if_neg (Ne.symm _)]
-  · intro h; exact (h <| Finset.mem_univ _).elim
+  · refine' Finset.sum_eq_single n _ _
+    · intro b _ ne
+      simp [Multiset.count_singleton, ne, if_neg (Ne.symm _)]
+    · intro h; exact (h <| Finset.mem_univ _).elim
   · rw [Multiset.count_singleton_self, mul_one]
 #align mv_polynomial.indicator_mem_restrict_degree MvPolynomial.indicator_mem_restrictDegree
 
diff --git a/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean b/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
index c04f67473ff834..a00e3c2b2ac404 100644
--- a/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
+++ b/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
@@ -80,11 +80,11 @@ theorem isIntegrallyClosed_dvd {s : S} (hs : IsIntegral R s) {p : R[X]}
   have := FractionRing.isScalarTower_liftAlgebra R L
   have : minpoly K (algebraMap S L s) ∣ map (algebraMap R K) (p %ₘ minpoly R s) := by
     rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]
-    refine' dvd_sub (minpoly.dvd K (algebraMap S L s) _) _
-    rw [← map_aeval_eq_aeval_map, hp, map_zero]
-    rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-    apply dvd_mul_of_dvd_left
-    rw [isIntegrallyClosed_eq_field_fractions K L hs]
+    · refine' dvd_sub (minpoly.dvd K (algebraMap S L s) _) _
+      · rw [← map_aeval_eq_aeval_map, hp, map_zero]
+        rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
+      apply dvd_mul_of_dvd_left
+      rw [isIntegrallyClosed_eq_field_fractions K L hs]
     exact Monic.map _ (minpoly.monic hs)
   rw [isIntegrallyClosed_eq_field_fractions _ _ hs,
     map_dvd_map (algebraMap R K) (IsFractionRing.injective R K) (minpoly.monic hs)] at this
diff --git a/Mathlib/FieldTheory/PerfectClosure.lean b/Mathlib/FieldTheory/PerfectClosure.lean
index 7098bc52d8ab6e..7da5a0d31d46fc 100644
--- a/Mathlib/FieldTheory/PerfectClosure.lean
+++ b/Mathlib/FieldTheory/PerfectClosure.lean
@@ -433,7 +433,8 @@ instance instPerfectRing : PerfectRing (PerfectClosure K p) p where
 @[simp]
 theorem iterate_frobenius_mk (n : ℕ) (x : K) :
     (frobenius (PerfectClosure K p) p)^[n] (mk K p ⟨n, x⟩) = of K p x := by
-  induction' n with n ih; rfl
+  induction' n with n ih
+  · rfl
   rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]
 
 /-- Given a ring `K` of characteristic `p` and a perfect ring `L` of the same characteristic,
diff --git a/Mathlib/FieldTheory/RatFunc.lean b/Mathlib/FieldTheory/RatFunc.lean
index 0c17f5929a6194..31eaa815c34615 100644
--- a/Mathlib/FieldTheory/RatFunc.lean
+++ b/Mathlib/FieldTheory/RatFunc.lean
@@ -609,8 +609,9 @@ def map [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap 
       fun {p q p' q'} hq hq' h => by
       beta_reduce -- Porting note(#12129): force the function to be applied
       rw [dif_pos, dif_pos]
-      congr 1 -- Porting note: this was a `rw [ofFractionRing.inj_eq]` which was overkill anyway
-      rw [Localization.mk_eq_mk_iff]
+      on_goal 1 =>
+        congr 1 -- Porting note: this was a `rw [ofFractionRing.inj_eq]` which was overkill anyway
+        rw [Localization.mk_eq_mk_iff]
       rotate_left
       · exact hφ hq
       · exact hφ hq'
@@ -626,14 +627,14 @@ def map [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap 
     cases' x with x; cases' y with y
     -- Porting note: added `using Localization.rec` (`Localization.induction_on` didn't work)
     induction' x using Localization.rec with p q
-    induction' y using Localization.rec with p' q'
-    · have hq : φ q ∈ S[X]⁰ := hφ q.prop
-      have hq' : φ q' ∈ S[X]⁰ := hφ q'.prop
-      have hqq' : φ ↑(q * q') ∈ S[X]⁰ := by simpa using Submonoid.mul_mem _ hq hq'
-      simp_rw [← ofFractionRing_mul, Localization.mk_mul, liftOn_ofFractionRing_mk, dif_pos hq,
-        dif_pos hq', dif_pos hqq', ← ofFractionRing_mul, Submonoid.coe_mul, map_mul,
-        Localization.mk_mul, Submonoid.mk_mul_mk]
-    · rfl
+    · induction' y using Localization.rec with p' q'
+      · have hq : φ q ∈ S[X]⁰ := hφ q.prop
+        have hq' : φ q' ∈ S[X]⁰ := hφ q'.prop
+        have hqq' : φ ↑(q * q') ∈ S[X]⁰ := by simpa using Submonoid.mul_mem _ hq hq'
+        simp_rw [← ofFractionRing_mul, Localization.mk_mul, liftOn_ofFractionRing_mk, dif_pos hq,
+          dif_pos hq', dif_pos hqq', ← ofFractionRing_mul, Submonoid.coe_mul, map_mul,
+          Localization.mk_mul, Submonoid.mk_mul_mk]
+      · rfl
     · rfl
 #align ratfunc.map RatFunc.map
 
@@ -707,10 +708,10 @@ def liftMonoidWithZeroHom (φ : R[X] →*₀ G₀) (hφ : R[X]⁰ ≤ G₀⁰.co
     cases' x with x
     cases' y with y
     induction' x using Localization.rec with p q
-    induction' y using Localization.rec with p' q'
-    · rw [← ofFractionRing_mul, Localization.mk_mul]
-      simp only [liftOn_ofFractionRing_mk, div_mul_div_comm, map_mul, Submonoid.coe_mul]
-    · rfl
+    · induction' y using Localization.rec with p' q'
+      · rw [← ofFractionRing_mul, Localization.mk_mul]
+        simp only [liftOn_ofFractionRing_mk, div_mul_div_comm, map_mul, Submonoid.coe_mul]
+      · rfl
     · rfl
   map_zero' := by
     beta_reduce -- Porting note(#12129): force the function to be applied
@@ -735,7 +736,7 @@ theorem liftMonoidWithZeroHom_injective [Nontrivial R] (φ : R[X] →*₀ G₀)
     congr 1
     refine Localization.mk_eq_mk_iff.mpr (Localization.r_of_eq (M := R[X]) ?_)
     have := mul_eq_mul_of_div_eq_div _ _ ?_ ?_ h
-    rwa [← map_mul, ← map_mul, hφ.eq_iff, mul_comm, mul_comm a'.fst] at this
+    · rwa [← map_mul, ← map_mul, hφ.eq_iff, mul_comm, mul_comm a'.fst] at this
     all_goals exact map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _)
 #align ratfunc.lift_monoid_with_zero_hom_injective RatFunc.liftMonoidWithZeroHom_injective
 
@@ -752,17 +753,17 @@ def liftRingHom (φ : R[X] →+* L) (hφ : R[X]⁰ ≤ L⁰.comap φ) : RatFunc
       cases' y with y
       -- Porting note: had to add the recursor explicitly below
       induction' x using Localization.rec with p q
-      induction' y using Localization.rec with p' q'
-      · rw [← ofFractionRing_add, Localization.add_mk]
-        simp only [RingHom.toMonoidWithZeroHom_eq_coe,
-          liftMonoidWithZeroHom_apply_ofFractionRing_mk]
-        rw [div_add_div, div_eq_div_iff]
-        · rw [mul_comm _ p, mul_comm _ p', mul_comm _ (φ p'), add_comm]
-          simp only [map_add, map_mul, Submonoid.coe_mul]
-        all_goals
-          try simp only [← map_mul, ← Submonoid.coe_mul]
-          exact nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _))
-      · rfl
+      · induction' y using Localization.rec with p' q'
+        · rw [← ofFractionRing_add, Localization.add_mk]
+          simp only [RingHom.toMonoidWithZeroHom_eq_coe,
+            liftMonoidWithZeroHom_apply_ofFractionRing_mk]
+          rw [div_add_div, div_eq_div_iff]
+          · rw [mul_comm _ p, mul_comm _ p', mul_comm _ (φ p'), add_comm]
+            simp only [map_add, map_mul, Submonoid.coe_mul]
+          all_goals
+            try simp only [← map_mul, ← Submonoid.coe_mul]
+            exact nonZeroDivisors.ne_zero (hφ (SetLike.coe_mem _))
+        · rfl
       · rfl }
 #align ratfunc.lift_ring_hom RatFunc.liftRingHom
 
diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
index 469c8cef455502..71bc6fb62ceb90 100644
--- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
+++ b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
@@ -291,8 +291,8 @@ instance ofRestrict {X : TopCat} (Y : PresheafedSpace C) {f : X ⟶ Y.carrier}
     · -- Porting note: was `apply Subsingleton.helim; rw [this]`
       -- See https://github.com/leanprover/lean4/issues/2273
       congr
-      simp only [unop_op]
-      congr
+      · simp only [unop_op]
+        congr
       apply Subsingleton.helim
       rw [this]
     · infer_instance
@@ -1172,11 +1172,11 @@ theorem lift_range (H' : Set.range g.1.base ⊆ Set.range f.1.base) :
   rw [LocallyRingedSpace.comp_val, SheafedSpace.comp_base, ← this, ← Category.assoc, coe_comp]
   rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
   -- Porting note (#11224): change `rw` to `erw` on this lemma
-  erw [TopCat.pullback_fst_range]
-  ext
-  constructor
-  · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
-  · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
+  · erw [TopCat.pullback_fst_range]
+    ext
+    constructor
+    · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
+    · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
   · rw [← TopCat.epi_iff_surjective]
     rw [show (inv (pullback.snd : pullback f g ⟶ _)).val.base = _ from
         (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _).map_inv _]
diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
index a03cceedbae61f..c0858d5eba0f30 100644
--- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
+++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
@@ -145,7 +145,7 @@ theorem pullback_base (i j k : D.J) (S : Set (D.V (i, j)).carrier) :
   -- Porting note: `rw` to `erw` on `coe_comp`
   erw [coe_comp]
   rw [Set.preimage_comp, Set.image_preimage_eq, TopCat.pullback_snd_image_fst_preimage]
-  rfl
+  · rfl
   rw [← TopCat.epi_iff_surjective]
   infer_instance
 #align algebraic_geometry.PresheafedSpace.glue_data.pullback_base AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base
@@ -218,8 +218,8 @@ theorem snd_invApp_t_app' (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)
     simp_rw [Category.assoc]
     erw [IsOpenImmersion.inv_naturality, IsOpenImmersion.inv_naturality_assoc,
       IsOpenImmersion.app_inv_app'_assoc]
-    simp_rw [← (𝖣.V (k, i)).presheaf.map_comp, eqToHom_map (Functor.op _), eqToHom_op,
-      eqToHom_trans]
+    · simp_rw [← (𝖣.V (k, i)).presheaf.map_comp, eqToHom_map (Functor.op _), eqToHom_op,
+        eqToHom_trans]
     rintro x ⟨y, -, eq⟩
     replace eq := ConcreteCategory.congr_arg (𝖣.t i k).base eq
     change ((π₂ i, j, k) ≫ D.t i k).base y = (D.t k i ≫ D.t i k).base x at eq
@@ -290,16 +290,16 @@ theorem opensImagePreimageMap_app' (i j k : D.J) (U : Opens (D.U i).carrier) :
         ((π₁ j, i, k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
           (π₂⁻¹ j, i, k) (unop _) ≫ (D.V (j, k)).presheaf.map (eqToHom eq) := by
   constructor
-  delta opensImagePreimageMap
-  simp_rw [Category.assoc]
-  rw [(D.f j k).c.naturality, f_invApp_f_app_assoc]
-  erw [← (D.V (j, k)).presheaf.map_comp]
-  simp_rw [← Category.assoc]
-  erw [← comp_c_app, ← comp_c_app]
-  simp_rw [Category.assoc]
-  dsimp only [Functor.op, unop_op, Quiver.Hom.unop_op]
-  rw [eqToHom_map (Opens.map _), eqToHom_op, eqToHom_trans]
-  congr
+  · delta opensImagePreimageMap
+    simp_rw [Category.assoc]
+    rw [(D.f j k).c.naturality, f_invApp_f_app_assoc]
+    · erw [← (D.V (j, k)).presheaf.map_comp]
+      · simp_rw [← Category.assoc]
+        erw [← comp_c_app, ← comp_c_app]
+        · simp_rw [Category.assoc]
+          dsimp only [Functor.op, unop_op, Quiver.Hom.unop_op]
+          rw [eqToHom_map (Opens.map _), eqToHom_op, eqToHom_trans]
+          congr
 #align algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app' AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app'
 
 /-- The red and the blue arrows in ![this diagram](https://i.imgur.com/mBzV1Rx.png) commute. -/
@@ -464,8 +464,8 @@ theorem π_ιInvApp_π (i j : D.J) (U : Opens (D.U i).carrier) :
     change Mono ((_ ≫ D.f j i).c.app _)
     rw [comp_c_app]
     apply (config := { allowSynthFailures := true }) mono_comp
-    erw [D.ι_image_preimage_eq i j U]
-    · infer_instance
+    · erw [D.ι_image_preimage_eq i j U]
+      infer_instance
     · have : IsIso (D.t i j).c := by apply c_isIso_of_iso
       infer_instance)]
   simp_rw [Category.assoc]
diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean
index 376b38c6b96341..d1943c9cf413db 100644
--- a/Mathlib/GroupTheory/GroupAction/Quotient.lean
+++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean
@@ -359,8 +359,8 @@ theorem ConjClasses.card_carrier {G : Type*} [Group G] [Fintype G] (g : G)
   classical
   rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
   rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
-  simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
-  exact Fintype.card_pos_iff.mpr inferInstance
+  · simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
+  · exact Fintype.card_pos_iff.mpr inferInstance
 
 namespace Subgroup