chore: formatting issues (#4947)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib/Algebra/Algebra/Equiv.lean

@@ -660,10 +660,10 @@ instance aut : Group (A₁ ≃ₐ[R] A₁) where
   mul_left_inv ϕ := ext <| symm_apply_apply ϕ
 #align alg_equiv.aut AlgEquiv.aut
 
-theorem aut_mul (ϕ ψ : A₁ ≃ₐ[R] A₁): ϕ * ψ = ψ.trans ϕ :=
+theorem aut_mul (ϕ ψ : A₁ ≃ₐ[R] A₁) : ϕ * ψ = ψ.trans ϕ :=
   rfl
 
-theorem aut_one : 1 = AlgEquiv.refl (R:= R) (A₁ := A₁) :=
+theorem aut_one : 1 = AlgEquiv.refl (R := R) (A₁ := A₁) :=
   rfl
 
 @[simp]

Mathlib/Algebra/Algebra/Hom.lean

@@ -77,9 +77,9 @@ instance (priority := 100) linearMapClass [AlgHomClass F R A B] : LinearMapClass
 `AlgHom`. This is declared as the default coercion from `F` to `α →+* β`. -/
 @[coe]
 def toAlgHom {F : Type _} [AlgHomClass F R A B] (f : F) : A →ₐ[R] B :=
-{ (f : A →+* B) with
-    toFun := f
-    commutes' := AlgHomClass.commutes f }
+  { (f : A →+* B) with
+      toFun := f
+      commutes' := AlgHomClass.commutes f }
 
 instance coeTC {F : Type _} [AlgHomClass F R A B] : CoeTC F (A →ₐ[R] B) :=
   ⟨AlgHomClass.toAlgHom⟩

Mathlib/Algebra/Algebra/Operations.lean

@@ -81,7 +81,7 @@ variable (S T : Set A) {M N P Q : Submodule R A} {m n : A}
 
 /-- `1 : Submodule R A` is the submodule R of A. -/
 instance one : One (Submodule R A) :=
--- porting note: `f.range` notation doesn't work
+  -- porting note: `f.range` notation doesn't work
   ⟨LinearMap.range (Algebra.linearMap R A)⟩
 #align submodule.has_one Submodule.one
 

Mathlib/Algebra/BigOperators/Order.lean

@@ -397,7 +397,7 @@ section CanonicallyOrderedMonoid
 
 variable [CanonicallyOrderedMonoid M] {f : ι → M} {s t : Finset ι}
 
-@[to_additive (attr:=simp) sum_eq_zero_iff]
+@[to_additive (attr := simp) sum_eq_zero_iff]
 theorem prod_eq_one_iff' : (∏ x in s, f x) = 1 ↔ ∀ x ∈ s, f x = 1 :=
   prod_eq_one_iff_of_one_le' fun x _ ↦ one_le (f x)
 #align finset.prod_eq_one_iff' Finset.prod_eq_one_iff'

Mathlib/Algebra/BigOperators/Pi.lean

@@ -41,7 +41,7 @@ theorem multiset_prod_apply {α : Type _} {β : α → Type _} [∀ a, CommMonoi
 
 end Pi
 
-@[to_additive (attr:=simp)]
+@[to_additive (attr := simp)]
 theorem Finset.prod_apply {α : Type _} {β : α → Type _} {γ} [∀ a, CommMonoid (β a)] (a : α)
     (s : Finset γ) (g : γ → ∀ a, β a) : (∏ c in s, g c) a = ∏ c in s, g c a :=
   (Pi.evalMonoidHom β a).map_prod _ _

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -67,7 +67,7 @@ instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
 
 @[to_additive]
 instance FunLike_instance (X Y : GroupCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
-show FunLike (X →* Y) X (fun _ => Y) from inferInstance
+  show FunLike (X →* Y) X (fun _ => Y) from inferInstance
 
 -- porting note: added
 @[to_additive (attr := simp)]
@@ -213,7 +213,7 @@ instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
 
 @[to_additive]
 instance FunLike_instance (X Y : CommGroupCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
-show FunLike (X →* Y) X (fun _ => Y) from inferInstance
+  show FunLike (X →* Y) X (fun _ => Y) from inferInstance
 
 -- porting note: added
 @[to_additive (attr := simp)]

Mathlib/Algebra/Category/GroupCat/Colimits.lean

@@ -112,7 +112,7 @@ def ColimitType : Type v :=
 #align AddCommGroup.colimits.colimit_type AddCommGroupCat.Colimits.ColimitType
 
 instance ColimitTypeInhabited : Inhabited (ColimitType.{v} F) :=
-⟨Quot.mk _ zero⟩
+  ⟨Quot.mk _ zero⟩
 
 instance : AddCommGroup (ColimitType F) where
   zero := Quot.mk _ zero

Mathlib/Algebra/Category/Mon/FilteredColimits.lean

@@ -72,7 +72,7 @@ set_option linter.uppercaseLean3 false in
 
 @[to_additive]
 theorem M.mk_eq (x y : Σ j, F.obj j)
-    (h : ∃ (k : J)(f : x.1 ⟶ k)(g : y.1 ⟶ k), F.map f x.2 = F.map g y.2) :
+    (h : ∃ (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k), F.map f x.2 = F.map g y.2) :
   M.mk.{v, u} F x = M.mk F y :=
   Quot.EqvGen_sound (Types.FilteredColimit.eqvGen_quot_rel_of_rel (F ⋙ forget MonCat) x y h)
 set_option linter.uppercaseLean3 false in

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -87,7 +87,7 @@ instance {X Y : MonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
 
 @[to_additive]
 instance Hom_FunLike (X Y : MonCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
-show FunLike (X →* Y) X (fun _ => Y) by infer_instance
+  show FunLike (X →* Y) X (fun _ => Y) by infer_instance
 
 -- porting note: added
 @[to_additive (attr := simp)]
@@ -208,7 +208,7 @@ instance {X Y : CommMonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
 
 @[to_additive]
 instance Hom_FunLike (X Y : CommMonCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
-show FunLike (X →* Y) X (fun _ => Y) by infer_instance
+  show FunLike (X →* Y) X (fun _ => Y) by infer_instance
 
 -- porting note: added
 @[to_additive (attr := simp)]

Mathlib/Algebra/Category/Ring/Limits.lean

@@ -52,13 +52,13 @@ set_option linter.uppercaseLean3 false in
 /-- The flat sections of a functor into `SemiRing` form a subsemiring of all sections.
 -/
 def sectionsSubsemiring (F : J ⥤ SemiRingCatMax.{v, u}) : Subsemiring.{max v u} (∀ j, F.obj j) :=
--- Porting note : if `f` and `g` were inlined, it does not compile
-letI f : J ⥤ AddMonCat.{max v u} := F ⋙ forget₂ SemiRingCatMax.{v, u} AddCommMonCat.{max v u} ⋙
-  forget₂ AddCommMonCat AddMonCat
-letI g : J ⥤ MonCat.{max v u} := F ⋙ forget₂ SemiRingCatMax.{v, u} MonCat.{max v u}
-{ (MonCat.sectionsSubmonoid.{v, u} (J := J) g),
-  (AddMonCat.sectionsAddSubmonoid.{v, u} (J := J) f) with
-  carrier := (F ⋙ forget SemiRingCat).sections }
+  -- Porting note : if `f` and `g` were inlined, it does not compile
+  letI f : J ⥤ AddMonCat.{max v u} := F ⋙ forget₂ SemiRingCatMax.{v, u} AddCommMonCat.{max v u} ⋙
+    forget₂ AddCommMonCat AddMonCat
+  letI g : J ⥤ MonCat.{max v u} := F ⋙ forget₂ SemiRingCatMax.{v, u} MonCat.{max v u}
+  { (MonCat.sectionsSubmonoid.{v, u} (J := J) g),
+    (AddMonCat.sectionsAddSubmonoid.{v, u} (J := J) f) with
+    carrier := (F ⋙ forget SemiRingCat).sections }
 set_option linter.uppercaseLean3 false in
 #align SemiRing.sections_subsemiring SemiRingCat.sectionsSubsemiring
 
@@ -72,7 +72,7 @@ set_option linter.uppercaseLean3 false in
 def limitπRingHom (F : J ⥤ SemiRingCatMax.{v, u}) (j) :
     (Types.limitCone.{v, u} (F ⋙ forget SemiRingCat)).pt →+* (F ⋙ forget SemiRingCat).obj j :=
   -- Porting note : if `f` and `g` were inlined, it does not compile
-  letI f : J ⥤ AddMonCat.{max v u}:= F ⋙ forget₂ SemiRingCatMax.{v, u} AddCommMonCat.{max v u} ⋙
+  letI f : J ⥤ AddMonCat.{max v u} := F ⋙ forget₂ SemiRingCatMax.{v, u} AddCommMonCat.{max v u} ⋙
     forget₂ AddCommMonCat AddMonCat
   { AddMonCat.limitπAddMonoidHom f j,
     MonCat.limitπMonoidHom (F ⋙ forget₂ SemiRingCat MonCat.{max v u}) j with

Mathlib/Algebra/DirectLimit.lean

@@ -91,7 +91,7 @@ def DirectLimit : Type max v w :=
   DirectSum ι G ⧸
     (span R <|
       { a |
-        ∃ (i j : _)(H : i ≤ j)(x : _),
+        ∃ (i j : _) (H : i ≤ j) (x : _),
           DirectSum.lof R ι G i x - DirectSum.lof R ι G j (f i j H x) = a })
 #align module.direct_limit Module.DirectLimit
 
@@ -615,7 +615,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
 /-- A component that corresponds to zero in the direct limit is already zero in some
 bigger module in the directed system. -/
 theorem of.zero_exact [IsDirected ι (· ≤ ·)] {i x} (hix : of G (fun i j h => f' i j h) i x = 0) :
-    ∃ (j : _)(hij : i ≤ j), f' i j hij x = 0 :=
+    ∃ (j : _) (hij : i ≤ j), f' i j hij x = 0 :=
   haveI : Nonempty ι := ⟨i⟩
   let ⟨j, s, H, hxs, hx⟩ := of.zero_exact_aux hix
   have hixs : (⟨i, x⟩ : Σi, G i) ∈ s := isSupported_of.1 hxs

Mathlib/Algebra/DirectSum/Module.lean

@@ -320,8 +320,8 @@ def coeLinearMap : (⨁ i, A i) →ₗ[R] M :=
 
 @[simp]
 theorem coeLinearMap_of (i : ι) (x : A i) : DirectSum.coeLinearMap A (of (fun i ↦ A i) i x) = x :=
--- Porting note: spelled out arguments. (I don't know how this works.)
-toAddMonoid_of (β := fun i => A i) (fun i ↦ ((A i).subtype : A i →+ M)) i x
+  -- Porting note: spelled out arguments. (I don't know how this works.)
+  toAddMonoid_of (β := fun i => A i) (fun i ↦ ((A i).subtype : A i →+ M)) i x
 #align direct_sum.coe_linear_map_of DirectSum.coeLinearMap_of
 
 variable {A}

Mathlib/Algebra/Free.lean

@@ -444,19 +444,19 @@ end Magma
 
 /-- Free additive semigroup over a given alphabet. -/
 structure FreeAddSemigroup (α : Type u) where
-/-- The head of the element -/
+  /-- The head of the element -/
   head : α
-/-- The tail of the element -/
+  /-- The tail of the element -/
   tail : List α
 #align free_add_semigroup FreeAddSemigroup
 compile_inductive% FreeAddSemigroup
 
 /-- Free semigroup over a given alphabet. -/
 @[to_additive (attr := ext)]
 structure FreeSemigroup (α : Type u) where
-/-- The head of the element -/
+  /-- The head of the element -/
   head : α
-/-- The tail of the element -/
+  /-- The tail of the element -/
   tail : List α
 #align free_semigroup FreeSemigroup
 compile_inductive% FreeSemigroup

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -240,7 +240,7 @@ def lift : (α → M) ≃ (FreeMonoid α →* M) where
 -- porting note: new
 @[to_additive (attr := simp)]
 theorem lift_ofList (f : α → M) (l : List α) : lift f (ofList l) = (l.map f).prod :=
-prodAux_eq _
+  prodAux_eq _
 
 @[to_additive (attr := simp)]
 theorem lift_symm_apply (f : FreeMonoid α →* M) : lift.symm f = f ∘ of := rfl
@@ -249,7 +249,7 @@ theorem lift_symm_apply (f : FreeMonoid α →* M) : lift.symm f = f ∘ of := r
 
 @[to_additive]
 theorem lift_apply (f : α → M) (l : FreeMonoid α) : lift f l = ((toList l).map f).prod :=
-prodAux_eq _
+  prodAux_eq _
 #align free_monoid.lift_apply FreeMonoid.lift_apply
 #align free_add_monoid.lift_apply FreeAddMonoid.lift_apply
 
@@ -270,7 +270,7 @@ theorem lift_restrict (f : FreeMonoid α →* M) : lift (f ∘ of) = f := lift.a
 
 @[to_additive]
 theorem comp_lift (g : M →* N) (f : α → M) : g.comp (lift f) = lift (g ∘ f) :=
--- Porting note: replace ext by FreeMonoid.hom_eq
+  -- Porting note: replace ext by FreeMonoid.hom_eq
   FreeMonoid.hom_eq (by simp)
 #align free_monoid.comp_lift FreeMonoid.comp_lift
 #align free_add_monoid.comp_lift FreeAddMonoid.comp_lift

Mathlib/Algebra/FreeMonoid/Count.lean

@@ -32,7 +32,7 @@ def countp : FreeAddMonoid α →+ ℕ where
   map_add' := List.countp_append _
 #align free_add_monoid.countp FreeAddMonoid.countp
 
-theorem countp_of (x : α): countp p (of x) = if p x = true then 1 else 0 := by
+theorem countp_of (x : α) : countp p (of x) = if p x = true then 1 else 0 := by
   simp [countp, List.countp, List.countp.go]
 #align free_add_monoid.countp_of FreeAddMonoid.countp_of
 

Mathlib/Algebra/GradedMonoid.lean

@@ -468,7 +468,7 @@ instance CommMonoid.gCommMonoid [AddCommMonoid ι] [CommMonoid R] :
 /-- When all the indexed types are the same, the dependent product is just the regular product. -/
 @[simp]
 theorem List.dProd_monoid {α} [AddMonoid ι] [Monoid R] (l : List α) (fι : α → ι) (fA : α → R) :
-    @List.dProd _ _ (fun _:ι => R) _ _ l fι fA = (l.map fA).prod := by
+    @List.dProd _ _ (fun _ : ι => R) _ _ l fι fA = (l.map fA).prod := by
   match l with
   | [] =>
     rw [List.dProd_nil, List.map_nil, List.prod_nil]

Mathlib/Algebra/Group/OrderSynonym.lean

@@ -140,25 +140,25 @@ theorem ofDual_div [Div α] (a b : αᵒᵈ) : ofDual (a / b) = ofDual a / ofDua
 #align of_dual_div ofDual_div
 #align of_dual_sub ofDual_sub
 
-@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) toDual_smul]
+@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) toDual_smul]
 theorem toDual_pow [Pow α β] (a : α) (b : β) : toDual (a ^ b) = toDual a ^ b := rfl
 #align to_dual_pow toDual_pow
 #align to_dual_smul toDual_smul
 #align to_dual_vadd toDual_vadd
 
-@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) ofDual_smul]
+@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofDual_smul]
 theorem ofDual_pow [Pow α β] (a : αᵒᵈ) (b : β) : ofDual (a ^ b) = ofDual a ^ b := rfl
 #align of_dual_pow ofDual_pow
 #align of_dual_smul ofDual_smul
 #align of_dual_vadd ofDual_vadd
 
-@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) toDual_smul']
+@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) toDual_smul']
 theorem pow_toDual [Pow α β] (a : α) (b : β) : a ^ toDual b = a ^ b := rfl
 #align pow_to_dual pow_toDual
 #align to_dual_smul' toDual_smul'
 #align to_dual_vadd' toDual_vadd'
 
-@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) ofDual_smul']
+@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofDual_smul']
 theorem pow_ofDual [Pow α β] (a : α) (b : βᵒᵈ) : a ^ ofDual b = a ^ b := rfl
 #align pow_of_dual pow_ofDual
 #align of_dual_smul' ofDual_smul'
@@ -280,25 +280,25 @@ theorem ofLex_div [Div α] (a b : Lex α) : ofLex (a / b) = ofLex a / ofLex b :=
 #align of_lex_div ofLex_div
 #align of_lex_sub ofLex_sub
 
-@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) toLex_smul]
+@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) toLex_smul]
 theorem toLex_pow [Pow α β] (a : α) (b : β) : toLex (a ^ b) = toLex a ^ b := rfl
 #align to_lex_pow toLex_pow
 #align to_lex_smul toLex_smul
 #align to_lex_vadd toLex_vadd
 
-@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) ofLex_smul]
+@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofLex_smul]
 theorem ofLex_pow [Pow α β] (a : Lex α) (b : β) : ofLex (a ^ b) = ofLex a ^ b := rfl
 #align of_lex_pow ofLex_pow
 #align of_lex_smul ofLex_smul
 #align of_lex_vadd ofLex_vadd
 
-@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) toLex_smul']
+@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) toLex_smul']
 theorem pow_toLex [Pow α β] (a : α) (b : β) : a ^ toLex b = a ^ b := rfl
 #align pow_to_lex pow_toLex
 #align to_lex_smul' toLex_smul'
 #align to_lex_vadd' toLex_vadd'
 
-@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) ofLex_smul']
+@[to_additive (attr := simp, to_additive) (reorder := 1 2, 4 5) ofLex_smul']
 theorem pow_ofLex [Pow α β] (a : α) (b : Lex β) : a ^ ofLex b = a ^ b := rfl
 #align pow_of_lex pow_ofLex
 #align of_lex_smul' ofLex_smul'

Mathlib/Algebra/Group/UniqueProds.lean

@@ -84,7 +84,7 @@ theorem set_subsingleton (A B : Finset G) (a0 b0 : G) (h : UniqueMul A B a0 b0)
 --  (ab «expr ∈ » [finset.product/multiset.product/set.prod/list.product](A, B)) -/
 @[to_additive]
 theorem iff_existsUnique (aA : a0 ∈ A) (bB : b0 ∈ B) :
-    UniqueMul A B a0 b0 ↔ ∃! (ab : _)(_ : ab ∈ A ×ˢ B), ab.1 * ab.2 = a0 * b0 :=
+    UniqueMul A B a0 b0 ↔ ∃! (ab : _) (_ : ab ∈ A ×ˢ B), ab.1 * ab.2 = a0 * b0 :=
   ⟨fun _ ↦ ⟨(a0, b0), ⟨Finset.mem_product.mpr ⟨aA, bB⟩, rfl, by simp⟩, by simpa⟩,
     fun h ↦ h.elim₂
       (by
@@ -99,7 +99,7 @@ theorem iff_existsUnique (aA : a0 ∈ A) (bB : b0 ∈ B) :
 @[to_additive]
 theorem exists_iff_exists_existsUnique :
     (∃ a0 b0 : G, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0) ↔
-      ∃ g : G, ∃! (ab : _)(_ : ab ∈ A ×ˢ B), ab.1 * ab.2 = g :=
+      ∃ g : G, ∃! (ab : _) (_ : ab ∈ A ×ˢ B), ab.1 * ab.2 = g :=
   ⟨fun ⟨a0, b0, hA, hB, h⟩ ↦ ⟨_, (iff_existsUnique hA hB).mp h⟩, fun ⟨g, h⟩ ↦ by
     have h' := h
     rcases h' with ⟨⟨a, b⟩, ⟨hab, rfl, -⟩, -⟩

Mathlib/Algebra/Group/Units.lean

@@ -604,7 +604,7 @@ attribute [nontriviality] isAddUnit_of_subsingleton
 
 @[to_additive]
 instance [Monoid M] : CanLift M Mˣ Units.val IsUnit :=
-{ prf := fun _ ↦ id }
+  { prf := fun _ ↦ id }
 
 /-- A subsingleton `Monoid` has a unique unit. -/
 @[to_additive "A subsingleton `AddMonoid` has a unique additive unit."]

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -845,7 +845,7 @@ attribute [to_additive existing zmultiplesHom] zpowersHom
 variable {M G A}
 
 theorem powersHom_apply [Monoid M] (x : M) (n : Multiplicative ℕ) :
-    powersHom M x n = x ^ (Multiplicative.toAdd n):=
+    powersHom M x n = x ^ (Multiplicative.toAdd n) :=
   rfl
 #align powers_hom_apply powersHom_apply
 

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -41,7 +41,7 @@ theorem eq_of_sub_eq_zero' [AddGroup R] {a b : R} (h : a - b = 0) : a = b :=
 -- This theorem was introduced during ad-hoc porting
 -- and hopefully can be removed again after `Mathlib.Algebra.Ring.Basic` is fully ported.
 theorem pow_succ'' [Monoid M] : ∀ (n : ℕ) (a : M), a ^ n.succ = a * a ^ n :=
-Monoid.npow_succ
+  Monoid.npow_succ
 
 /-- Typeclass for expressing that a type `M₀` with multiplication and a zero satisfies
 `0 * a = 0` and `a * 0 = 0` for all `a : M₀`. -/
@@ -189,7 +189,7 @@ export GroupWithZero (inv_zero)
 attribute [simp] inv_zero
 
 @[simp] lemma mul_inv_cancel [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : a * a⁻¹ = 1 :=
-GroupWithZero.mul_inv_cancel a h
+  GroupWithZero.mul_inv_cancel a h
 #align mul_inv_cancel mul_inv_cancel
 
 /-- A type `G₀` is a commutative “group with zero”

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

@@ -218,15 +218,15 @@ theorem mk0_inj {a b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) : Units.mk0 a ha = Un
 #align units.mk0_inj Units.mk0_inj
 
 /-- In a group with zero, an existential over a unit can be rewritten in terms of `Units.mk0`. -/
-theorem exists0 {p : G₀ˣ → Prop} : (∃ g : G₀ˣ, p g) ↔ ∃ (g : G₀)(hg : g ≠ 0), p (Units.mk0 g hg) :=
+theorem exists0 {p : G₀ˣ → Prop} : (∃ g : G₀ˣ, p g) ↔ ∃ (g : G₀) (hg : g ≠ 0), p (Units.mk0 g hg) :=
   ⟨fun ⟨g, pg⟩ => ⟨g, g.ne_zero, (g.mk0_val g.ne_zero).symm ▸ pg⟩,
   fun ⟨g, hg, pg⟩ => ⟨Units.mk0 g hg, pg⟩⟩
 #align units.exists0 Units.exists0
 
 /-- An alternative version of `Units.exists0`. This one is useful if Lean cannot
 figure out `p` when using `Units.exists0` from right to left. -/
 theorem exists0' {p : ∀ g : G₀, g ≠ 0 → Prop} :
-    (∃ (g : G₀)(hg : g ≠ 0), p g hg) ↔ ∃ g : G₀ˣ, p g g.ne_zero :=
+    (∃ (g : G₀) (hg : g ≠ 0), p g hg) ↔ ∃ g : G₀ˣ, p g g.ne_zero :=
   Iff.trans (by simp_rw [val_mk0]) exists0.symm
   -- porting note: had to add the `rfl`
 #align units.exists0' Units.exists0'

Mathlib/Algebra/HierarchyDesign.lean

@@ -133,7 +133,7 @@ you should provide instances transferring
 Typically this is done using the `Function.Injective.Z` definition mentioned above.
 ```
 instance SubY.toZ [Z α] : Z (SubY α) :=
-coe_injective.Z coe ...
+  coe_injective.Z coe ...
 ```
 
 ## Morphisms and equivalences

Mathlib/Algebra/Hom/Equiv/Basic.lean

@@ -168,7 +168,7 @@ end MulEquivClass
 "Turn an element of a type `F` satisfying `AddEquivClass F α β` into an actual
 `AddEquiv`. This is declared as the default coercion from `F` to `α ≃+ β`."]
 def MulEquivClass.toMulEquiv [Mul α] [Mul β] [MulEquivClass F α β] (f : F) : α ≃* β :=
-{ (f : α ≃ β), (f : α →ₙ* β) with }
+  { (f : α ≃ β), (f : α →ₙ* β) with }
 
 /-- Any type satisfying `MulEquivClass` can be cast into `MulEquiv` via
 `MulEquivClass.toMulEquiv`. -/