chore: uncdot various files (#12422)

These `·` are scoping when there is a single active goal.

These were found using a modification of the linter at #12339.

Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

@@ -125,10 +125,10 @@ theorem lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable (x : V →
     Matrix.toLinearMap₂' (G.lapMatrix ℝ) x x = 0 ↔ ∀ i j : V, G.Reachable i j → x i = x j := by
   rw [lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]
   refine ⟨?_, fun h i j hA ↦ h i j hA.reachable⟩
-  · intro h i j ⟨w⟩
-    induction' w with w i j _ hA _ h'
-    · rfl
-    · exact (h i j hA).trans h'
+  intro h i j ⟨w⟩
+  induction' w with w i j _ hA _ h'
+  · rfl
+  · exact (h i j hA).trans h'
 
 theorem lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable (x : V → ℝ) :
     Matrix.toLin' (G.lapMatrix ℝ) x = 0 ↔ ∀ i j : V, G.Reachable i j → x i = x j := by

Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean

@@ -333,28 +333,28 @@ protected lemma GrowsPolynomially.mul {f g : ℝ → ℝ} (hf : GrowsPolynomiall
           simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]
         simp only [iff_eventuallyEq hmain, neg_mul]
         exact this
-  · intro b hb
-    have hf := hf.abs b hb
-    have hg := hg.abs b hb
-    obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf
-    obtain ⟨c₃, hc₃_mem, c₄, hc₄_mem, hg⟩ := hg
-    refine ⟨c₁ * c₃, by show 0 < c₁ * c₃; positivity, ?_⟩
-    refine ⟨c₂ * c₄, by show 0 < c₂ * c₄; positivity, ?_⟩
-    filter_upwards [hf, hg] with x hf hg
-    intro u hu
-    refine ⟨?lb, ?ub⟩
-    case lb => calc
-      c₁ * c₃ * (|f x| * |g x|) = (c₁ * |f x|) * (c₃ * |g x|) := by ring
-      _ ≤ |f u| * |g u| := by
-             gcongr
-             · exact (hf u hu).1
-             · exact (hg u hu).1
-    case ub => calc
-      |f u| * |g u| ≤ (c₂ * |f x|) * (c₄ * |g x|) := by
-             gcongr
-             · exact (hf u hu).2
-             · exact (hg u hu).2
-      _ = c₂ * c₄ * (|f x| * |g x|) := by ring
+  intro b hb
+  have hf := hf.abs b hb
+  have hg := hg.abs b hb
+  obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf
+  obtain ⟨c₃, hc₃_mem, c₄, hc₄_mem, hg⟩ := hg
+  refine ⟨c₁ * c₃, by show 0 < c₁ * c₃; positivity, ?_⟩
+  refine ⟨c₂ * c₄, by show 0 < c₂ * c₄; positivity, ?_⟩
+  filter_upwards [hf, hg] with x hf hg
+  intro u hu
+  refine ⟨?lb, ?ub⟩
+  case lb => calc
+    c₁ * c₃ * (|f x| * |g x|) = (c₁ * |f x|) * (c₃ * |g x|) := by ring
+    _ ≤ |f u| * |g u| := by
+           gcongr
+           · exact (hf u hu).1
+           · exact (hg u hu).1
+  case ub => calc
+    |f u| * |g u| ≤ (c₂ * |f x|) * (c₄ * |g x|) := by
+           gcongr
+           · exact (hf u hu).2
+           · exact (hg u hu).2
+    _ = c₂ * c₄ * (|f x| * |g x|) := by ring
 
 lemma GrowsPolynomially.const_mul {f : ℝ → ℝ} {c : ℝ} (hf : GrowsPolynomially f) :
     GrowsPolynomially fun x => c * f x :=

Mathlib/Data/Complex/Exponential.lean

@@ -1282,8 +1282,8 @@ theorem sum_div_factorial_le {α : Type*} [LinearOrderedField α] (n j : ℕ) (h
     _ ≤ ∑ m in range (j - n), ((n.factorial : α) * (n.succ : α) ^ m)⁻¹ := by
       simp_rw [one_div]
       gcongr
-      · rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm]
-        exact Nat.factorial_mul_pow_le_factorial
+      rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm]
+      exact Nat.factorial_mul_pow_le_factorial
     _ = (n.factorial : α)⁻¹ * ∑ m in range (j - n), (n.succ : α)⁻¹ ^ m := by
       simp [mul_inv, ← mul_sum, ← sum_mul, mul_comm, inv_pow]
     _ = ((n.succ : α) - n.succ * (n.succ : α)⁻¹ ^ (j - n)) / (n.factorial * n) := by
@@ -1321,8 +1321,8 @@ theorem exp_bound {x : ℂ} (hx : abs x ≤ 1) {n : ℕ} (hn : 0 < n) :
     _ ≤ ∑ m in filter (fun k => n ≤ k) (range j), abs x ^ n * (1 / m.factorial) := by
       simp_rw [map_mul, map_pow, map_div₀, abs_natCast]
       gcongr
-      · rw [abv_pow abs]
-        exact pow_le_one _ (abs.nonneg _) hx
+      rw [abv_pow abs]
+      exact pow_le_one _ (abs.nonneg _) hx
     _ = abs x ^ n * ∑ m in (range j).filter fun k => n ≤ k, (1 / m.factorial : ℝ) := by
       simp [abs_mul, abv_pow abs, abs_div, ← mul_sum]
     _ ≤ abs x ^ n * (n.succ * (n.factorial * n : ℝ)⁻¹) := by
@@ -1351,19 +1351,19 @@ theorem exp_bound' {x : ℂ} {n : ℕ} (hx : abs x / n.succ ≤ 1 / 2) :
     _ = ∑ i : ℕ in range k, abs x ^ n / n.factorial * (abs x ^ i / (n.succ : ℝ) ^ i) := ?_
     _ ≤ abs x ^ n / ↑n.factorial * 2 := ?_
   · gcongr
-    · exact mod_cast Nat.factorial_mul_pow_le_factorial
+    exact mod_cast Nat.factorial_mul_pow_le_factorial
   · refine' Finset.sum_congr rfl fun _ _ => _
     simp only [pow_add, div_eq_inv_mul, mul_inv, mul_left_comm, mul_assoc]
   · rw [← mul_sum]
     gcongr
-    · simp_rw [← div_pow]
-      rw [geom_sum_eq, div_le_iff_of_neg]
-      · trans (-1 : ℝ)
-        · linarith
-        · simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]
-          positivity
-      · linarith
+    simp_rw [← div_pow]
+    rw [geom_sum_eq, div_le_iff_of_neg]
+    · trans (-1 : ℝ)
       · linarith
+      · simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]
+        positivity
+    · linarith
+    · linarith
 #align complex.exp_bound' Complex.exp_bound'
 
 theorem abs_exp_sub_one_le {x : ℂ} (hx : abs x ≤ 1) : abs (exp x - 1) ≤ 2 * abs x :=

Mathlib/Data/Finsupp/Multiset.lean

@@ -89,7 +89,7 @@ theorem prod_toMultiset [CommMonoid α] (f : α →₀ ℕ) :
   · intro a n f _ _ ih
     rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul,
       Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton]
-    · exact pow_zero a
+    exact pow_zero a
 #align finsupp.prod_to_multiset Finsupp.prod_toMultiset
 
 @[simp]

Mathlib/Data/Nat/Totient.lean

@@ -347,9 +347,9 @@ theorem totient_gcd_mul_totient_mul (a b : ℕ) : φ (a.gcd b) * φ (a * b) = φ
   rw [shuffle, shuffle]
   rotate_left
   repeat' apply prod_primeFactors_dvd
-  · simp only [prod_primeFactors_gcd_mul_prod_primeFactors_mul]
-    rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc]
-    exact mul_dvd_mul (prod_primeFactors_dvd a) (prod_primeFactors_dvd b)
+  simp only [prod_primeFactors_gcd_mul_prod_primeFactors_mul]
+  rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc]
+  exact mul_dvd_mul (prod_primeFactors_dvd a) (prod_primeFactors_dvd b)
 #align nat.totient_gcd_mul_totient_mul Nat.totient_gcd_mul_totient_mul
 
 theorem totient_super_multiplicative (a b : ℕ) : φ a * φ b ≤ φ (a * b) := by

Mathlib/FieldTheory/ChevalleyWarning.lean

@@ -93,10 +93,10 @@ theorem MvPolynomial.sum_eval_eq_zero (f : MvPolynomial σ K)
     _ = a ^ d i * ∏ j, x₀ j ^ d j := congr_arg _ (Fintype.prod_congr _ _ ?_)
     -- see below
     _ = (∏ j, x₀ j ^ d j) * a ^ d i := mul_comm _ _
-  · -- the remaining step of the calculation above
-    rintro ⟨j, hj⟩
-    show (e a : σ → K) j ^ d j = x₀ ⟨j, hj⟩ ^ d j
-    rw [Equiv.subtypeEquivCodomain_symm_apply_ne]
+  -- the remaining step of the calculation above
+  rintro ⟨j, hj⟩
+  show (e a : σ → K) j ^ d j = x₀ ⟨j, hj⟩ ^ d j
+  rw [Equiv.subtypeEquivCodomain_symm_apply_ne]
 #align mv_polynomial.sum_eval_eq_zero MvPolynomial.sum_eval_eq_zero
 
 variable [DecidableEq K] (p : ℕ) [CharP K p]

Mathlib/FieldTheory/Finite/Basic.lean

@@ -625,8 +625,8 @@ theorem unit_isSquare_iff (hF : ringChar F ≠ 2) (a : Fˣ) :
     · rintro ⟨y, rfl⟩
       rw [← pow_two, ← pow_mul, hodd]
       apply_fun Units.val using Units.ext
-      · push_cast
-        exact FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y)
+      push_cast
+      exact FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y)
     · subst a; intro h
       have key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2) := by
         rw [← pow_mul] at h

Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

@@ -142,10 +142,10 @@ theorem AdjoinMonic.isIntegral (z : AdjoinMonic k) : IsIntegral k z := by
     | h_C => exact isIntegral_algebraMap
     | h_add _ _ ha hb => exact (ha _ rfl).add (hb _ rfl)
     | h_X p f ih =>
-      · refine @IsIntegral.mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_
-        refine ⟨f, f.2.1, ?_⟩
-        erw [AdjoinMonic.algebraMap, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem]
-        exact le_maxIdeal k (Ideal.subset_span ⟨f, rfl⟩)
+      refine @IsIntegral.mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_
+      refine ⟨f, f.2.1, ?_⟩
+      erw [AdjoinMonic.algebraMap, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem]
+      exact le_maxIdeal k (Ideal.subset_span ⟨f, rfl⟩)
 #align algebraic_closure.adjoin_monic.is_integral AlgebraicClosure.AdjoinMonic.isIntegral
 
 theorem AdjoinMonic.exists_root {f : k[X]} (hfm : f.Monic) (hfi : Irreducible f) :

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -91,9 +91,9 @@ theorem exists_pow_nat_eq [IsAlgClosed k] (x : k) {n : ℕ} (hn : 0 < n) : ∃ z
     rw [degree_X_pow_sub_C hn x]
     exact ne_of_gt (WithBot.coe_lt_coe.2 hn)
   obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this
-  · use z
-    simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz
-    exact sub_eq_zero.1 hz
+  use z
+  simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz
+  exact sub_eq_zero.1 hz
 #align is_alg_closed.exists_pow_nat_eq IsAlgClosed.exists_pow_nat_eq
 
 theorem exists_eq_mul_self [IsAlgClosed k] (x : k) : ∃ z, x = z * z := by

Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

@@ -121,8 +121,8 @@ theorem map_polynomial_aeval_of_nonempty [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X]
     (hnon : (σ a).Nonempty) : σ (aeval a p) = (fun k => eval k p) '' σ a := by
   nontriviality A
   refine' Or.elim (le_or_gt (degree p) 0) (fun h => _) (map_polynomial_aeval_of_degree_pos a p)
-  · rw [eq_C_of_degree_le_zero h]
-    simp only [Set.image_congr, eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]
+  rw [eq_C_of_degree_le_zero h]
+  simp only [Set.image_congr, eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]
 #align spectrum.map_polynomial_aeval_of_nonempty spectrum.map_polynomial_aeval_of_nonempty
 
 /-- A specialization of `spectrum.subset_polynomial_aeval` to monic monomials for convenience. -/

Mathlib/FieldTheory/RatFunc.lean

@@ -731,13 +731,13 @@ theorem liftMonoidWithZeroHom_injective [Nontrivial R] (φ : R[X] →*₀ G₀)
   rintro ⟨x⟩ ⟨y⟩
   induction' x using Localization.induction_on with a
   induction' y using Localization.induction_on with a'
-  · simp_rw [liftMonoidWithZeroHom_apply_ofFractionRing_mk]
-    intro h
-    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
-    all_goals exact map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _)
+  simp_rw [liftMonoidWithZeroHom_apply_ofFractionRing_mk]
+  intro h
+  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
+  all_goals exact map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _)
 #align ratfunc.lift_monoid_with_zero_hom_injective RatFunc.liftMonoidWithZeroHom_injective
 
 /-- Lift an injective ring homomorphism `R[X] →+* L` to a `RatFunc R →+* L`
@@ -810,9 +810,9 @@ instance (R : Type*) [CommSemiring R] [Algebra R K[X]] : Algebra R (RatFunc K) w
   smul_def' c x := by
     induction' x using RatFunc.induction_on' with p q hq
       -- Porting note: the first `rw [...]` was not needed
-    · rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
-      rw [mk_one', ← mk_smul, mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ←
-        ofFractionRing_mul, IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]
+    rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
+    rw [mk_one', ← mk_smul, mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ←
+      ofFractionRing_mul, IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def]
   commutes' c x := mul_comm _ _
 
 variable {K}
@@ -1309,7 +1309,7 @@ theorem denom_dvd {x : RatFunc K} {q : K[X]} (hq : q ≠ 0) :
     obtain ⟨_hx, hp⟩ := mul_ne_zero_iff.mp hq
     use num x * p
     rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]
-    · exact algebraMap_ne_zero hp
+    exact algebraMap_ne_zero hp
   · rintro ⟨p, rfl⟩
     exact denom_div_dvd p q
 #align ratfunc.denom_dvd RatFunc.denom_dvd

Mathlib/Geometry/Euclidean/Sphere/Power.lean

@@ -104,9 +104,9 @@ theorem mul_dist_eq_mul_dist_of_cospherical {a b c d p : P} (h : Cospherical ({a
     dist a p * dist b p = dist c p * dist d p := by
   obtain ⟨q, r, h'⟩ := (cospherical_def {a, b, c, d}).mp h
   obtain ⟨ha, hb, hc, hd⟩ := h' a (by simp), h' b (by simp), h' c (by simp), h' d (by simp)
-  · rw [← hd] at hc
-    rw [← hb] at ha
-    rw [mul_dist_eq_abs_sub_sq_dist hapb ha, hb, mul_dist_eq_abs_sub_sq_dist hcpd hc, hd]
+  rw [← hd] at hc
+  rw [← hb] at ha
+  rw [mul_dist_eq_abs_sub_sq_dist hapb ha, hb, mul_dist_eq_abs_sub_sq_dist hcpd hc, hd]
 #align euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical
 
 /-- **Intersecting Chords Theorem**. -/

Mathlib/Geometry/Manifold/Instances/Sphere.lean

@@ -245,8 +245,8 @@ theorem stereo_left_inv (hv : ‖v‖ = 1) {x : sphere (0 : E) 1} (hx : (x : E)
   · simp [a, inner_add_right, inner_smul_right, hvy, real_inner_self_eq_norm_mul_norm, hv, mul_smul,
       mul_pow, Real.norm_eq_abs, sq_abs, norm_smul]
     -- Porting note: used to be simp only [split, add_comm] but get maxRec errors
-    · rw [split, add_comm]
-      ac_rfl
+    rw [split, add_comm]
+    ac_rfl
   -- Porting note: this branch did not exit in ml3
   · rw [split, add_comm]
     congr!

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

@@ -416,7 +416,7 @@ theorem mfderiv_prod_eq_add {f : M × M' → M''} {p : M × M'}
     mfderiv_snd, mfderiv_const, mfderiv_const]
   symm
   convert ContinuousLinearMap.comp_id <| mfderiv (.prod I I') I'' f (p.1, p.2)
-  · exact ContinuousLinearMap.coprod_inl_inr
+  exact ContinuousLinearMap.coprod_inl_inr
 #align mfderiv_prod_eq_add mfderiv_prod_eq_add
 
 end Prod

Mathlib/Geometry/RingedSpace/OpenImmersion.lean

@@ -116,12 +116,12 @@ noncomputable def isoRestrict : X ≅ Y.restrict H.base_open :=
     fapply NatIso.ofComponents
     · intro U
       refine' asIso (f.c.app (op (H.openFunctor.obj (unop U)))) ≪≫ X.presheaf.mapIso (eqToIso _)
-      · induction U using Opposite.rec' with | h U => ?_
-        cases U
-        dsimp only [IsOpenMap.functor, Functor.op, Opens.map]
-        congr 2
-        erw [Set.preimage_image_eq _ H.base_open.inj]
-        rfl
+      induction U using Opposite.rec' with | h U => ?_
+      cases U
+      dsimp only [IsOpenMap.functor, Functor.op, Opens.map]
+      congr 2
+      erw [Set.preimage_image_eq _ H.base_open.inj]
+      rfl
     · intro U V i
       simp only [CategoryTheory.eqToIso.hom, TopCat.Presheaf.pushforwardObj_map, Category.assoc,
         Functor.op_map, Iso.trans_hom, asIso_hom, Functor.mapIso_hom, ← X.presheaf.map_comp]
@@ -133,12 +133,12 @@ noncomputable def isoRestrict : X ≅ Y.restrict H.base_open :=
 theorem isoRestrict_hom_ofRestrict : H.isoRestrict.hom ≫ Y.ofRestrict _ = f := by
   -- Porting note: `ext` did not pick up `NatTrans.ext`
   refine PresheafedSpace.Hom.ext _ _ rfl <| NatTrans.ext _ _ <| funext fun x => ?_
-  · simp only [isoRestrict_hom_c_app, NatTrans.comp_app, eqToHom_refl,
-      ofRestrict_c_app, Category.assoc, whiskerRight_id']
-    erw [Category.comp_id, comp_c_app, f.c.naturality_assoc, ← X.presheaf.map_comp]
-    trans f.c.app x ≫ X.presheaf.map (𝟙 _)
-    · congr 1
-    · erw [X.presheaf.map_id, Category.comp_id]
+  simp only [isoRestrict_hom_c_app, NatTrans.comp_app, eqToHom_refl,
+    ofRestrict_c_app, Category.assoc, whiskerRight_id']
+  erw [Category.comp_id, comp_c_app, f.c.naturality_assoc, ← X.presheaf.map_comp]
+  trans f.c.app x ≫ X.presheaf.map (𝟙 _)
+  · congr 1
+  · erw [X.presheaf.map_id, Category.comp_id]
 #align algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict_hom_of_restrict AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict
 
 @[simp]

Mathlib/GroupTheory/HNNExtension.lean

@@ -566,10 +566,10 @@ theorem prod_smul_empty (w : NormalWord d) :
     erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1]
     ext <;> simp
     -- The next 4 were not needed before leanprover/lean4#2644
-    · erw [(d.compl _).equiv_snd_eq_inv_mul]
-      simp_rw [SetLike.coe_sort_coe]
-      erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1]
-      simp
+    erw [(d.compl _).equiv_snd_eq_inv_mul]
+    simp_rw [SetLike.coe_sort_coe]
+    erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1]
+    simp
 
 variable (d)
 /-- The equivalence between elements of the HNN extension and words in normal form. -/

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -250,8 +250,8 @@ instance [Fintype α] [DecidableEq α] (f : Perm α) : DecidableRel (SameCycle f
     ⟨fun ⟨n, _, hn⟩ => ⟨n, hn⟩, fun ⟨i, hi⟩ => ⟨(i % orderOf f).natAbs,
       List.mem_range.2 (Int.ofNat_lt.1 <| by
         rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ <| Int.natCast_ne_zero.2 (orderOf_pos _).ne')]
-        · refine' (Int.emod_lt _ <| Int.natCast_ne_zero_iff_pos.2 <| orderOf_pos _).trans_le _
-          simp [orderOf_le_card_univ]),
+        refine' (Int.emod_lt _ <| Int.natCast_ne_zero_iff_pos.2 <| orderOf_pos _).trans_le _
+        simp [orderOf_le_card_univ]),
       by
         rw [← zpow_natCast, Int.natAbs_of_nonneg (Int.emod_nonneg _ <|
           Int.natCast_ne_zero_iff_pos.2 <| orderOf_pos _), zpow_mod_orderOf, hi]⟩⟩

Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

@@ -409,8 +409,8 @@ def toCycle (f : Perm α) (hf : IsCycle f) : Cycle α :=
       intro x y _ s
       refine' heq_of_eq _
       split_ifs with hx hy hy <;> try rfl
-      · have hc : SameCycle f x y := IsCycle.sameCycle hf hx hy
-        exact Quotient.sound' hc.toList_isRotated)
+      have hc : SameCycle f x y := IsCycle.sameCycle hf hx hy
+      exact Quotient.sound' hc.toList_isRotated)
 #align equiv.perm.to_cycle Equiv.Perm.toCycle
 
 theorem toCycle_eq_toList (f : Perm α) (hf : IsCycle f) (x : α) (hx : f x ≠ x) :

Mathlib/GroupTheory/SchurZassenhaus.lean

@@ -216,7 +216,7 @@ private theorem step2 (K : Subgroup G) [K.Normal] (hK : K ≤ N) : K = ⊥ ∨ K
     intro hH'
     rw [comap_injective this hH', isComplement'_top_right, map_eq_bot_iff,
       QuotientGroup.ker_mk'] at hH
-    · exact h4.2 (le_antisymm hK hH)
+    exact h4.2 (le_antisymm hK hH)
 
 /-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
 private theorem step3 (K : Subgroup N) [(K.map N.subtype).Normal] : K = ⊥ ∨ K = ⊤ := by

Mathlib/GroupTheory/SpecificGroups/Dihedral.lean

@@ -199,7 +199,7 @@ theorem exponent : Monoid.exponent (DihedralGroup n) = lcm n 2 := by
     rintro (m | m)
     · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r]
       refine' Nat.dvd_trans ⟨gcd n m.val, _⟩ (dvd_lcm_left n 2)
-      · exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm
+      exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm
     · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_sr]
       exact dvd_lcm_right n 2
   · apply lcm_dvd

Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean

@@ -172,7 +172,7 @@ theorem monic_generator_eq_minpoly (a : A) (p : 𝕜[X]) (p_monic : p.Monic)
   · rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen
     rw [eq_comm]
     apply eq_of_monic_of_associated p_monic _ p_gen
-    · apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)
+    apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)
 #align polynomial.monic_generator_eq_minpoly Polynomial.monic_generator_eq_minpoly
 
 theorem span_minpoly_eq_annihilator {M} [AddCommGroup M] [Module 𝕜 M] (f : Module.End 𝕜 M) :

Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

@@ -119,8 +119,8 @@ theorem iSup_generalizedEigenspace_eq_top [IsAlgClosed K] [FiniteDimensional K V
     -- Since the dimensions of `ER` and `ES` add up to the dimension of `V`, it follows that the
     -- span of all generalized eigenvectors is all of `V`.
     show ⨆ (μ : K) (k : ℕ), f.generalizedEigenspace μ k = ⊤
-    · rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add h_disjoint]
-      apply sup_le hER hES
+    rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add h_disjoint]
+    apply sup_le hER hES
 #align module.End.supr_generalized_eigenspace_eq_top Module.End.iSup_generalizedEigenspace_eq_top
 
 end Module.End