chore(Algebra): fix whitespace (leanprover-community#33182)

Found by extending the commandStart linter to proof bodies.

Author: harahu

Mathlib/Algebra/Category/ModuleCat/Semi.lean

@@ -90,7 +90,7 @@ structure Hom (M N : SemimoduleCat.{v} R) where
   /-- The underlying linear map. -/
   hom' : M →ₗ[R] N
 
-instance moduleCategory : Category.{v, max (v+1) u} (SemimoduleCat.{v} R) where
+instance moduleCategory : Category.{v, max (v + 1) u} (SemimoduleCat.{v} R) where
   Hom M N := Hom M N
   id _ := ⟨LinearMap.id⟩
   comp f g := ⟨g.hom'.comp f.hom'⟩

Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean

@@ -148,7 +148,7 @@ lemma map_ιFree_mapFree_hom :
     F.map (ιFree i) ≫ (mapFree F η I).hom = η.hom ≫ ιFree i := by
   have : η.inv ≫ η.hom ≫ ιFree i = (η.inv ≫ F.map (ιFree i)) ≫ (mapFree F η I).hom := by
     simp [← ιFree_mapFree_inv]
-  rw [←Iso.hom_inv_id_assoc η (η.hom ≫ ιFree i)]
+  rw [← Iso.hom_inv_id_assoc η (η.hom ≫ ιFree i)]
   simp [this]
 
 end

Mathlib/Algebra/Category/MonCat/Colimits.lean

@@ -89,18 +89,18 @@ open Prequotient
 because of the monoid laws, or
 because one element is mapped to another by a morphism in the diagram.
 -/
-inductive Relation : Prequotient F → Prequotient F → Prop-- Make it an equivalence relation:
+inductive Relation : Prequotient F → Prequotient F → Prop -- Make it an equivalence relation:
   | refl : ∀ x, Relation x x
   | symm : ∀ (x y) (_ : Relation x y), Relation y x
   | trans : ∀ (x y z) (_ : Relation x y) (_ : Relation y z),
-      Relation x z-- There's always a `map` relation
+      Relation x z -- There's always a `map` relation
   | map :
     ∀ (j j' : J) (f : j ⟶ j') (x : F.obj j),
       Relation (Prequotient.of j' ((F.map f) x))
         (Prequotient.of j x)-- Then one relation per operation, describing the interaction with `of`
   | mul : ∀ (j) (x y : F.obj j), Relation (Prequotient.of j (x * y))
       (mul (Prequotient.of j x) (Prequotient.of j y))
-  | one : ∀ j, Relation (Prequotient.of j 1) one-- Then one relation per argument of each operation
+  | one : ∀ j, Relation (Prequotient.of j 1) one -- Then one relation per argument of each operation
   | mul_1 : ∀ (x x' y) (_ : Relation x x'), Relation (mul x y) (mul x' y)
   | mul_2 : ∀ (x y y') (_ : Relation y y'), Relation (mul x y) (mul x y')
     -- And one relation per axiom

Mathlib/Algebra/GradedMonoid.lean

@@ -602,7 +602,7 @@ instance SetLike.gMonoid {S : Type*} [SetLike S R] [Monoid R] [AddMonoid ι] (A
 @[simp]
 theorem SetLike.coe_gnpow {S : Type*} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S)
     [SetLike.GradedMonoid A] {i : ι} (x : A i) (n : ℕ) :
-    ↑(@GradedMonoid.GMonoid.gnpow _ (fun i => A i) _ _ n _ x) = (x:R)^n :=
+    ↑(@GradedMonoid.GMonoid.gnpow _ (fun i => A i) _ _ n _ x) = (x : R)^n :=
   rfl
 
 /-- Build a `GCommMonoid` instance for a collection of subobjects. -/

Mathlib/Algebra/Homology/Embedding/Extend.lean

@@ -156,7 +156,7 @@ lemma extend_d_eq {i' j' : ι'} {i j : ι} (hi : e.f i = i') (hj : e.f j = j') :
 
 lemma extend_d_from_eq_zero (i' j' : ι') (i : ι) (hi : e.f i = i') (hi' : ¬ c.Rel i (c.next i)) :
     (K.extend e).d i' j' = 0 := by
-  obtain hj'|⟨j, hj⟩ := (e.r j').eq_none_or_eq_some
+  obtain hj' | ⟨j, hj⟩ := (e.r j').eq_none_or_eq_some
   · exact extend.d_none_eq_zero' _ _ _ hj'
   · rw [extend_d_eq K e hi (e.f_eq_of_r_eq_some hj), K.shape, zero_comp, comp_zero]
     intro hij
@@ -165,7 +165,7 @@ lemma extend_d_from_eq_zero (i' j' : ι') (i : ι) (hi : e.f i = i') (hi' : ¬ c
 
 lemma extend_d_to_eq_zero (i' j' : ι') (j : ι) (hj : e.f j = j') (hj' : ¬ c.Rel (c.prev j) j) :
     (K.extend e).d i' j' = 0 := by
-  obtain hi'|⟨i, hi⟩ := (e.r i').eq_none_or_eq_some
+  obtain hi' | ⟨i, hi⟩ := (e.r i').eq_none_or_eq_some
   · exact extend.d_none_eq_zero _ _ _ hi'
   · rw [extend_d_eq K e (e.f_eq_of_r_eq_some hi) hj, K.shape, zero_comp, comp_zero]
     intro hij

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -779,7 +779,7 @@ theorem mk'_d_1_0 : (mk' X₀ X₁ d₀ succ').d 1 0 = d₀ := by
 the inductive construction. -/
 def mk'XIso (n : ℕ) :
     (mk' X₀ X₁ d₀ succ').X (n + 2) ≅ (succ' ((mk' X₀ X₁ d₀ succ').d (n + 1) n)).1 := by
-  obtain _|n := n
+  obtain _ | n := n
   · apply eqToIso
     dsimp [mk', mk, of, mkAux]
     rw [id_comp]
@@ -793,7 +793,7 @@ lemma mk'_congr_succ'_d {X Y : V} (f g : X ⟶ Y) (h : f = g) :
 lemma mk'_d (n : ℕ) :
     (mk' X₀ X₁ d₀ succ').d (n + 2) (n + 1) = (mk'XIso X₀ X₁ d₀ succ' n).hom ≫
       (succ' ((mk' X₀ X₁ d₀ succ').d (n + 1) n)).2.1 := by
-  obtain _|n := n
+  obtain _ | n := n
   · dsimp [mk'XIso, mk']
     rw [mk_d_2_1]
     apply mk'_congr_succ'_d

Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean

@@ -62,8 +62,8 @@ lemma rightShift_v (a n' : ℤ) (hn' : n' + a = n) (p q : ℤ) (hpq : p + n' = q
 
 /-- The map `Cochain K L n → Cochain (K⟦a⟧) L n'` when `n + a = n'`. -/
 def leftShift (a n' : ℤ) (hn' : n + a = n') : Cochain (K⟦a⟧) L n' :=
-  Cochain.mk (fun p q hpq => (a * n' + ((a * (a-1))/2)).negOnePow •
-    (K.shiftFunctorObjXIso a p (p + a) rfl).hom ≫ γ.v (p+a) q (by lia))
+  Cochain.mk (fun p q hpq => (a * n' + ((a * (a - 1)) / 2)).negOnePow •
+    (K.shiftFunctorObjXIso a p (p + a) rfl).hom ≫ γ.v (p + a) q (by lia))
 
 lemma leftShift_v (a n' : ℤ) (hn' : n + a = n') (p q : ℤ) (hpq : p + n' = q)
     (p' : ℤ) (hp' : p' + n = q) :
@@ -91,12 +91,12 @@ lemma rightUnshift_v {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn :
 /-- The map `Cochain (K⟦a⟧) L n' → Cochain K L n` when `n + a = n'`. -/
 def leftUnshift {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') :
     Cochain K L n :=
-  Cochain.mk (fun p q hpq => (a * n' + ((a * (a-1))/2)).negOnePow •
-    (K.shiftFunctorObjXIso a (p - a) p (by lia)).inv ≫ γ.v (p-a) q (by lia))
+  Cochain.mk (fun p q hpq => (a * n' + ((a * (a - 1)) / 2)).negOnePow •
+    (K.shiftFunctorObjXIso a (p - a) p (by lia)).inv ≫ γ.v (p - a) q (by lia))
 
 lemma leftUnshift_v {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n')
     (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p' + n' = q) :
-    (γ.leftUnshift n hn).v p q hpq = (a * n' + ((a * (a-1))/2)).negOnePow •
+    (γ.leftUnshift n hn).v p q hpq = (a * n' + ((a * (a - 1)) / 2)).negOnePow •
       (K.shiftFunctorObjXIso a p' p (by lia)).inv ≫ γ.v p' q (by lia) := by
   obtain rfl : p' = p - a := by lia
   rfl
@@ -139,16 +139,16 @@ lemma rightShift_rightUnshift {a n' : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : 
 lemma leftUnshift_leftShift (a n' : ℤ) (hn' : n + a = n') :
     (γ.leftShift a n' hn').leftUnshift n hn' = γ := by
   ext p q hpq
-  rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q-n') (by lia),
-    γ.leftShift_v a n' hn' (q-n') q (by lia) p hpq, Linear.comp_units_smul,
+  rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q - n') (by lia),
+    γ.leftShift_v a n' hn' (q - n') q (by lia) p hpq, Linear.comp_units_smul,
     Iso.inv_hom_id_assoc, smul_smul, Int.units_mul_self, one_smul]
 
 @[simp]
 lemma leftShift_leftUnshift {a n' : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn' : n + a = n') :
     (γ.leftUnshift n hn').leftShift a n' hn' = γ := by
   ext p q hpq
-  rw [(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q-n) (by lia),
-    γ.leftUnshift_v n hn' (q-n) q (by lia) p hpq, Linear.comp_units_smul, smul_smul,
+  rw [(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q - n) (by lia),
+    γ.leftUnshift_v n hn' (q - n) q (by lia) p hpq, Linear.comp_units_smul, smul_smul,
     Iso.hom_inv_id_assoc, Int.units_mul_self, one_smul]
 
 @[simp]
@@ -403,10 +403,10 @@ lemma δ_rightShift (a n' m' : ℤ) (hn' : n' + a = n) (m : ℤ) (hm' : m' + a =
     ext p q hpq
     dsimp
     rw [(δ n m γ).rightShift_v a m' hm' p q hpq _ rfl,
-      δ_v n m hnm _ p (p+m) rfl (p+n) (p+1) (by lia) rfl,
-      δ_v n' m' hnm' _ p q hpq (p+n') (p+1) (by lia) rfl,
-      γ.rightShift_v a n' hn' p (p+n') rfl (p+n) rfl,
-      γ.rightShift_v a n' hn' (p+1) q _ (p+m) (by lia)]
+      δ_v n m hnm _ p (p + m) rfl (p + n) (p + 1) (by lia) rfl,
+      δ_v n' m' hnm' _ p q hpq (p + n') (p + 1) (by lia) rfl,
+      γ.rightShift_v a n' hn' p (p + n') rfl (p + n) rfl,
+      γ.rightShift_v a n' hn' (p + 1) q _ (p + m) (by lia)]
     simp only [shiftFunctorObjXIso, shiftFunctor_obj_d',
       Linear.comp_units_smul, assoc, HomologicalComplex.XIsoOfEq_inv_comp_d,
       add_comp, HomologicalComplex.d_comp_XIsoOfEq_inv, Linear.units_smul_comp, smul_add,
@@ -430,11 +430,11 @@ lemma δ_leftShift (a n' m' : ℤ) (hn' : n + a = n') (m : ℤ) (hm' : m + a = m
   · have hnm' : n' + 1 = m' := by lia
     ext p q hpq
     dsimp
-    rw [(δ n m γ).leftShift_v a m' hm' p q hpq (p+a) (by lia),
-      δ_v n m hnm _ (p+a) q (by lia) (p+n') (p+1+a) (by lia) (by lia),
-      δ_v n' m' hnm' _ p q hpq (p+n') (p+1) (by lia) rfl,
-      γ.leftShift_v a n' hn' p (p+n') rfl (p+a) (by lia),
-      γ.leftShift_v a n' hn' (p+1) q (by lia) (p+1+a) (by lia)]
+    rw [(δ n m γ).leftShift_v a m' hm' p q hpq (p + a) (by lia),
+      δ_v n m hnm _ (p + a) q (by lia) (p + n') (p + 1 + a) (by lia) (by lia),
+      δ_v n' m' hnm' _ p q hpq (p + n') (p + 1) (by lia) rfl,
+      γ.leftShift_v a n' hn' p (p + n') rfl (p + a) (by lia),
+      γ.leftShift_v a n' hn' (p + 1) q (by lia) (p + 1 + a) (by lia)]
     simp only [shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl,
       Iso.refl_hom, id_comp, Linear.units_smul_comp, shiftFunctor_obj_d',
       Linear.comp_units_smul, smul_add, smul_smul]

Mathlib/Algebra/Homology/HomotopyCategory/KInjective.lean

@@ -106,7 +106,7 @@ lemma isKInjective_of_injective_aux {K L : CochainComplex C ℤ}
   subst hnm
   let u := f.f (n + 1) - α.v (n + 1) n (by lia) ≫ L.d n (n + 1) -
     K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) (by lia)
-  have hu : K.d n (n+1) ≫ u = 0 := by
+  have hu : K.d n (n + 1) ≫ u = 0 := by
     have eq := hα n n (add_zero n) (by rfl)
     simp only [δ_v (-1) 0 (neg_add_cancel 1) α n n (add_zero _) (n - 1) (n + 1)
       (by lia) (by lia), Int.negOnePow_zero, one_smul, Cochain.ofHom_v] at eq

Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean

@@ -110,7 +110,7 @@ lemma inr_f_snd_v (p : ℤ) :
 lemma inl_fst :
     (inl φ).comp (fst φ).1 (neg_add_cancel 1) = Cochain.ofHom (𝟙 F) := by
   ext p
-  simp [Cochain.comp_v _ _ (neg_add_cancel 1) p (p-1) p rfl (by lia)]
+  simp [Cochain.comp_v _ _ (neg_add_cancel 1) p (p - 1) p rfl (by lia)]
 
 @[simp]
 lemma inl_snd :
@@ -475,7 +475,7 @@ noncomputable def liftCocycle {K : CochainComplex C ℤ} {n m : ℤ}
     (eq : δ n m β + α.1.comp (Cochain.ofHom φ) (add_zero m) = 0) :
     Cocycle K (mappingCone φ) n :=
   Cocycle.mk (liftCochain φ α β h) m h (by
-    simp only [δ_liftCochain φ α β h (m+1) rfl, eq,
+    simp only [δ_liftCochain φ α β h (m + 1) rfl, eq,
       Cocycle.δ_eq_zero, Cochain.zero_comp, neg_zero, add_zero])
 
 section

Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean

@@ -78,7 +78,7 @@ noncomputable def hom :
     (descCochain _ 0 (Cochain.ofHom (inr (f ≫ g))) (neg_add_cancel 1)) (by
       ext p _ rfl
       dsimp [mappingConeCompTriangle, map]
-      simp [ext_from_iff _ _ _ rfl, inl_v_d_assoc _ (p+1) p (p+2) (by lia) (by lia)])
+      simp [ext_from_iff _ _ _ rfl, inl_v_d_assoc _ (p + 1) p (p + 2) (by lia) (by lia)])
 
 /-- Given two composable morphisms `f` and `g` in the category of cochain complexes, this
 is the canonical morphism (which is a homotopy equivalence) from the mapping cone of
@@ -89,7 +89,7 @@ noncomputable def inv : mappingCone (mappingConeCompTriangle f g).mor₁ ⟶ map
       ext p
       rw [ext_from_iff _ (p + 1) _ rfl, ext_to_iff _ _ (p + 1) rfl]
       simp [map, δ_zero_cochain_comp,
-        Cochain.comp_v _ _ (add_neg_cancel 1) p (p+1) p (by lia) (by lia)])
+        Cochain.comp_v _ _ (add_neg_cancel 1) p (p + 1) p (by lia) (by lia)])
 @[reassoc (attr := simp)]
 lemma hom_inv_id : hom f g ≫ inv f g = 𝟙 _ := by
   ext n