style: fix many leading by's in mathlib (#35343)

grunweg · grunweg · commit 2b9cd2f09056 · 2026-02-15T14:33:50.000Z
Per the style guide, these should go on the preceding line. Inspired by #22727, and then searching for `:=\n\s*by ` in mathlib.
diff --git a/Mathlib/Algebra/FreeMonoid/Count.lean b/Mathlib/Algebra/FreeMonoid/Count.lean
@@ -58,8 +58,8 @@ theorem count_apply [DecidableEq α] (x : α) (l : FreeAddMonoid α) :
     count x l = Multiplicative.ofAdd (l.toList.count x) := rfl
 
 theorem count_of [DecidableEq α] (x y : α) :
-    count x (of y) = Pi.mulSingle (M := fun _ => Multiplicative ℕ) x (Multiplicative.ofAdd 1) y :=
-  by simp only [count, eq_comm, countP_of, ofAdd_zero, Pi.mulSingle_apply]
+    count x (of y) = Pi.mulSingle (M := fun _ ↦ Multiplicative ℕ) x (Multiplicative.ofAdd 1) y := by
+  simp [count, countP_of, Pi.mulSingle_apply]
 
 end FreeMonoid
 
diff --git a/Mathlib/Algebra/Group/Int/Defs.lean b/Mathlib/Algebra/Group/Int/Defs.lean
@@ -43,8 +43,7 @@ instance instAddCommGroup : AddCommGroup ℤ where
   nsmul := (· * ·)
   nsmul_zero := Int.zero_mul
   nsmul_succ n x :=
-    show (n + 1 : ℤ) * x = n * x + x
-    by rw [Int.add_mul, Int.one_mul]
+    show (n + 1 : ℤ) * x = n * x + x by rw [Int.add_mul, Int.one_mul]
   zsmul := (· * ·)
   zsmul_zero' := Int.zero_mul
   zsmul_succ' m n := by
diff --git a/Mathlib/Algebra/Group/Invertible/Basic.lean b/Mathlib/Algebra/Group/Invertible/Basic.lean
@@ -141,9 +141,9 @@ before applying this lemma. -/
 theorem map_invOf {R : Type*} {S : Type*} {F : Type*} [MulOneClass R] [Monoid S]
     [FunLike F R S] [MonoidHomClass F R S] (f : F) (r : R)
     [Invertible r] [ifr : Invertible (f r)] :
-    f (⅟r) = ⅟(f r) :=
+    f (⅟r) = ⅟(f r) := by
   have h : ifr = Invertible.map f r := Subsingleton.elim _ _
-  by subst h; rfl
+  subst h; rfl
 
 /-- If a function `f : R → S` has a left-inverse that is a monoid hom,
   then `r : R` is invertible if `f r` is.
diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean
@@ -600,8 +600,7 @@ lemma closure_prod_one (s : Set M) : closure (s ×ˢ ({1} : Set N)) = (closure s
   le_antisymm
     (closure_le.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, .rfl⟩)
     (prod_le_iff.2 ⟨
-      map_le_of_le_comap _ <| closure_le.2 fun _x hx => subset_closure ⟨hx, rfl⟩,
-      by simp⟩)
+      map_le_of_le_comap _ <| closure_le.2 fun _x hx => subset_closure ⟨hx, rfl⟩, by simp⟩)
 
 @[to_additive (attr := simp) closure_zero_prod]
 lemma closure_one_prod (t : Set N) : closure (({1} : Set M) ×ˢ t) = .prod ⊥ (closure t) :=
diff --git a/Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean b/Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
@@ -208,8 +208,7 @@ lemma acyclic_truncGE_iff_isSupportedOutside :
     (K.truncGE e).Acyclic ↔ K.IsSupportedOutside e := by
   constructor
   · intro hK
-    exact ⟨fun i =>
-      by simpa only [exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK (e.f i)⟩
+    exact ⟨fun i ↦ by simpa only [exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK (e.f i)⟩
   · intro hK i'
     by_cases hi' : ∃ i, e.f i = i'
     · obtain ⟨i, rfl⟩ := hi'
diff --git a/Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean b/Mathlib/Algebra/Homology/Embedding/TruncLEHomology.lean
@@ -155,8 +155,7 @@ lemma shortComplexTruncLE_X₃_isSupportedOutside :
         dsimp [shortComplexTruncLE]
         rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]
       · simp
-    · have : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i)) :=
-        by dsimp; infer_instance
+    · have : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i)) := by dsimp; infer_instance
       rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
         comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
         comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]
diff --git a/Mathlib/Algebra/Module/LocalizedModule/Submodule.lean b/Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
@@ -286,7 +286,7 @@ instance IsLocalizedModule.toLocalizedQuotient' (M' : Submodule R M) :
     IsLocalizedModule p (M'.toLocalizedQuotient' S p f) where
   map_units x := by
     refine (Module.End.isUnit_iff _).mpr ⟨fun m n e ↦ ?_, fun m ↦ ⟨(IsLocalization.mk' S 1 x) • m,
-        by rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]⟩⟩
+      by rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]⟩⟩
     obtain ⟨⟨m, rfl⟩, n, rfl⟩ := PProd.mk (mk_surjective _ m) (mk_surjective _ n)
     simp only [Module.algebraMap_end_apply, ← mk_smul, Submodule.Quotient.eq, ← smul_sub] at e
     replace e := Submodule.smul_mem _ (IsLocalization.mk' S 1 x) e
diff --git a/Mathlib/Algebra/Module/Presentation/Free.lean b/Mathlib/Algebra/Module/Presentation/Free.lean
@@ -81,8 +81,7 @@ lemma free_iff_exists_presentation :
   constructor
   · rw [free_def.{_, _, v}]
     rintro ⟨G, ⟨⟨e⟩⟩⟩
-    exact ⟨(presentationFinsupp A G).ofLinearEquiv e.symm,
-      by dsimp; infer_instance⟩
+    exact ⟨(presentationFinsupp A G).ofLinearEquiv e.symm, by dsimp; infer_instance⟩
   · rintro ⟨p, h⟩
     exact p.toIsPresentation.free
 
diff --git a/Mathlib/Algebra/MvPolynomial/Basic.lean b/Mathlib/Algebra/MvPolynomial/Basic.lean
@@ -550,8 +550,8 @@ def coeff (m : σ →₀ ℕ) (p : MvPolynomial σ R) : R :=
 theorem mem_support_iff {p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∈ p.support ↔ p.coeff m ≠ 0 := by
   simp [support, coeff]
 
-theorem notMem_support_iff {p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∉ p.support ↔ p.coeff m = 0 :=
-  by simp
+theorem notMem_support_iff {p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∉ p.support ↔ p.coeff m = 0 := by
+  simp
 
 theorem sum_def {A} [AddCommMonoid A] {p : MvPolynomial σ R} {b : (σ →₀ ℕ) → R → A} :
     p.sum b = ∑ m ∈ p.support, b m (p.coeff m) := by simp [support, Finsupp.sum, coeff]
diff --git a/Mathlib/Algebra/Order/CauSeq/Completion.lean b/Mathlib/Algebra/Order/CauSeq/Completion.lean
@@ -210,10 +210,10 @@ theorem inv_zero : (0 : (Cauchy abv))⁻¹ = 0 :=
 theorem inv_mk {f} (hf) : (mk (abv := abv) f)⁻¹ = mk (inv f hf) :=
   congr_arg mk <| by rw [dif_neg]
 
-theorem cau_seq_zero_ne_one : ¬(0 : CauSeq _ abv) ≈ 1 := fun h =>
+theorem cau_seq_zero_ne_one : ¬(0 : CauSeq _ abv) ≈ 1 := fun h ↦
   have : LimZero (1 - 0 : CauSeq _ abv) := Setoid.symm h
   have : LimZero (1 : CauSeq _ abv) := by simpa
-  by apply one_ne_zero <| const_limZero.1 this
+  one_ne_zero <| const_limZero.1 this
 
 theorem zero_ne_one : (0 : (Cauchy abv)) ≠ 1 := fun h => cau_seq_zero_ne_one <| mk_eq.1 h
 
diff --git a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
@@ -179,19 +179,19 @@ lemma denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units :
       exact ⟨z, by simp [hz, hz']⟩
 
 -- Counterexample with monoid: `{ x : ℝ | 0 ≤ x ≤ 1 }`
-instance [DenselyOrdered α] : Nontrivial αˣ :=
+instance [DenselyOrdered α] : Nontrivial αˣ := by
   have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
-  by tauto
+  tauto
 
 -- Counterexample with monoid:
 -- `{ x : ℝ | x = 0 ∨ ∃ (a : ℤ) (b c : ℕ), x = Real.exp (a + b * √2 - c * √3) }`
-instance [DenselyOrdered α] : DenselyOrdered αˣ :=
+instance [DenselyOrdered α] : DenselyOrdered αˣ := by
   have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
-  by tauto
+  tauto
 
-lemma denselyOrdered_units_iff [Nontrivial αˣ] : DenselyOrdered αˣ ↔ DenselyOrdered α :=
+lemma denselyOrdered_units_iff [Nontrivial αˣ] : DenselyOrdered αˣ ↔ DenselyOrdered α := by
   have := denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units (α := α)
-  by tauto
+  tauto
 
 end LinearOrderedCommGroupWithZero
 
diff --git a/Mathlib/Analysis/Calculus/Deriv/MeanValue.lean b/Mathlib/Analysis/Calculus/Deriv/MeanValue.lean
@@ -333,11 +333,11 @@ of the real line. If `f` is differentiable on the interior of `D` and `f' < C`,
 theorem Convex.image_sub_lt_mul_sub_of_deriv_lt {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
     (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C}
     (lt_hf' : ∀ x ∈ interior D, deriv f x < C) (x : ℝ) (hx : x ∈ D) (y : ℝ) (hy : y ∈ D)
-    (hxy : x < y) : f y - f x < C * (y - x) :=
+    (hxy : x < y) : f y - f x < C * (y - x) := by
   have hf'_gt : ∀ x ∈ interior D, -C < deriv (fun y => -f y) x := fun x hx => by
     rw [deriv.fun_neg, neg_lt_neg_iff]
     exact lt_hf' x hx
-  by linarith [hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x hx y hy hxy]
+  linarith [hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x hx y hy hxy]
 
 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f' < C`, then `f` grows slower than
 `C * x` on `D`, i.e., `f y - f x < C * (y - x)` whenever `x < y`. -/
@@ -353,11 +353,11 @@ of the real line. If `f` is differentiable on the interior of `D` and `f' ≤ C`
 theorem Convex.image_sub_le_mul_sub_of_deriv_le {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
     (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D)) {C}
     (le_hf' : ∀ x ∈ interior D, deriv f x ≤ C) (x : ℝ) (hx : x ∈ D) (y : ℝ) (hy : y ∈ D)
-    (hxy : x ≤ y) : f y - f x ≤ C * (y - x) :=
+    (hxy : x ≤ y) : f y - f x ≤ C * (y - x) := by
   have hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (fun y => -f y) x := fun x hx => by
     rw [deriv.fun_neg, neg_le_neg_iff]
     exact le_hf' x hx
-  by linarith [hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x hx y hy hxy]
+  linarith [hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x hx y hy hxy]
 
 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f' ≤ C`, then `f` grows at most as fast
 as `C * x`, i.e., `f y - f x ≤ C * (y - x)` whenever `x ≤ y`. -/
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean
@@ -642,10 +642,10 @@ TODO (low prio): prove a version without assumption `[HasSummableGeomSeries R]`
 of units. -/
 @[fun_prop]
 theorem hasFDerivAt_ringInverse (x : Rˣ) :
-    HasFDerivAt Ring.inverse (-mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹) x :=
+    HasFDerivAt Ring.inverse (-mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹) x := by
   have : (fun t : R => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =o[𝓝 0] id :=
     (inverse_add_norm_diff_second_order x).trans_isLittleO (isLittleO_norm_pow_id one_lt_two)
-  by simpa [hasFDerivAt_iff_isLittleO_nhds_zero] using this
+  simpa [hasFDerivAt_iff_isLittleO_nhds_zero] using this
 
 @[fun_prop]
 theorem differentiableAt_inverse {x : R} (hx : IsUnit x) :
diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
@@ -484,15 +484,15 @@ lemma iteratedDerivWithin_sum {s : Set 𝕜} (hx : x ∈ s) (hs : UniqueDiffOn 
 
 lemma iteratedDerivWithin_fun_sum {s : Set 𝕜} (hx : x ∈ s) (hs : UniqueDiffOn 𝕜 s)
     (hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 n (f i) s x) :
-    iteratedDerivWithin n (∑ i ∈ I, f i ·) s x = ∑ i ∈ I, iteratedDerivWithin n (f i) s x :=
-  by simpa [sum_fn] using iteratedDerivWithin_sum hx hs hf
+    iteratedDerivWithin n (∑ i ∈ I, f i ·) s x = ∑ i ∈ I, iteratedDerivWithin n (f i) s x := by
+  simpa [sum_fn] using iteratedDerivWithin_sum hx hs hf
 
 lemma iteratedDeriv_sum (hf : ∀ i ∈ I, ContDiffAt 𝕜 n (f i) x) :
     iteratedDeriv n (∑ i ∈ I, f i) x = ∑ i ∈ I, iteratedDeriv n (f i) x := by
   simpa using iteratedDerivWithin_sum (Set.mem_univ x) uniqueDiffOn_univ hf
 
 lemma iteratedDeriv_fun_sum (hf : ∀ i ∈ I, ContDiffAt 𝕜 n (f i) x) :
-    iteratedDeriv n (fun z ↦ ∑ i ∈ I, f i z) x = ∑ i ∈ I, iteratedDeriv n (f i) x :=
-  by simpa [sum_fn] using iteratedDeriv_sum hf
+    iteratedDeriv n (fun z ↦ ∑ i ∈ I, f i z) x = ∑ i ∈ I, iteratedDeriv n (f i) x := by
+  simpa [sum_fn] using iteratedDeriv_sum hf
 
 end sums
diff --git a/Mathlib/Analysis/Complex/Basic.lean b/Mathlib/Analysis/Complex/Basic.lean
@@ -656,9 +656,9 @@ lemma slitPlane_ne_zero {z : ℂ} (hz : z ∈ slitPlane) : z ≠ 0 :=
   ne_of_mem_of_not_mem hz zero_notMem_slitPlane
 
 /-- The slit plane includes the open unit ball of radius `1` around `1`. -/
-lemma ball_one_subset_slitPlane : Metric.ball 1 1 ⊆ slitPlane := fun z hz ↦ .inl <|
+lemma ball_one_subset_slitPlane : Metric.ball 1 1 ⊆ slitPlane := fun z hz ↦ .inl <| by
   have : -1 < z.re - 1 := neg_lt_of_abs_lt <| (abs_re_le_norm _).trans_lt hz
-  by linarith
+  linarith
 
 /-- The slit plane includes the open unit ball of radius `1` around `1`. -/
 lemma mem_slitPlane_of_norm_lt_one {z : ℂ} (hz : ‖z‖ < 1) : 1 + z ∈ slitPlane :=
diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean
@@ -1159,9 +1159,9 @@ theorem continuous_of_le [TopologicalSpace E] [IsTopologicalAddGroup E]
   exact isOpen_lt hq continuous_const
 
 lemma ball_mem_nhds [TopologicalSpace E] {p : Seminorm 𝕝 E} (hp : Continuous p) {r : ℝ}
-    (hr : 0 < r) : p.ball 0 r ∈ (𝓝 0 : Filter E) :=
+    (hr : 0 < r) : p.ball 0 r ∈ (𝓝 0 : Filter E) := by
   have this : Tendsto p (𝓝 0) (𝓝 0) := map_zero p ▸ hp.tendsto 0
-  by simpa only [p.ball_zero_eq] using this (Iio_mem_nhds hr)
+  simpa only [p.ball_zero_eq] using this (Iio_mem_nhds hr)
 
 lemma uniformSpace_eq_of_hasBasis
     {ι} [UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E]
diff --git a/Mathlib/CategoryTheory/Adjunction/Mates.lean b/Mathlib/CategoryTheory/Adjunction/Mates.lean
@@ -391,8 +391,7 @@ is an isomorphism, then `α` is an isomorphism. The converse is given in `conjug
 -/
 theorem conjugateEquiv_of_iso (α : L₂ ⟶ L₁) [IsIso (conjugateEquiv adj₁ adj₂ α)] :
     IsIso α := by
-  suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α))
-    by simpa using this
+  suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α)) by simpa using this
   infer_instance
 
 /--
diff --git a/Mathlib/CategoryTheory/Join/Basic.lean b/Mathlib/CategoryTheory/Join/Basic.lean
@@ -286,8 +286,7 @@ action on edge maps. -/
 def mkNatTrans {F : C ⋆ D ⥤ E} {F' : C ⋆ D ⥤ E}
     (αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F') (αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F')
     (h : whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
-      whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F' :=
-      by cat_disch) :
+      whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F' := by cat_disch) :
     F ⟶ F' where
   app x := match x with
     | left x => αₗ.app x
@@ -303,8 +302,7 @@ section
 variable {F : C ⋆ D ⥤ E} {F' : C ⋆ D ⥤ E}
     (αₗ : inclLeft C D ⋙ F ⟶ inclLeft C D ⋙ F') (αᵣ : inclRight C D ⋙ F ⟶ inclRight C D ⋙ F')
     (h : whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
-      whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F' :=
-      by cat_disch)
+      whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F' := by cat_disch)
 
 set_option backward.privateInPublic true in
 set_option backward.privateInPublic.warn false in
@@ -354,8 +352,7 @@ lemma mkNatTransComp
     (βₗ : inclLeft C D ⋙ F' ⟶ inclLeft C D ⋙ F'')
     (βᵣ : inclRight C D ⋙ F' ⟶ inclRight C D ⋙ F'')
     (h : whiskerRight (edgeTransform C D) F ≫ whiskerLeft (Prod.snd C D) αᵣ =
-      whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F' :=
-      by cat_disch)
+      whiskerLeft (Prod.fst C D) αₗ ≫ whiskerRight (edgeTransform C D) F' := by cat_disch)
     (h' : whiskerRight (edgeTransform C D) F' ≫ whiskerLeft (Prod.snd C D) βᵣ =
       whiskerLeft (Prod.fst C D) βₗ ≫ whiskerRight (edgeTransform C D) F'' := by cat_disch) :
     mkNatTrans (αₗ ≫ βₗ) (αᵣ ≫ βᵣ) (by simp [← h', reassoc_of% h]) =
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean
@@ -42,9 +42,8 @@ def isLimitMapConeFanMkEquiv {P : C} (g : ∀ j, P ⟶ f j) :
     IsLimit (Functor.mapCone G (Fan.mk P g)) ≃
       IsLimit (Fan.mk _ fun j => G.map (g j) : Fan fun j => G.obj (f j)) := by
   refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)
-  · refine Discrete.natIso fun j => Iso.refl (G.obj (f j.as))
-  refine Cones.ext (Iso.refl _) fun j =>
-      by dsimp; cases j; simp
+  · exact Discrete.natIso fun j => Iso.refl (G.obj (f j.as))
+  exact Cones.ext (Iso.refl _) fun j ↦ by dsimp; cases j; simp
 
 /-- The property of preserving products expressed in terms of fans. -/
 def isLimitFanMkObjOfIsLimit [PreservesLimit (Discrete.functor f) G] {P : C} (g : ∀ j, P ⟶ f j)
diff --git a/Mathlib/CategoryTheory/Limits/Types/Multicoequalizer.lean b/Mathlib/CategoryTheory/Limits/Types/Multicoequalizer.lean
@@ -45,8 +45,7 @@ lemma isMulticoequalizer_iff {J : MultispanShape.{w, w'}} {d : MultispanIndex J
   have (x : d.multispan.ColimitType) :
       ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (.right i) a = x := by
     obtain ⟨(l | r), z, rfl⟩ := d.multispan.ιColimitType_jointly_surjective x
-    · exact ⟨J.fst l, d.multispan.map (WalkingMultispan.Hom.fst l) z,
-        by rw [ιColimitType_map]⟩
+    · exact ⟨J.fst l, d.multispan.map (WalkingMultispan.Hom.fst l) z, by rw [ιColimitType_map]⟩
     · exact ⟨r, z, by simp⟩
   constructor
   · intro hc
diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean
@@ -241,8 +241,8 @@ namespace Hom
 
 @[simp] lemma hom_hom_inv (f : G ⟶ H) : f⁻¹.hom.hom = f.hom.hom⁻¹ := rfl
 @[simp] lemma hom_hom_div (f g : G ⟶ H) : (f / g).hom.hom = f.hom.hom / g.hom.hom := rfl
-@[simp] lemma hom_hom_zpow (f : G ⟶ H) (n : ℤ) : (f ^ n).hom.hom = f.hom.hom ^ n :=
-  by cases n <;> simp
+@[simp] lemma hom_hom_zpow (f : G ⟶ H) (n : ℤ) : (f ^ n).hom.hom = f.hom.hom ^ n := by
+  cases n <;> simp
 
 @[deprecated (since := "2025-12-18")] alias hom_inv := hom_hom_inv
 @[deprecated (since := "2025-12-18")] alias hom_div := hom_hom_div
diff --git a/Mathlib/CategoryTheory/Topos/Classifier.lean b/Mathlib/CategoryTheory/Topos/Classifier.lean
@@ -124,8 +124,7 @@ def mkOfTerminalΩ₀
 instance {c : Classifier C} : ∀ Y : C, Unique (Y ⟶ c.Ω₀) := fun Y =>
   { default := c.χ₀ Y,
     uniq f :=
-      have : f ≫ c.truth = c.χ₀ Y ≫ c.truth :=
-        by calc
+      have : f ≫ c.truth = c.χ₀ Y ≫ c.truth := calc
           _ = c.χ (𝟙 Y) := c.uniq (𝟙 Y) (of_horiz_isIso_mono { })
           _ = c.χ₀ Y ≫ c.truth := by simp [← (c.isPullback (𝟙 Y)).w]
       Mono.right_cancellation _ _ this }
diff --git a/Mathlib/Combinatorics/Matroid/Circuit.lean b/Mathlib/Combinatorics/Matroid/Circuit.lean
@@ -726,8 +726,8 @@ lemma IsBase.mem_fundCocircuit_iff_mem_fundCircuit {e f : α} (hB : M.IsBase B)
   obtain hfB | hfB := em' <| f ∈ B
   · rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he
     contradiction
-  obtain ⟨heE, heB⟩ : e ∈ M.E \ B :=
-    by simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he
+  obtain ⟨heE, heB⟩ : e ∈ M.E \ B := by
+    simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he
   -- Use basis exchange to argue the equivalence.
   rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he
   rw [hB.indep.mem_fundCircuit_iff (by rwa [hB.closure_eq]) heB]
diff --git a/Mathlib/Combinatorics/Matroid/Loop.lean b/Mathlib/Combinatorics/Matroid/Loop.lean
@@ -284,8 +284,9 @@ lemma compl_loops_eq (M : Matroid α) : M.E \ M.loops = {e | M.IsNonloop e} := b
 lemma isNonloop_of_not_isLoop (he : e ∈ M.E := by aesop_mat) (h : ¬ M.IsLoop e) : M.IsNonloop e :=
   ⟨h,he⟩
 
-lemma isLoop_of_not_isNonloop (he : e ∈ M.E := by aesop_mat) (h : ¬ M.IsNonloop e) : M.IsLoop e :=
-  by rwa [isNonloop_iff, and_iff_left he, not_not] at h
+lemma isLoop_of_not_isNonloop (he : e ∈ M.E := by aesop_mat) (h : ¬ M.IsNonloop e) :
+    M.IsLoop e := by
+  rwa [isNonloop_iff, and_iff_left he, not_not] at h
 
 @[simp]
 lemma not_isLoop_iff (he : e ∈ M.E := by aesop_mat) : ¬M.IsLoop e ↔ M.IsNonloop e :=
@@ -482,8 +483,7 @@ lemma IsColoop.dual_isLoop (he : M.IsColoop e) : M✶.IsLoop e :=
 lemma IsColoop.isCocircuit (he : M.IsColoop e) : M.IsCocircuit {e} :=
   IsLoop.isCircuit he
 
-lemma IsLoop.dual_isColoop (he : M.IsLoop e) : M✶.IsColoop e :=
-  by rwa [IsColoop, dual_dual]
+lemma IsLoop.dual_isColoop (he : M.IsLoop e) : M✶.IsColoop e := by rwa [IsColoop, dual_dual]
 
 @[simp]
 lemma dual_isColoop_iff_isLoop : M✶.IsColoop e ↔ M.IsLoop e :=
diff --git a/Mathlib/Computability/NFA.lean b/Mathlib/Computability/NFA.lean
@@ -292,8 +292,8 @@ theorem mem_evalFrom_iff_nonempty_path {s t : σ} {x : List α} :
       have h : s = t := by simp at h; tauto
       ⟨h ▸ Path.nil s⟩
     | a :: x =>
-      have h : ∃ s' ∈ M.step s a, t ∈ M.evalFrom {s'} x :=
-        by rw [evalFrom_cons, mem_evalFrom_iff_exists, stepSet_singleton] at h; exact h
+      have h : ∃ s' ∈ M.step s a, t ∈ M.evalFrom {s'} x := by
+        rw [evalFrom_cons, mem_evalFrom_iff_exists, stepSet_singleton] at h; exact h
       let ⟨s', h₁, h₂⟩ := h
       let ⟨p'⟩ := mem_evalFrom_iff_nonempty_path.1 h₂
       ⟨Path.cons s' _ _ _ _ h₁ p'⟩
diff --git a/Mathlib/Data/Finset/Grade.lean b/Mathlib/Data/Finset/Grade.lean
@@ -107,8 +107,8 @@ lemma covBy_insert (ha : a ∉ s) : s ⋖ insert a s :=
   (wcovBy_insert _ _).covBy_of_lt <| ssubset_insert ha
 
 omit [DecidableEq α] in
-@[simp] lemma empty_covBy_singleton (a : α) : ∅ ⋖ ({a} : Finset α) :=
-  by classical exact insert_empty_eq (β := Finset α) a ▸ covBy_insert <| notMem_empty a
+@[simp] lemma empty_covBy_singleton (a : α) : ∅ ⋖ ({a} : Finset α) := by
+  classical exact insert_empty_eq (β := Finset α) a ▸ covBy_insert <| notMem_empty a
 
 @[simp] lemma erase_covBy (ha : a ∈ s) : s.erase a ⋖ s := ⟨erase_ssubset ha, (erase_wcovBy _ _).2⟩
 
diff --git a/Mathlib/Data/Finsupp/Single.lean b/Mathlib/Data/Finsupp/Single.lean
@@ -396,8 +396,8 @@ variable [Zero M] [Zero N] [Zero P]
 
 @[simp]
 theorem mapRange_single {f : M → N} {hf : f 0 = 0} {a : α} {b : M} :
-    mapRange f hf (single a b) = single a (f b) :=
-  by classical grind
+    mapRange f hf (single a b) = single a (f b) := by
+  classical grind
 
 end MapRange
 
diff --git a/Mathlib/GroupTheory/Perm/Fin.lean b/Mathlib/GroupTheory/Perm/Fin.lean
diff --git a/Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean b/Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean
diff --git a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean
diff --git a/Mathlib/NumberTheory/ModularForms/ArithmeticSubgroups.lean b/Mathlib/NumberTheory/ModularForms/ArithmeticSubgroups.lean
diff --git a/Mathlib/Order/RelSeries.lean b/Mathlib/Order/RelSeries.lean
diff --git a/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean b/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean b/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
diff --git a/Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean b/Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean
diff --git a/Mathlib/Topology/Sets/OpenCover.lean b/Mathlib/Topology/Sets/OpenCover.lean
diff --git a/MathlibTest/Use.lean b/MathlibTest/Use.lean
