chore: exactly 4 spaces in subsequent lines (#7296)

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

Mathlib/Algebra/Hom/Equiv/Basic.lean

@@ -561,7 +561,7 @@ protected theorem map_one {M N} [MulOneClass M] [MulOneClass N] (h : M ≃* N) :
 
 @[to_additive]
 protected theorem map_eq_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_eq_one_iff h
 #align mul_equiv.map_eq_one_iff MulEquiv.map_eq_one_iff
 #align add_equiv.map_eq_zero_iff AddEquiv.map_eq_zero_iff
@@ -718,15 +718,15 @@ def piSubsingleton {ι : Type*} (M : ι → Type*) [∀ j, Mul (M j)] [Subsingle
 /-- A multiplicative equivalence of groups preserves inversion. -/
 @[to_additive "An additive equivalence of additive groups preserves negation."]
 protected theorem map_inv [Group G] [DivisionMonoid H] (h : G ≃* H) (x : G) :
-  h x⁻¹ = (h x)⁻¹ :=
+    h x⁻¹ = (h x)⁻¹ :=
   _root_.map_inv h x
 #align mul_equiv.map_inv MulEquiv.map_inv
 #align add_equiv.map_neg AddEquiv.map_neg
 
 /-- A multiplicative equivalence of groups preserves division. -/
 @[to_additive "An additive equivalence of additive groups preserves subtractions."]
 protected theorem map_div [Group G] [DivisionMonoid H] (h : G ≃* H) (x y : G) :
-  h (x / y) = h x / h y :=
+    h (x / y) = h x / h y :=
   _root_.map_div h x y
 #align mul_equiv.map_div MulEquiv.map_div
 #align add_equiv.map_sub AddEquiv.map_sub

Mathlib/Algebra/Hom/Group/Defs.lean

@@ -917,14 +917,14 @@ protected theorem MonoidHom.map_one [MulOneClass M] [MulOneClass N] (f : M →*
 #align add_monoid_hom.map_zero AddMonoidHom.map_zero
 
 protected theorem MonoidWithZeroHom.map_one [MulZeroOneClass M] [MulZeroOneClass N] (f : M →*₀ N) :
-  f 1 = 1 := f.map_one'
+    f 1 = 1 := f.map_one'
 #align monoid_with_zero_hom.map_one MonoidWithZeroHom.map_one
 
 /-- If `f` is an additive monoid homomorphism then `f 0 = 0`. -/
 add_decl_doc AddMonoidHom.map_zero
 
 protected theorem MonoidWithZeroHom.map_zero [MulZeroOneClass M] [MulZeroOneClass N] (f : M →*₀ N) :
-  f 0 = 0 := f.map_zero'
+    f 0 = 0 := f.map_zero'
 #align monoid_with_zero_hom.map_zero MonoidWithZeroHom.map_zero
 
 @[to_additive]
@@ -936,7 +936,7 @@ protected theorem MulHom.map_mul [Mul M] [Mul N] (f : M →ₙ* N) (a b : M) : f
 /-- If `f` is a monoid homomorphism then `f (a * b) = f a * f b`. -/
 @[to_additive]
 protected theorem MonoidHom.map_mul [MulOneClass M] [MulOneClass N] (f : M →* N) (a b : M) :
-  f (a * b) = f a * f b := f.map_mul' a b
+    f (a * b) = f a * f b := f.map_mul' a b
 #align monoid_hom.map_mul MonoidHom.map_mul
 #align add_monoid_hom.map_add AddMonoidHom.map_add
 
@@ -1278,7 +1278,7 @@ theorem MonoidWithZeroHom.id_comp [MulZeroOneClass M] [MulZeroOneClass N] (f : M
 
 @[to_additive]
 protected theorem MonoidHom.map_pow [Monoid M] [Monoid N] (f : M →* N) (a : M) (n : ℕ) :
-  f (a ^ n) = f a ^ n := map_pow f a n
+    f (a ^ n) = f a ^ n := map_pow f a n
 #align monoid_hom.map_pow MonoidHom.map_pow
 #align add_monoid_hom.map_nsmul AddMonoidHom.map_nsmul
 
@@ -1428,29 +1428,29 @@ theorem comp_one [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : N →* P)
 
 /-- Group homomorphisms preserve inverse. -/
 @[to_additive "Additive group homomorphisms preserve negation."]
-protected theorem map_inv [Group α] [DivisionMonoid β] (f : α →* β) (a : α) :
-  f a⁻¹ = (f a)⁻¹ := map_inv f _
+protected theorem map_inv [Group α] [DivisionMonoid β] (f : α →* β) (a : α) : f a⁻¹ = (f a)⁻¹ :=
+  map_inv f _
 #align monoid_hom.map_inv MonoidHom.map_inv
 #align add_monoid_hom.map_neg AddMonoidHom.map_neg
 
 /-- Group homomorphisms preserve integer power. -/
 @[to_additive "Additive group homomorphisms preserve integer scaling."]
 protected theorem map_zpow [Group α] [DivisionMonoid β] (f : α →* β) (g : α) (n : ℤ) :
-  f (g ^ n) = f g ^ n := map_zpow f g n
+    f (g ^ n) = f g ^ n := map_zpow f g n
 #align monoid_hom.map_zpow MonoidHom.map_zpow
 #align add_monoid_hom.map_zsmul AddMonoidHom.map_zsmul
 
 /-- Group homomorphisms preserve division. -/
 @[to_additive "Additive group homomorphisms preserve subtraction."]
 protected theorem map_div [Group α] [DivisionMonoid β] (f : α →* β) (g h : α) :
-  f (g / h) = f g / f h := map_div f g h
+    f (g / h) = f g / f h := map_div f g h
 #align monoid_hom.map_div MonoidHom.map_div
 #align add_monoid_hom.map_sub AddMonoidHom.map_sub
 
 /-- Group homomorphisms preserve division. -/
 @[to_additive "Additive group homomorphisms preserve subtraction."]
 protected theorem map_mul_inv [Group α] [DivisionMonoid β] (f : α →* β) (g h : α) :
-  f (g * h⁻¹) = f g * (f h)⁻¹ := by simp
+    f (g * h⁻¹) = f g * (f h)⁻¹ := by simp
 #align monoid_hom.map_mul_inv MonoidHom.map_mul_inv
 #align add_monoid_hom.map_add_neg AddMonoidHom.map_add_neg
 

Mathlib/Algebra/Hom/Units.lean

@@ -497,7 +497,7 @@ protected theorem mul_eq_mul_of_div_eq_div (hb : IsUnit b) (hd : IsUnit d)
 
 @[to_additive]
 protected theorem div_eq_div_iff (hb : IsUnit b) (hd : IsUnit d) :
-  a / b = c / d ↔ a * d = c * b := by
+    a / b = c / d ↔ a * d = c * b := by
   rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
     hd.div_mul_cancel]
 #align is_unit.div_eq_div_iff IsUnit.div_eq_div_iff

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -135,7 +135,7 @@ initialize_simps_projections NonUnitalStarAlgHom
 
 @[simp]
 protected theorem coe_coe {F : Type*} [NonUnitalStarAlgHomClass F R A B] (f : F) :
-  ⇑(f : A →⋆ₙₐ[R] B) = f := rfl
+    ⇑(f : A →⋆ₙₐ[R] B) = f := rfl
 #align non_unital_star_alg_hom.coe_coe NonUnitalStarAlgHom.coe_coe
 
 @[simp]

Mathlib/Control/Traversable/Instances.lean

@@ -162,7 +162,7 @@ protected theorem traverse_map {α β γ : Type u} (g : α → β) (f : β → G
 variable [LawfulApplicative F] [LawfulApplicative G]
 
 protected theorem id_traverse {σ α} (x : σ ⊕ α) :
-  Sum.traverse (pure : α → Id α) x = x := by cases x <;> rfl
+    Sum.traverse (pure : α → Id α) x = x := by cases x <;> rfl
 #align sum.id_traverse Sum.id_traverse
 
 protected theorem comp_traverse {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : σ ⊕ α) :

Mathlib/Data/Analysis/Topology.lean

@@ -130,7 +130,7 @@ protected theorem is_basis [T : TopologicalSpace α] (F : Realizer α) :
 #align ctop.realizer.is_basis Ctop.Realizer.is_basis
 
 protected theorem mem_nhds [T : TopologicalSpace α] (F : Realizer α) {s : Set α} {a : α} :
-  s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F b ∧ F.F b ⊆ s := by
+    s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F b ∧ F.F b ⊆ s := by
   have := @mem_nhds_toTopsp _ _ F.F s a; rwa [F.eq] at this
 #align ctop.realizer.mem_nhds Ctop.Realizer.mem_nhds
 

Mathlib/Data/Countable/Defs.lean

@@ -46,13 +46,13 @@ instance : Countable ℕ :=
 export Countable (exists_injective_nat)
 
 protected theorem Function.Injective.countable [Countable β] {f : α → β} (hf : Injective f) :
-  Countable α :=
+    Countable α :=
   let ⟨g, hg⟩ := exists_injective_nat β
   ⟨⟨g ∘ f, hg.comp hf⟩⟩
 #align function.injective.countable Function.Injective.countable
 
 protected theorem Function.Surjective.countable [Countable α] {f : α → β} (hf : Surjective f) :
-  Countable β :=
+    Countable β :=
   (injective_surjInv hf).countable
 #align function.surjective.countable Function.Surjective.countable
 

Mathlib/FieldTheory/RatFunc.lean

@@ -281,7 +281,7 @@ See also `induction_on`, which is a recursion principle defined in terms of `alg
 -/
 @[elab_as_elim]
 protected theorem induction_on' {P : RatFunc K → Prop} :
-  ∀ (x : RatFunc K) (_pq : ∀ (p q : K[X]) (_ : q ≠ 0), P (RatFunc.mk p q)), P x
+    ∀ (x : RatFunc K) (_pq : ∀ (p q : K[X]) (_ : q ≠ 0), P (RatFunc.mk p q)), P x
   | ⟨x⟩, f =>
     Localization.induction_on x fun ⟨p, q⟩ => by
       simpa only [mk_coe_def, Localization.mk_eq_mk'] using

Mathlib/LinearAlgebra/TensorProduct/Tower.lean

@@ -214,7 +214,7 @@ theorem map_comp (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) (g₂ : Q →ₗ
 protected theorem map_one : map (1 : M →ₗ[A] M) (1 : N →ₗ[R] N) = 1 := map_id
 
 protected theorem map_mul (f₁ f₂ : M →ₗ[A] M) (g₁ g₂ : N →ₗ[R] N) :
-  map (f₁ * f₂) (g₁ * g₂) = map f₁ g₁ * map f₂ g₂ := map_comp _ _ _ _
+    map (f₁ * f₂) (g₁ * g₂) = map f₁ g₁ * map f₂ g₂ := map_comp _ _ _ _
 
 theorem map_add_left (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) :
     map (f₁ + f₂) g = map f₁ g + map f₂ g := by

Mathlib/Order/Filter/Bases.lean

@@ -286,7 +286,7 @@ protected theorem IsBasis.hasBasis (h : IsBasis p s) : HasBasis h.filter p s :=
 #align filter.is_basis.has_basis Filter.IsBasis.hasBasis
 
 protected theorem HasBasis.mem_of_superset (hl : l.HasBasis p s) (hi : p i) (ht : s i ⊆ t) :
-     t ∈ l :=
+    t ∈ l :=
   hl.mem_iff.2 ⟨i, hi, ht⟩
 #align filter.has_basis.mem_of_superset Filter.HasBasis.mem_of_superset