style: cleanup by putting by on the same line as := (#8407)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Archive/Imo/Imo2005Q3.lean

@@ -36,9 +36,7 @@ theorem key_insight (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x
     ring
   have h₅ :
     (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) /
-        ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) ≥
-      0 :=
-    by positivity
+        ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) ≥ 0 := by positivity
   calc
     (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2)
       ≥ (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) := by linarith only [key, h₅]

Archive/Wiedijk100Theorems/Partition.lean

@@ -496,15 +496,15 @@ theorem same_gf [Field α] (m : ℕ) :
   calc
     (∏ i in range (m + 1), (1 - X ^ (2 * i + 1))⁻¹) *
           ∏ i in range (m + 1), (1 - X ^ (m + 1 + i + 1)) =
-        π₁ * (1 - X ^ (2 * m + 1))⁻¹ * (π₀ * (1 - X ^ (m + 1 + m + 1))) :=
-      by rw [prod_range_succ _ m, ← hπ₁, prod_range_succ _ m, ← hπ₀]
+        π₁ * (1 - X ^ (2 * m + 1))⁻¹ * (π₀ * (1 - X ^ (m + 1 + m + 1))) := by
+      rw [prod_range_succ _ m, ← hπ₁, prod_range_succ _ m, ← hπ₀]
     _ = π₁ * (1 - X ^ (2 * m + 1))⁻¹ * (π₀ * ((1 + X ^ (m + 1)) * (1 - X ^ (m + 1)))) := by
       rw [← sq_sub_sq, one_pow, add_assoc _ m 1, ← two_mul (m + 1), pow_mul']
     _ = π₀ * (1 - X ^ (m + 1)) * (1 - X ^ (2 * m + 1))⁻¹ * (π₁ * (1 + X ^ (m + 1))) := by ring
     _ =
         (∏ i in range (m + 1), (1 - X ^ (m + 1 + i))) * (1 - X ^ (2 * m + 1))⁻¹ *
-          (π₁ * (1 + X ^ (m + 1))) :=
-      by rw [prod_range_succ', add_zero, hπ₀]; simp_rw [← add_assoc]
+          (π₁ * (1 + X ^ (m + 1))) := by
+      rw [prod_range_succ', add_zero, hπ₀]; simp_rw [← add_assoc]
     _ = π₂ * (1 - X ^ (m + 1 + m)) * (1 - X ^ (2 * m + 1))⁻¹ * (π₁ * (1 + X ^ (m + 1))) := by
       rw [add_right_comm, hπ₂, ← prod_range_succ]; simp_rw [add_right_comm]
     _ = π₂ * (1 - X ^ (2 * m + 1)) * (1 - X ^ (2 * m + 1))⁻¹ * (π₁ * (1 + X ^ (m + 1))) := by

Archive/Wiedijk100Theorems/SolutionOfCubic.lean

@@ -105,8 +105,8 @@ theorem cubic_eq_zero_iff (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
   have hi3 : (3 : K) ≠ 0 := nonzero_of_invertible _
   have h9 : (9 : K) = 3 ^ 2 := by norm_num
   have h54 : (54 : K) = 2 * 3 ^ 3 := by norm_num
-  have h₁ : a * x ^ 3 + b * x ^ 2 + c * x + d = a * (x ^ 3 + b / a * x ^ 2 + c / a * x + d / a) :=
-    by field_simp; ring
+  have h₁ : a * x ^ 3 + b * x ^ 2 + c * x + d
+    = a * (x ^ 3 + b / a * x ^ 2 + c / a * x + d / a) := by field_simp; ring
   have h₂ : ∀ x, a * x = 0 ↔ x = 0 := by intro x; simp [ha]
   have hp' : p = (3 * (c / a) - (b / a) ^ 2) / 9 := by field_simp [hp, h9]; ring_nf
   have hq' : q = (9 * (b / a) * (c / a) - 2 * (b / a) ^ 3 - 27 * (d / a)) / 54 := by
@@ -136,8 +136,8 @@ theorem cubic_eq_zero_iff_of_p_eq_zero (ha : a ≠ 0) (hω : IsPrimitiveRoot ω
   have h₂ :=
     calc
       a * x ^ 3 + b * x ^ 2 + c * x + d =
-          a * (x + b / (3 * a)) ^ 3 + (c - b ^ 2 / (3 * a)) * x + (d - b ^ 3 * a / (3 * a) ^ 3) :=
-        by field_simp; ring
+      a * (x + b / (3 * a)) ^ 3 + (c - b ^ 2 / (3 * a)) * x + (d - b ^ 3 * a / (3 * a) ^ 3) := by
+        field_simp; ring
       _ = a * (x + b / (3 * a)) ^ 3 + (d - (9 * a * b * c - 2 * b ^ 3) * a / (3 * a) ^ 3) := by
         simp only [hb2, hb3]; field_simp; ring
       _ = a * ((x + b / (3 * a)) ^ 3 - s ^ 3) := by rw [hs3, hq]; field_simp [h54]; ring

Mathlib/Algebra/Algebra/Basic.lean

@@ -368,8 +368,9 @@ theorem left_comm (x : A) (r : R) (y : A) :
 #align algebra.left_comm Algebra.left_comm
 
 /-- `mul_right_comm` for `Algebra`s when one element is from the base ring. -/
-theorem right_comm (x : A) (r : R) (y : A) : x * algebraMap R A r * y = x * y * algebraMap R A r :=
-  by rw [mul_assoc, commutes, ← mul_assoc]
+theorem right_comm (x : A) (r : R) (y : A) :
+    x * algebraMap R A r * y = x * y * algebraMap R A r := by
+  rw [mul_assoc, commutes, ← mul_assoc]
 #align algebra.right_comm Algebra.right_comm
 
 instance _root_.IsScalarTower.right : IsScalarTower R A A :=

Mathlib/Algebra/Algebra/Operations.lean

@@ -294,8 +294,8 @@ theorem map_op_mul :
 theorem comap_unop_mul :
     comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M * N) =
       comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) N *
-        comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M :=
-  by simp_rw [← map_equiv_eq_comap_symm, map_op_mul]
+        comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M := by
+  simp_rw [← map_equiv_eq_comap_symm, map_op_mul]
 #align submodule.comap_unop_mul Submodule.comap_unop_mul
 
 theorem map_unop_mul (M N : Submodule R Aᵐᵒᵖ) :
@@ -312,8 +312,8 @@ theorem map_unop_mul (M N : Submodule R Aᵐᵒᵖ) :
 theorem comap_op_mul (M N : Submodule R Aᵐᵒᵖ) :
     comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
       comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) N *
-        comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M :=
-  by simp_rw [comap_equiv_eq_map_symm, map_unop_mul]
+        comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M := by
+  simp_rw [comap_equiv_eq_map_symm, map_unop_mul]
 #align submodule.comap_op_mul Submodule.comap_op_mul
 
 section
@@ -534,14 +534,14 @@ theorem comap_op_pow (n : ℕ) (M : Submodule R Aᵐᵒᵖ) :
 
 theorem map_op_pow (n : ℕ) :
     map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) =
-      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M ^ n :=
-  by rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]
+      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M ^ n := by
+  rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]
 #align submodule.map_op_pow Submodule.map_op_pow
 
 theorem map_unop_pow (n : ℕ) (M : Submodule R Aᵐᵒᵖ) :
     map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
-      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M ^ n :=
-  by rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]
+      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M ^ n := by
+  rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]
 #align submodule.map_unop_pow Submodule.map_unop_pow
 
 /-- `span` is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets

Mathlib/Algebra/Algebra/Spectrum.lean

@@ -230,13 +230,11 @@ theorem unit_mem_mul_iff_mem_swap_mul {a b : A} {r : Rˣ} : ↑r ∈ σ (a * b)
     refine' fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, _, _⟩, rfl⟩
     calc
       (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
-          1 - y * x + y * ((1 - x * y) * h.unit.inv) * x :=
-        by noncomm_ring
+          1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
       _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
     calc
       (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
-          1 - y * x + y * (h.unit.inv * (1 - x * y)) * x :=
-        by noncomm_ring
+          1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
       _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
   have := Iff.intro (h₁ (r⁻¹ • a) b) (h₁ b (r⁻¹ • a))
   rw [mul_smul_comm r⁻¹ b a] at this

Mathlib/Algebra/Algebra/Tower.lean

@@ -157,8 +157,8 @@ variable {R S A B}
 
 @[simp]
 theorem _root_.AlgHom.map_algebraMap (f : A →ₐ[S] B) (r : R) :
-    f (algebraMap R A r) = algebraMap R B r :=
-  by rw [algebraMap_apply R S A r, f.commutes, ← algebraMap_apply R S B]
+    f (algebraMap R A r) = algebraMap R B r := by
+  rw [algebraMap_apply R S A r, f.commutes, ← algebraMap_apply R S B]
 #align alg_hom.map_algebra_map AlgHom.map_algebraMap
 
 variable (R)

Mathlib/Algebra/Associated.lean

@@ -913,8 +913,8 @@ theorem isUnit_iff_eq_bot {a : Associates α} : IsUnit a ↔ a = ⊥ := by
 
 theorem isUnit_mk {a : α} : IsUnit (Associates.mk a) ↔ IsUnit a :=
   calc
-    IsUnit (Associates.mk a) ↔ a ~ᵤ 1 :=
-    by rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]
+    IsUnit (Associates.mk a) ↔ a ~ᵤ 1 := by
+      rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]
     _ ↔ IsUnit a := associated_one_iff_isUnit
 #align associates.is_unit_mk Associates.isUnit_mk
 
@@ -1123,8 +1123,7 @@ instance instCancelCommMonoidWithZero : CancelCommMonoidWithZero (Associates α)
     have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]
     exact Quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩ }
 
-instance : NoZeroDivisors (Associates α) :=
-  by infer_instance
+instance : NoZeroDivisors (Associates α) := by infer_instance
 
 theorem le_of_mul_le_mul_left (a b c : Associates α) (ha : a ≠ 0) : a * b ≤ a * c → b ≤ c
   | ⟨d, hd⟩ => ⟨d, mul_left_cancel₀ ha <| by rwa [← mul_assoc]⟩

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -199,8 +199,8 @@ section GaussSum
 /-- Gauss' summation formula -/
 theorem sum_range_id_mul_two (n : ℕ) : (∑ i in range n, i) * 2 = n * (n - 1) :=
   calc
-    (∑ i in range n, i) * 2 = (∑ i in range n, i) + ∑ i in range n, (n - 1 - i) :=
-    by rw [sum_range_reflect (fun i => i) n, mul_two]
+    (∑ i in range n, i) * 2 = (∑ i in range n, i) + ∑ i in range n, (n - 1 - i) := by
+      rw [sum_range_reflect (fun i => i) n, mul_two]
     _ = ∑ i in range n, (i + (n - 1 - i)) := sum_add_distrib.symm
     _ = ∑ i in range n, (n - 1) :=
       sum_congr rfl fun i hi => add_tsub_cancel_of_le <| Nat.le_sub_one_of_lt <| mem_range.1 hi

Mathlib/Algebra/BigOperators/NatAntidiagonal.lean

@@ -23,8 +23,9 @@ namespace Finset
 namespace Nat
 
 theorem prod_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → M} :
-    (∏ p in antidiagonal (n + 1), f p) = f (0, n + 1) * ∏ p in antidiagonal n, f (p.1 + 1, p.2) :=
-  by rw [antidiagonal_succ, prod_cons, prod_map]; rfl
+    (∏ p in antidiagonal (n + 1), f p)
+      = f (0, n + 1) * ∏ p in antidiagonal n, f (p.1 + 1, p.2) := by
+  rw [antidiagonal_succ, prod_cons, prod_map]; rfl
 #align finset.nat.prod_antidiagonal_succ Finset.Nat.prod_antidiagonal_succ
 
 theorem sum_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → N} :

Mathlib/Algebra/BigOperators/Ring.lean

@@ -106,8 +106,8 @@ theorem prod_sum {δ : α → Type*} [DecidableEq α] [∀ a, DecidableEq (δ a)
       intro x _ y _ h
       simp only [disjoint_iff_ne, mem_image]
       rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
-      have : Pi.cons s a x p₂ a (mem_insert_self _ _) = Pi.cons s a y p₃ a (mem_insert_self _ _) :=
-        by rw [eq₂, eq₃, eq]
+      have : Pi.cons s a x p₂ a (mem_insert_self _ _)
+              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
       rw [Pi.cons_same, Pi.cons_same] at this
       exact h this
     rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
@@ -134,8 +134,7 @@ theorem prod_add [DecidableEq α] (f g : α → β) (s : Finset α) :
   classical
   calc
     ∏ a in s, (f a + g a) =
-        ∏ a in s, ∑ p in ({True, False} : Finset Prop), if p then f a else g a :=
-      by simp
+        ∏ a in s, ∑ p in ({True, False} : Finset Prop), if p then f a else g a := by simp
     _ = ∑ p in (s.pi fun _ => {True, False} : Finset (∀ a ∈ s, Prop)),
           ∏ a in s.attach, if p a.1 a.2 then f a.1 else g a.1 :=
       prod_sum

Mathlib/Algebra/Category/ModuleCat/Free.lean

@@ -121,8 +121,8 @@ theorem span_exact (he : Exact f g) (huv : u ∘ Sum.inl = f ∘ v)
   rw [← sub_add_cancel m m', ← hnm,]
   simp only [SMulHomClass.map_smul]
   have hn' : (Finsupp.sum cn fun a b ↦ b • f (v a)) =
-      (Finsupp.sum cn fun a b ↦ b • u (Sum.inl a)) :=
-    by congr; ext a b; change b • (f ∘ v) a = _; rw [← huv]; rfl
+      (Finsupp.sum cn fun a b ↦ b • u (Sum.inl a)) := by
+    congr; ext a b; change b • (f ∘ v) a = _; rw [← huv]; rfl
   rw [hn']
   apply add_mem
   · rw [Finsupp.mem_span_range_iff_exists_finsupp]

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -152,8 +152,8 @@ end
 theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : ModuleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂)
     (f₃ : X₃ ⟶ Y₃) :
     tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
-      (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) :=
-  by convert associator_naturality_aux f₁ f₂ f₃ using 1
+      (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) := by
+  convert associator_naturality_aux f₁ f₂ f₃ using 1
 #align Module.monoidal_category.associator_naturality ModuleCat.MonoidalCategory.associator_naturality
 
 theorem pentagon (W X Y Z : ModuleCat R) :

Mathlib/Algebra/Free.lean

@@ -724,8 +724,7 @@ theorem toFreeSemigroup_comp_of : @toFreeSemigroup α ∘ of = FreeSemigroup.of
 
 @[to_additive]
 theorem toFreeSemigroup_comp_map (f : α → β) :
-    toFreeSemigroup.comp (map f) = (FreeSemigroup.map f).comp toFreeSemigroup :=
-  by ext1; rfl
+    toFreeSemigroup.comp (map f) = (FreeSemigroup.map f).comp toFreeSemigroup := by ext1; rfl
 #align free_magma.to_free_semigroup_comp_map FreeMagma.toFreeSemigroup_comp_map
 
 @[to_additive]

Mathlib/Algebra/GeomSum.lean

@@ -143,8 +143,7 @@ theorem geom_sum₂_self {α : Type*} [CommRing α] (x : α) (n : ℕ) :
     ∑ i in range n, x ^ i * x ^ (n - 1 - i) = n * x ^ (n - 1) :=
   calc
     ∑ i in Finset.range n, x ^ i * x ^ (n - 1 - i) =
-        ∑ i in Finset.range n, x ^ (i + (n - 1 - i)) :=
-      by simp_rw [← pow_add]
+        ∑ i in Finset.range n, x ^ (i + (n - 1 - i)) := by simp_rw [← pow_add]
     _ = ∑ i in Finset.range n, x ^ (n - 1) :=
       Finset.sum_congr rfl fun i hi =>
         congr_arg _ <| add_tsub_cancel_of_le <| Nat.le_sub_one_of_lt <| Finset.mem_range.1 hi
@@ -418,8 +417,8 @@ theorem Nat.pred_mul_geom_sum_le (a b n : ℕ) :
     ((b - 1) * ∑ i in range n.succ, a / b ^ i) ≤ a * b - a / b ^ n :=
   calc
     ((b - 1) * ∑ i in range n.succ, a / b ^ i) =
-        (∑ i in range n, a / b ^ (i + 1) * b) + a * b - ((∑ i in range n, a / b ^ i) + a / b ^ n) :=
-      by rw [tsub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
+    (∑ i in range n, a / b ^ (i + 1) * b) + a * b - ((∑ i in range n, a / b ^ i) + a / b ^ n) := by
+      rw [tsub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
         Nat.div_one]
     _ ≤ (∑ i in range n, a / b ^ i) + a * b - ((∑ i in range n, a / b ^ i) + a / b ^ n) := by
       refine' tsub_le_tsub_right (add_le_add_right (sum_le_sum fun i _ => _) _) _

Mathlib/Algebra/GradedMonoid.lean

@@ -446,8 +446,8 @@ theorem GradedMonoid.list_prod_map_eq_dProd (l : List α) (f : α → GradedMono
 
 theorem GradedMonoid.list_prod_ofFn_eq_dProd {n : ℕ} (f : Fin n → GradedMonoid A) :
     (List.ofFn f).prod =
-      GradedMonoid.mk _ ((List.finRange n).dProd (fun i => (f i).1) fun i => (f i).2) :=
-  by rw [List.ofFn_eq_map, GradedMonoid.list_prod_map_eq_dProd]
+      GradedMonoid.mk _ ((List.finRange n).dProd (fun i => (f i).1) fun i => (f i).2) := by
+  rw [List.ofFn_eq_map, GradedMonoid.list_prod_map_eq_dProd]
 #align graded_monoid.list_prod_of_fn_eq_dprod GradedMonoid.list_prod_ofFn_eq_dProd
 
 end DProd

Mathlib/Algebra/IndicatorFunction.lean

@@ -355,8 +355,9 @@ variable [MulOneClass M] {s t : Set α} {f g : α → M} {a : α}
 
 @[to_additive]
 theorem mulIndicator_union_mul_inter_apply (f : α → M) (s t : Set α) (a : α) :
-    mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a :=
-  by by_cases hs : a ∈ s <;> by_cases ht : a ∈ t <;> simp [*]
+    mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a
+      = mulIndicator s f a * mulIndicator t f a := by
+  by_cases hs : a ∈ s <;> by_cases ht : a ∈ t <;> simp [*]
 #align set.mul_indicator_union_mul_inter_apply Set.mulIndicator_union_mul_inter_apply
 #align set.indicator_union_add_inter_apply Set.indicator_union_add_inter_apply
 

Mathlib/Algebra/Periodic.lean

@@ -413,8 +413,9 @@ protected theorem Antiperiodic.neg [AddGroup α] [InvolutiveNeg β] (h : Antiper
     Antiperiodic f (-c) := by simpa only [sub_eq_add_neg, Antiperiodic] using h.sub_eq
 #align function.antiperiodic.neg Function.Antiperiodic.neg
 
-theorem Antiperiodic.neg_eq [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) : f (-c) = -f 0 :=
-  by simpa only [zero_add] using h.neg 0
+theorem Antiperiodic.neg_eq [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) :
+    f (-c) = -f 0 := by
+  simpa only [zero_add] using h.neg 0
 #align function.antiperiodic.neg_eq Function.Antiperiodic.neg_eq
 
 theorem Antiperiodic.nat_mul_eq_of_eq_zero [Semiring α] [NegZeroClass β] (h : Antiperiodic f c)

Mathlib/Algebra/Quaternion.lean

@@ -1267,8 +1267,8 @@ theorem im_sq : a.im ^ 2 = -normSq a.im := by
   simp_rw [sq, ← star_mul_self, im_star, neg_mul, neg_neg]
 #align quaternion.im_sq Quaternion.im_sq
 
-theorem coe_normSq_add : normSq (a + b) = normSq a + a * star b + b * star a + normSq b :=
-  by simp only [star_add, ← self_mul_star, mul_add, add_mul, add_assoc, add_left_comm]
+theorem coe_normSq_add : normSq (a + b) = normSq a + a * star b + b * star a + normSq b := by
+  simp only [star_add, ← self_mul_star, mul_add, add_mul, add_assoc, add_left_comm]
 #align quaternion.coe_norm_sq_add Quaternion.coe_normSq_add
 
 theorem normSq_smul (r : R) (q : ℍ[R]) : normSq (r • q) = r ^ 2 * normSq q := by

Mathlib/Algebra/RingQuot.lean

@@ -623,8 +623,9 @@ theorem mkAlgHom_coe (s : A → A → Prop) : (mkAlgHom S s : A →+* RingQuot s
   rfl
 #align ring_quot.mk_alg_hom_coe RingQuot.mkAlgHom_coe
 
-theorem mkAlgHom_rel {s : A → A → Prop} {x y : A} (w : s x y) : mkAlgHom S s x = mkAlgHom S s y :=
-  by simp [mkAlgHom_def, mkRingHom_def, Quot.sound (Rel.of w)]
+theorem mkAlgHom_rel {s : A → A → Prop} {x y : A} (w : s x y) :
+    mkAlgHom S s x = mkAlgHom S s y := by
+  simp [mkAlgHom_def, mkRingHom_def, Quot.sound (Rel.of w)]
 #align ring_quot.mk_alg_hom_rel RingQuot.mkAlgHom_rel
 
 theorem mkAlgHom_surjective (s : A → A → Prop) : Function.Surjective (mkAlgHom S s) := by

Mathlib/Algebra/Support.lean

@@ -99,8 +99,9 @@ theorem mulSupport_disjoint_iff {f : α → M} {s : Set α} :
 #align function.support_disjoint_iff Function.support_disjoint_iff
 
 @[to_additive]
-theorem disjoint_mulSupport_iff {f : α → M} {s : Set α} : Disjoint s (mulSupport f) ↔ EqOn f 1 s :=
-  by rw [disjoint_comm, mulSupport_disjoint_iff]
+theorem disjoint_mulSupport_iff {f : α → M} {s : Set α} :
+    Disjoint s (mulSupport f) ↔ EqOn f 1 s := by
+  rw [disjoint_comm, mulSupport_disjoint_iff]
 #align function.disjoint_mul_support_iff Function.disjoint_mulSupport_iff
 #align function.disjoint_support_iff Function.disjoint_support_iff
 

Mathlib/GroupTheory/Submonoid/Pointwise.lean

@@ -678,8 +678,9 @@ theorem closure_pow (s : Set R) : ∀ n : ℕ, closure s ^ n = closure (s ^ n)
   | n + 1 => by rw [pow_succ, pow_succ, closure_pow s n, closure_mul_closure]
 #align add_submonoid.closure_pow AddSubmonoid.closure_pow
 
-theorem pow_eq_closure_pow_set (s : AddSubmonoid R) (n : ℕ) : s ^ n = closure ((s : Set R) ^ n) :=
-  by rw [← closure_pow, closure_eq]
+theorem pow_eq_closure_pow_set (s : AddSubmonoid R) (n : ℕ) :
+    s ^ n = closure ((s : Set R) ^ n) := by
+  rw [← closure_pow, closure_eq]
 #align add_submonoid.pow_eq_closure_pow_set AddSubmonoid.pow_eq_closure_pow_set
 
 theorem pow_subset_pow {s : AddSubmonoid R} {n : ℕ} : (↑s : Set R) ^ n ⊆ ↑(s ^ n) :=

Mathlib/GroupTheory/Subsemigroup/Center.lean

@@ -62,13 +62,13 @@ variable {a b c : M} [Mul M]
 
 -- c.f. Commute.left_comm
 @[to_additive]
-protected theorem left_comm (h : IsMulCentral a) (b c) : a * (b * c) = b * (a * c) :=
-  by simp only [h.comm, h.right_assoc]
+protected theorem left_comm (h : IsMulCentral a) (b c) : a * (b * c) = b * (a * c) := by
+  simp only [h.comm, h.right_assoc]
 
 -- c.f. Commute.right_comm
 @[to_additive]
-protected theorem right_comm (h : IsMulCentral c) (a b) : a * b * c = a * c * b :=
-  by simp only [h.right_assoc, h.mid_assoc, h.comm]
+protected theorem right_comm (h : IsMulCentral c) (a b) : a * b * c = a * c * b := by
+  simp only [h.right_assoc, h.mid_assoc, h.comm]
 
 end IsMulCentral