chore: only four spaces for subsequent lines (#7286)

Co-authored-by: Moritz Firsching <firsching@google.com>

Counterexamples/SorgenfreyLine.lean

@@ -286,7 +286,7 @@ theorem nhds_prod_antitone_basis_inv_pnat (x y : ℝₗ) :
 /-- The sets of rational and irrational points of the antidiagonal `{(x, y) | x + y = 0}` cannot be
 separated by open neighborhoods. This implies that `ℝₗ × ℝₗ` is not a normal space. -/
 theorem not_separatedNhds_rat_irrational_antidiag :
-  ¬SeparatedNhds {x : ℝₗ × ℝₗ | x.1 + x.2 = 0 ∧ ∃ r : ℚ, ↑r = x.1}
+    ¬SeparatedNhds {x : ℝₗ × ℝₗ | x.1 + x.2 = 0 ∧ ∃ r : ℚ, ↑r = x.1}
     {x : ℝₗ × ℝₗ | x.1 + x.2 = 0 ∧ Irrational (toReal x.1)} := by
   have h₀ : ∀ {n : ℕ+}, 0 < (n : ℝ)⁻¹ := inv_pos.2 (Nat.cast_pos.2 (PNat.pos _))
   have h₀' : ∀ {n : ℕ+} {x : ℝ}, x < x + (n : ℝ)⁻¹ := lt_add_of_pos_right _ h₀

Mathlib/Algebra/Algebra/Operations.lean

@@ -638,7 +638,7 @@ instance moduleSet : Module (SetSemiring A) (Submodule R A) where
 variable {R A}
 
 theorem smul_def (s : SetSemiring A) (P : Submodule R A) :
-  s • P = span R (SetSemiring.down s) * P :=
+    s • P = span R (SetSemiring.down s) * P :=
   rfl
 #align submodule.smul_def Submodule.smul_def
 

Mathlib/Algebra/Category/GroupCat/Preadditive.lean

@@ -24,8 +24,7 @@ instance (P Q : AddCommGroupCat) : AddCommGroup (P ⟶ Q) :=
 
 -- porting note: this lemma was not necessary in mathlib
 @[simp]
-lemma hom_add_apply {P Q : AddCommGroupCat} (f g : P ⟶ Q) (x : P) :
-  (f + g) x = f x + g x := rfl
+lemma hom_add_apply {P Q : AddCommGroupCat} (f g : P ⟶ Q) (x : P) : (f + g) x = f x + g x := rfl
 
 section
 

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -145,7 +145,7 @@ add_decl_doc AddMonCat.ofHom
 
 @[to_additive (attr := simp)]
 lemma ofHom_apply {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) (x : X) :
-  (ofHom f) x = f x := rfl
+    (ofHom f) x = f x := rfl
 set_option linter.uppercaseLean3 false in
 #align Mon.of_hom_apply MonCat.ofHom_apply
 
@@ -278,7 +278,7 @@ add_decl_doc AddCommMonCat.ofHom
 
 @[to_additive (attr := simp)]
 lemma ofHom_apply {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) (x : X) :
-  (ofHom f) x = f x := rfl
+    (ofHom f) x = f x := rfl
 
 end CommMonCat
 

Mathlib/Algebra/Category/Ring/Colimits.lean

@@ -190,9 +190,11 @@ theorem quot_one : Quot.mk Setoid.r one = (1 : ColimitType F) :=
 
 @[simp]
 theorem quot_neg (x : Prequotient F) :
--- Porting note : Lean can't see `Quot.mk Setoid.r x` is a `ColimitType F` even with type annotation
--- so use `Neg.neg (α := ColimitType F)` to tell Lean negation happens inside `ColimitType F`.
-  (Quot.mk Setoid.r (neg x) : ColimitType F) = Neg.neg (α := ColimitType F) (Quot.mk Setoid.r x) :=
+    -- Porting note : Lean can't see `Quot.mk Setoid.r x` is a `ColimitType F` even with type
+    -- annotation so use `Neg.neg (α := ColimitType F)` to tell Lean negation happens inside
+    -- `ColimitType F`.
+    (Quot.mk Setoid.r (neg x) : ColimitType F) =
+    Neg.neg (α := ColimitType F) (Quot.mk Setoid.r x) :=
   rfl
 #align CommRing.colimits.quot_neg CommRingCat.Colimits.quot_neg
 

Mathlib/Algebra/CharP/Basic.lean

@@ -110,7 +110,7 @@ class CharP [AddMonoidWithOne R] (p : ℕ) : Prop where
 -- porting note: the field of the structure had implicit arguments where they were
 -- explicit in Lean 3
 theorem CharP.cast_eq_zero_iff (R : Type u) [AddMonoidWithOne R] (p : ℕ) [CharP R p] (x : ℕ) :
-  (x : R) = 0 ↔ p ∣ x :=
+    (x : R) = 0 ↔ p ∣ x :=
 CharP.cast_eq_zero_iff' (R := R) (p := p) x
 
 @[simp]

Mathlib/Algebra/DirectSum/Decomposition.lean

@@ -137,7 +137,7 @@ lemma decomposeAddEquiv_apply (a : M) :
 
 @[simp]
 lemma decomposeAddEquiv_symm_apply (a : ⨁ i, ℳ i) :
-  (decomposeAddEquiv ℳ).symm a = (decompose ℳ).symm a := rfl
+    (decomposeAddEquiv ℳ).symm a = (decompose ℳ).symm a := rfl
 
 @[simp]
 theorem decompose_zero : decompose ℳ (0 : M) = 0 :=

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -248,8 +248,7 @@ theorem out_top : (⊤ : Associates α).out = 0 :=
 
 -- Porting note: lower priority to avoid linter complaints about simp-normal form
 @[simp 1100]
-theorem normalize_out (a : Associates α) :
-  normalize a.out = a.out :=
+theorem normalize_out (a : Associates α) : normalize a.out = a.out :=
   Quotient.inductionOn a normalize_idem
 #align associates.normalize_out Associates.normalize_out
 
@@ -313,8 +312,7 @@ variable [CancelCommMonoidWithZero α]
 
 -- Porting note: lower priority to avoid linter complaints about simp-normal form
 @[simp 1100]
-theorem normalize_gcd [NormalizedGCDMonoid α] :
-  ∀ a b : α, normalize (gcd a b) = gcd a b :=
+theorem normalize_gcd [NormalizedGCDMonoid α] : ∀ a b : α, normalize (gcd a b) = gcd a b :=
   NormalizedGCDMonoid.normalize_gcd
 #align normalize_gcd normalize_gcd
 
@@ -733,8 +731,7 @@ theorem lcm_eq_zero_iff [GCDMonoid α] (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b
 
 -- Porting note: lower priority to avoid linter complaints about simp-normal form
 @[simp 1100]
-theorem normalize_lcm [NormalizedGCDMonoid α] (a b : α) :
-  normalize (lcm a b) = lcm a b :=
+theorem normalize_lcm [NormalizedGCDMonoid α] (a b : α) : normalize (lcm a b) = lcm a b :=
   NormalizedGCDMonoid.normalize_lcm a b
 #align normalize_lcm normalize_lcm
 

Mathlib/Algebra/Group/Commutator.lean

@@ -18,6 +18,6 @@ instance commutatorElement {G : Type*} [Group G] : Bracket G G :=
 #align commutator_element commutatorElement
 
 theorem commutatorElement_def {G : Type*} [Group G] (g₁ g₂ : G) :
-  ⁅g₁, g₂⁆ = g₁ * g₂ * g₁⁻¹ * g₂⁻¹ :=
+    ⁅g₁, g₂⁆ = g₁ * g₂ * g₁⁻¹ * g₂⁻¹ :=
   rfl
 #align commutator_element_def commutatorElement_def

Mathlib/Algebra/Group/Defs.lean

@@ -961,7 +961,7 @@ theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻
 #align zpow_neg_succ_of_nat zpow_negSucc
 
 theorem negSucc_zsmul {G} [SubNegMonoid G] (a : G) (n : ℕ) :
-  Int.negSucc n • a = -((n + 1) • a) := by
+    Int.negSucc n • a = -((n + 1) • a) := by
   rw [← ofNat_zsmul]
   exact SubNegMonoid.zsmul_neg' n a
 #align zsmul_neg_succ_of_nat negSucc_zsmul

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -1130,7 +1130,7 @@ theorem cast_int_mul_right (h : Commute a b) (m : ℤ) : Commute a (m * b : R) :
 
 @[simp]
 theorem cast_int_mul_left (h : Commute a b) (m : ℤ) :
-   Commute ((m : R) * a) b :=
+    Commute ((m : R) * a) b :=
   SemiconjBy.cast_int_mul_left h m
 #align commute.cast_int_mul_left Commute.cast_int_mul_left
 
@@ -1209,14 +1209,13 @@ namespace Units
 variable [Monoid M]
 
 theorem conj_pow (u : Mˣ) (x : M) (n : ℕ) :
-      ((↑u : M) * x * (↑u⁻¹ : M)) ^ n =
-      (u : M) * x ^ n * (↑u⁻¹ : M) :=
+    ((↑u : M) * x * (↑u⁻¹ : M)) ^ n = (u : M) * x ^ n * (↑u⁻¹ : M) :=
   (divp_eq_iff_mul_eq.2
   ((u.mk_semiconjBy x).pow_right n).eq.symm).symm
 #align units.conj_pow Units.conj_pow
 
 theorem conj_pow' (u : Mˣ) (x : M) (n : ℕ) :
-  ((↑u⁻¹ : M) * x * (u : M)) ^ n = (↑u⁻¹ : M) * x ^ n * (u : M) :=
+    ((↑u⁻¹ : M) * x * (u : M)) ^ n = (↑u⁻¹ : M) * x ^ n * (u : M) :=
   u⁻¹.conj_pow x n
 #align units.conj_pow' Units.conj_pow'
 

Mathlib/Algebra/Hom/Equiv/Basic.lean

@@ -165,13 +165,13 @@ variable {F}
 
 @[to_additive (attr := simp)]
 theorem map_eq_one_iff {M N} [MulOneClass M] [MulOneClass N] [MulEquivClass F M N] (h : F) {x : M} :
-  h x = 1 ↔ x = 1 := _root_.map_eq_one_iff h (EquivLike.injective h)
+    h x = 1 ↔ x = 1 := _root_.map_eq_one_iff h (EquivLike.injective h)
 #align mul_equiv_class.map_eq_one_iff MulEquivClass.map_eq_one_iff
 #align add_equiv_class.map_eq_zero_iff AddEquivClass.map_eq_zero_iff
 
 @[to_additive]
 theorem map_ne_one_iff {M N} [MulOneClass M] [MulOneClass N] [MulEquivClass F M N] (h : F) {x : M} :
-  h x ≠ 1 ↔ x ≠ 1 := _root_.map_ne_one_iff h (EquivLike.injective h)
+    h x ≠ 1 ↔ x ≠ 1 := _root_.map_ne_one_iff h (EquivLike.injective h)
 #align mul_equiv_class.map_ne_one_iff MulEquivClass.map_ne_one_iff
 #align add_equiv_class.map_ne_zero_iff AddEquivClass.map_ne_zero_iff
 
@@ -344,7 +344,7 @@ theorem symm_bijective : Function.Bijective (symm : M ≃* N → N ≃* M) :=
 -- because the signature of `MulEquiv.mk` has changed.
 @[to_additive (attr := simp)]
 theorem symm_mk (f : M ≃ N) (h) :
-  (MulEquiv.mk f h).symm = ⟨f.symm, (MulEquiv.mk f h).symm.map_mul'⟩ := rfl
+    (MulEquiv.mk f h).symm = ⟨f.symm, (MulEquiv.mk f h).symm.map_mul'⟩ := rfl
 #align mul_equiv.symm_mk MulEquiv.symm_mkₓ
 #align add_equiv.symm_mk AddEquiv.symm_mkₓ
 
@@ -410,7 +410,7 @@ theorem trans_apply (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) : e₁.trans e
 
 @[to_additive (attr := simp)]
 theorem symm_trans_apply (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :
-  (e₁.trans e₂).symm p = e₁.symm (e₂.symm p) := rfl
+    (e₁.trans e₂).symm p = e₁.symm (e₂.symm p) := rfl
 #align mul_equiv.symm_trans_apply MulEquiv.symm_trans_apply
 #align add_equiv.symm_trans_apply AddEquiv.symm_trans_apply
 
@@ -441,28 +441,28 @@ theorem eq_symm_apply (e : M ≃* N) {x y} : y = e.symm x ↔ e y = x :=
 
 @[to_additive]
 theorem eq_comp_symm {α : Type*} (e : M ≃* N) (f : N → α) (g : M → α) :
-  f = g ∘ e.symm ↔ f ∘ e = g :=
+    f = g ∘ e.symm ↔ f ∘ e = g :=
   e.toEquiv.eq_comp_symm f g
 #align mul_equiv.eq_comp_symm MulEquiv.eq_comp_symm
 #align add_equiv.eq_comp_symm AddEquiv.eq_comp_symm
 
 @[to_additive]
 theorem comp_symm_eq {α : Type*} (e : M ≃* N) (f : N → α) (g : M → α) :
-  g ∘ e.symm = f ↔ g = f ∘ e :=
+    g ∘ e.symm = f ↔ g = f ∘ e :=
   e.toEquiv.comp_symm_eq f g
 #align mul_equiv.comp_symm_eq MulEquiv.comp_symm_eq
 #align add_equiv.comp_symm_eq AddEquiv.comp_symm_eq
 
 @[to_additive]
 theorem eq_symm_comp {α : Type*} (e : M ≃* N) (f : α → M) (g : α → N) :
-  f = e.symm ∘ g ↔ e ∘ f = g :=
+    f = e.symm ∘ g ↔ e ∘ f = g :=
   e.toEquiv.eq_symm_comp f g
 #align mul_equiv.eq_symm_comp MulEquiv.eq_symm_comp
 #align add_equiv.eq_symm_comp AddEquiv.eq_symm_comp
 
 @[to_additive]
 theorem symm_comp_eq {α : Type*} (e : M ≃* N) (f : α → M) (g : α → N) :
-  e.symm ∘ g = f ↔ g = e ∘ f :=
+    e.symm ∘ g = f ↔ g = e ∘ f :=
   e.toEquiv.symm_comp_eq f g
 #align mul_equiv.symm_comp_eq MulEquiv.symm_comp_eq
 #align add_equiv.symm_comp_eq AddEquiv.symm_comp_eq
@@ -568,7 +568,7 @@ protected theorem map_eq_one_iff {M N} [MulOneClass M] [MulOneClass N] (h : M 
 
 @[to_additive]
 theorem map_ne_one_iff {M N} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} :
-  h x ≠ 1 ↔ x ≠ 1 :=
+    h x ≠ 1 ↔ x ≠ 1 :=
   MulEquivClass.map_ne_one_iff h
 #align mul_equiv.map_ne_one_iff MulEquiv.map_ne_one_iff
 #align add_equiv.map_ne_zero_iff AddEquiv.map_ne_zero_iff
@@ -604,14 +604,14 @@ def toMonoidHom {M N} [MulOneClass M] [MulOneClass N] (h : M ≃* N) : M →* N
 
 @[to_additive (attr := simp)]
 theorem coe_toMonoidHom {M N} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
-  ⇑e.toMonoidHom = e := rfl
+    ⇑e.toMonoidHom = e := rfl
 #align mul_equiv.coe_to_monoid_hom MulEquiv.coe_toMonoidHom
 #align add_equiv.coe_to_add_monoid_hom AddEquiv.coe_toAddMonoidHom
 
 set_option linter.deprecated false in
 @[to_additive]
 theorem toMonoidHom_injective {M N} [MulOneClass M] [MulOneClass N] :
-  Function.Injective (toMonoidHom : M ≃* N → M →* N) :=
+    Function.Injective (toMonoidHom : M ≃* N → M →* N) :=
   fun _ _ h => MulEquiv.ext (MonoidHom.ext_iff.1 h)
 #align mul_equiv.to_monoid_hom_injective MulEquiv.toMonoidHom_injective
 #align add_equiv.to_add_monoid_hom_injective AddEquiv.toAddMonoidHom_injective
@@ -679,7 +679,7 @@ def piCongrRight {η : Type*} {Ms Ns : η → Type*} [∀ j, Mul (Ms j)] [∀ j,
 
 @[to_additive (attr := simp)]
 theorem piCongrRight_refl {η : Type*} {Ms : η → Type*} [∀ j, Mul (Ms j)] :
-  (piCongrRight fun j => MulEquiv.refl (Ms j)) = MulEquiv.refl _ := rfl
+    (piCongrRight fun j => MulEquiv.refl (Ms j)) = MulEquiv.refl _ := rfl
 #align mul_equiv.Pi_congr_right_refl MulEquiv.piCongrRight_refl
 #align add_equiv.Pi_congr_right_refl AddEquiv.piCongrRight_refl
 

Mathlib/Algebra/Hom/Group/Basic.lean

@@ -80,19 +80,19 @@ instance [Mul M] [CommSemigroup N] : Mul (M →ₙ* N) :=
 
 @[to_additive (attr := simp)]
 theorem mul_apply {M N} [Mul M] [CommSemigroup N] (f g : M →ₙ* N) (x : M) :
-  (f * g) x = f x * g x := rfl
+    (f * g) x = f x * g x := rfl
 #align mul_hom.mul_apply MulHom.mul_apply
 #align add_hom.add_apply AddHom.add_apply
 
 @[to_additive]
 theorem mul_comp [Mul M] [Mul N] [CommSemigroup P] (g₁ g₂ : N →ₙ* P) (f : M →ₙ* N) :
-  (g₁ * g₂).comp f = g₁.comp f * g₂.comp f := rfl
+    (g₁ * g₂).comp f = g₁.comp f * g₂.comp f := rfl
 #align mul_hom.mul_comp MulHom.mul_comp
 #align add_hom.add_comp AddHom.add_comp
 
 @[to_additive]
 theorem comp_mul [Mul M] [CommSemigroup N] [CommSemigroup P] (g : N →ₙ* P) (f₁ f₂ : M →ₙ* N) :
-  g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ := by
+    g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ := by
   ext
   simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]
 #align mul_hom.comp_mul MulHom.comp_mul
@@ -122,19 +122,19 @@ add_decl_doc AddMonoidHom.add
 
 @[to_additive (attr := simp)]
 theorem mul_apply {M N} [MulOneClass M] [CommMonoid N] (f g : M →* N) (x : M) :
-  (f * g) x = f x * g x := rfl
+    (f * g) x = f x * g x := rfl
 #align monoid_hom.mul_apply MonoidHom.mul_apply
 #align add_monoid_hom.add_apply AddMonoidHom.add_apply
 
 @[to_additive]
 theorem mul_comp [MulOneClass M] [MulOneClass N] [CommMonoid P] (g₁ g₂ : N →* P) (f : M →* N) :
-  (g₁ * g₂).comp f = g₁.comp f * g₂.comp f := rfl
+    (g₁ * g₂).comp f = g₁.comp f * g₂.comp f := rfl
 #align monoid_hom.mul_comp MonoidHom.mul_comp
 #align add_monoid_hom.add_comp AddMonoidHom.add_comp
 
 @[to_additive]
 theorem comp_mul [MulOneClass M] [CommMonoid N] [CommMonoid P] (g : N →* P) (f₁ f₂ : M →* N) :
-  g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ := by
+    g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ := by
   ext
   simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]
 #align monoid_hom.comp_mul MonoidHom.comp_mul
@@ -204,7 +204,7 @@ def ofMapDiv {H : Type*} [Group H] (f : G → H) (hf : ∀ x y, f (x / y) = f x
 
 @[to_additive (attr := simp)]
 theorem coe_of_map_div {H : Type*} [Group H] (f : G → H) (hf : ∀ x y, f (x / y) = f x / f y) :
-  ↑(ofMapDiv f hf) = f := rfl
+    ↑(ofMapDiv f hf) = f := rfl
 #align monoid_hom.coe_of_map_div MonoidHom.coe_of_map_div
 #align add_monoid_hom.coe_of_map_sub AddMonoidHom.coe_of_map_sub
 
@@ -217,7 +217,7 @@ instance {M G} [MulOneClass M] [CommGroup G] : Inv (M →* G) :=
 
 @[to_additive (attr := simp)]
 theorem inv_apply {M G} [MulOneClass M] [CommGroup G] (f : M →* G) (x : M) :
-  f⁻¹ x = (f x)⁻¹ := rfl
+    f⁻¹ x = (f x)⁻¹ := rfl
 #align monoid_hom.inv_apply MonoidHom.inv_apply
 #align add_monoid_hom.neg_apply AddMonoidHom.neg_apply
 
@@ -247,7 +247,7 @@ instance {M G} [MulOneClass M] [CommGroup G] : Div (M →* G) :=
 
 @[to_additive (attr := simp)]
 theorem div_apply {M G} [MulOneClass M] [CommGroup G] (f g : M →* G) (x : M) :
-  (f / g) x = f x / g x := rfl
+    (f / g) x = f x / g x := rfl
 #align monoid_hom.div_apply MonoidHom.div_apply
 #align add_monoid_hom.sub_apply AddMonoidHom.sub_apply