style: fix whitespace (#37993)

Found by extending the whitespace linter to proof bodies in #30658.

Author: grunweg

Mathlib/Algebra/Algebra/Operations.lean

@@ -904,7 +904,7 @@ theorem restrictScalars_image_smul_eq {S M : Type*}
     (algebraMap S R '' s • N).restrictScalars S = s • N.restrictScalars S := by
   refine le_antisymm (fun x x_in ↦ ?_) (set_smul_le _ _ _ fun r x r_in x_in ↦ ?_)
   · rw [restrictScalars_mem] at x_in
-    refine set_smul_inductionOn x x_in ?_ ?_ (fun _ _ _ _ h h' ↦  add_mem h h') (zero_mem _)
+    refine set_smul_inductionOn x x_in ?_ ?_ (fun _ _ _ _ h h' ↦ add_mem h h') (zero_mem _)
     · rintro _ x ⟨r, r_in, rfl⟩ x_in
       rw [algebraMap_smul]
       exact mem_set_smul_of_mem_mem r_in x_in

Mathlib/Algebra/Category/ModuleCat/Presheaf/ColimitFunctor.lean

@@ -252,7 +252,7 @@ noncomputable def homEquiv {N : ModuleCat.{w} cR.pt} :
         rw [hφ]
         erw [toPresheaf_map_app_apply]
         rw [map_smul]
-        rfl}
+        rfl }
   left_inv φ := (forget₂ _ AddCommGrpCat).map_injective (by
     ext : 1
     exact (homEquiv' hcR hcM).left_inv ((forget₂ _ AddCommGrpCat).map φ).hom)

Mathlib/Algebra/Group/Indicator.lean

@@ -203,7 +203,7 @@ section One
 lemma mulSupport_subset_subsingleton_of_disjoint_on_mulSupport [One β] {s : γ → Set α} (f : α → β)
   (hs : Pairwise (Disjoint on (fun j ↦ s j ∩ f.mulSupport))) (i : α) (j : γ) (hj : i ∈ s j) :
     (fun d ↦ (s d).mulIndicator f i).mulSupport ⊆ {j} := by
-  suffices ∀ j', j' ≠ j →  {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False by by_contra; aesop
+  suffices ∀ j', j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False by by_contra; aesop
   intro j' h hj hj' hi
   simp only [Pairwise, Disjoint, Set.le_eq_subset, Set.subset_inter_iff] at hs
   simpa using hs h ⟨hj', hi⟩ ⟨hj, hi⟩

Mathlib/Algebra/Group/Units/Defs.lean

@@ -536,13 +536,13 @@ instance (x : M) [h : Decidable (∃ u : Mˣ, ↑u = x)] : Decidable (IsUnit x)
 
 theorem mul_left_iff {a b : M} (ha : IsUnit a) :
     IsUnit (a * b) ↔ IsUnit b :=
-  show IsUnit (ha.unit * b) ↔ _ by simp [- IsUnit.unit_spec]
+  show IsUnit (ha.unit * b) ↔ _ by simp [-IsUnit.unit_spec]
 
 grind_pattern mul_left_iff => IsUnit a, IsUnit (a * b)
 
 theorem mul_right_iff {a b : M} (hb : IsUnit b) :
     IsUnit (a * b) ↔ IsUnit a :=
-  show IsUnit (a * hb.unit) ↔ _ by simp [- IsUnit.unit_spec]
+  show IsUnit (a * hb.unit) ↔ _ by simp [-IsUnit.unit_spec]
 
 grind_pattern mul_right_iff => IsUnit b, IsUnit (a * b)
 

Mathlib/Algebra/GroupWithZero/Range.lean

@@ -137,8 +137,8 @@ def ValueGroup₀.restrict₀ : A →*₀ ValueGroup₀ f where
   toFun a :=
     letI : DecidablePred fun b : B ↦ b = 0 := Classical.decPred fun b ↦ b = 0
     if h : f a = 0 then 0 else (⟨Units.mk0 (f a) h, mem_valueGroup _ ⟨a, rfl⟩⟩ : valueGroup f)
-  map_one'  := by simp [← WithZero.coe_one]
-  map_mul'  := by aesop
+  map_one' := by simp [← WithZero.coe_one]
+  map_mul' := by aesop
   map_zero' := by simp
 
 namespace ValueGroup₀

Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean

@@ -88,7 +88,7 @@ lemma extClass_hom [HasDerivedCategory.{w'} C] : hS.extClass.hom = hS.singleδ :
   dsimp [extClass, SmallShiftedHom.equiv]
   erw [SmallHom.equiv_comp]
   rw [SmallHom.equiv_mkInv, SmallHom.equiv_mk]
-  dsimp [- Q_obj_single_obj, singleδ, triangleOfSESδ]
+  dsimp [-Q_obj_single_obj, singleδ, triangleOfSESδ]
   rw [Category.assoc, Category.assoc, Category.assoc,
     singleFunctorsPostcompQIso_hom_hom, singleFunctorsPostcompQIso_inv_hom,
     NatTrans.id_app, Category.id_comp, NatTrans.id_app]

Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean

@@ -105,7 +105,7 @@ lemma ShortComplex.ShortExact.mapShiftedHom_singleδ
     [HasDerivedCategory.{t} C] [HasDerivedCategory.{t'} D]
     {S : ShortComplex C} (hS : S.ShortExact) (F : C ⥤ D) [F.Additive]
     [PreservesFiniteLimits F] [PreservesFiniteColimits F] :
-    ShiftedHom.map hS.singleδ F.mapDerivedCategory  =
+    ShiftedHom.map hS.singleδ F.mapDerivedCategory =
       (F.mapDerivedCategorySingleFunctor 0).hom.app S.X₃ ≫
         (hS.map_of_exact F).singleδ ≫ ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₁)⟦1⟧' := by
   simp [← hS.mapShiftedHom_singleδ'_assoc, ← Functor.map_comp]

Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean

@@ -57,7 +57,7 @@ lemma triangleOfSESδ_naturality {S₁ S₂ : ShortComplex (CochainComplex C ℤ
   simp only [triangleOfSESδ, CochainComplex.mappingCone.triangle_obj₁, Category.assoc,
     IsIso.inv_comp_eq]
   rw [← Functor.comp_map, ← (Q.commShiftIso (1 : ℤ)).hom.naturality, ← Category.assoc,
-    ← Category.assoc, ← Category.assoc, ← Category.assoc , ← Iso.app_hom,
+    ← Category.assoc, ← Category.assoc, ← Category.assoc, ← Iso.app_hom,
     Iso.cancel_iso_hom_right, ← Q.map_comp]
   simp only [Functor.comp_obj, Functor.comp_map,
     ← CochainComplex.mappingCone.descShortComplex_naturality f,

Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

@@ -728,7 +728,7 @@ def isKernel (hm : n + 1 = m) :
           #adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
           this was just `cat_disch`. -/
           simp +instances only [HomComplex_X, map_add]
-          rfl})
+          rfl })
     (by cat_disch) (fun s l hl ↦ by ext : 3; simp [← hl])
 
 end Cocycle

Mathlib/Algebra/Homology/HomotopyCategory/MappingCocone.lean

@@ -243,7 +243,7 @@ lemma δ_liftCochain (n' : ℤ) (hn' : n + 1 = n') :
   dsimp [liftCochain, inl, inr]
   ext p q hpq
   simp [mappingCone.δ_liftCochain _ _ _ _ n' hn',
-    Cochain.δ_rightShift _ (-1) _ n' _ n  (by lia),
+    Cochain.δ_rightShift _ (-1) _ n' _ n (by lia),
     Cochain.rightShift_v (n := n) _ _ _ _ p _ _ (q + -1) (by lia),
     Cochain.rightShift_v _ _ _ _ _ _ _ (q + -1) rfl,
     Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero (q + -1)),