chore: fix whitespace (#35909)

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

Author: grunweg

Mathlib/Algebra/Category/ModuleCat/Stalk.lean

@@ -144,7 +144,7 @@ lemma IsColimit.ι_smul {cR : Cocone R} (hcR : IsColimit cR) {cM : Cocone M}
     (β := AddCommGrpCat.FilteredColimits.colimit M)
     ((cR.ι.app i ≫ β.hom) r) ((cM.ι.app i ≫ α.hom) m))
   simp only [Functor.const_obj_obj, comp_coconePointUniqueUpToIso_hom, α, β]
-  obtain ⟨s, α, H⟩ :=  IsFilteredOrEmpty.cocone_maps (leftToMax i i) (rightToMax i i)
+  obtain ⟨s, α, H⟩ := IsFilteredOrEmpty.cocone_maps (leftToMax i i) (rightToMax i i)
   refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (leftToMax _ _ ≫ α) α ?_
   dsimp
   simp only [← ConcreteCategory.comp_apply, ← Functor.map_comp, *]

Mathlib/Algebra/Homology/SpectralSequence/Basic.lean

@@ -68,7 +68,7 @@ attribute [reassoc (attr := simp)] Hom.comm
 @[simps! id_hom comp_hom]
 instance : Category (SpectralSequence C c r₀) where
   Hom := Hom
-  id _ := { hom _ _ := 𝟙 _}
+  id _ := { hom _ _ := 𝟙 _ }
   comp f g :=
     { hom r hr := f.hom r ≫ g.hom r
       comm r r' hrr' pq hr := by

Mathlib/Algebra/Lie/SemiDirect.lean

@@ -71,7 +71,7 @@ def toProdl : (K ⋊⁅ψ⁆ L) ≃ₗ[R] K × L :=
     map_smul' _ _ := rfl }
 
 instance : Bracket (K ⋊⁅ψ⁆ L) (K ⋊⁅ψ⁆ L) where
-  bracket x y :=  ⟨⁅x.left, y.left⁆ + ψ x.right y.left - ψ y.right x.left, ⁅x.right, y.right⁆⟩
+  bracket x y := ⟨⁅x.left, y.left⁆ + ψ x.right y.left - ψ y.right x.left, ⁅x.right, y.right⁆⟩
 
 @[simp] lemma zero_eq_mk : (0 : K ⋊⁅ψ⁆ L) = ⟨0, 0⟩ := rfl
 @[simp] lemma add_eq_mk (x y : K ⋊⁅ψ⁆ L) : x + y = ⟨x.left + y.left, x.right + y.right⟩ := rfl
@@ -84,7 +84,7 @@ instance : Bracket (K ⋊⁅ψ⁆ L) (K ⋊⁅ψ⁆ L) where
 
 instance : LieRing (K ⋊⁅ψ⁆ L) where
   add_lie _ _ _ := by simp; abel
-  lie_add _ _ _:= by simp; abel
+  lie_add _ _ _ := by simp; abel
   lie_self _ := by simp
   leibniz_lie _ _ _ := by simp; grind [lie_skew]
 

Mathlib/Algebra/Module/SpanRank.lean

@@ -308,7 +308,7 @@ lemma le_spanRank_restrictScalars (N : Submodule S M) :
     N.spanRank ≤ (N.restrictScalars R).spanRank := by
   obtain ⟨s, hs, e⟩ := (N.restrictScalars R).exists_span_set_card_eq_spanRank
   obtain rfl : span S s = N :=
-    le_antisymm (span_le.mpr (span_le.mp e.le:)) (e.ge.trans (span_le_restrictScalars R S s))
+    le_antisymm (span_le.mpr (span_le.mp e.le :)) (e.ge.trans (span_le_restrictScalars R S s))
   grw [← hs, spanRank_span_le_card]
 
 lemma spanRank_restrictScalars_eq (H : Function.Surjective (algebraMap R S))

Mathlib/AlgebraicGeometry/ColimitsOver.lean

@@ -289,7 +289,7 @@ lemma hasColimit_of_locallyDirected
   let d : ColimitGluingData D 𝒰 :=
     { cocone _ := colimit.cocone _
       isColimit _ := colimit.isColimit _
-      prop_trans := H  }
+      prop_trans := H }
   ⟨d.gluedCocone, d.isColimitGluedCocone⟩
 
 end AlgebraicGeometry.Scheme.Cover

Mathlib/AlgebraicGeometry/Group/Abelian.lean

@@ -117,12 +117,12 @@ theorem isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed [IsAlgCl
         simp [Set.range_comp, Scheme.Pullback.range_map, x]
       · exact ⟨y, subset_closure (by simp), rfl⟩
       · refine ⟨xe, subset_closure ?_, ?_⟩
-        · simp [xe, ← Scheme.Hom.comp_apply, - Scheme.Hom.comp_base]
+        · simp [xe, ← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base]
         · simp only [xe, γ, ← Scheme.Hom.comp_apply, ← Over.comp_left]
           congr 6; ext <;> simp
     convert congr((snd G G).left $this) using 1
     · simp [γ, ← Scheme.Hom.comp_apply]
-    · simp [xe, ← Scheme.Hom.comp_apply, - Scheme.Hom.comp_base]
+    · simp [xe, ← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base]
   · simp
 
 set_option backward.isDefEq.respectTransparency false in

Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean

@@ -307,7 +307,7 @@ nonrec lemma LocallyQuasiFinite.of_finite_preimage_singleton
   obtain ⟨R, rfl⟩ := hY
   wlog hX : ∃ S, X = Spec S
   · exact (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ this _ _
-      (fun x ↦ ((hf x).preimage (X.affineCover.f _).isOpenEmbedding.injective.injOn:)) ⟨_, rfl⟩
+      (fun x ↦ ((hf x).preimage (X.affineCover.f _).isOpenEmbedding.injective.injOn :)) ⟨_, rfl⟩
   obtain ⟨S, rfl⟩ := hX
   obtain ⟨φ, rfl⟩ := Spec.map_surjective f
   simp only [HasRingHomProperty.Spec_iff, id_eq] at *

Mathlib/AlgebraicGeometry/Normalization.lean

@@ -616,7 +616,7 @@ instance [Smooth g] : IsIso (f.normalizationPullback g) := by
       ← Scheme.Hom.preimage_inf, inf_eq_right.mpr hVU]) hU hV (f.isCompact_preimage hU.isCompact)
     (f.isQuasiSeparated_preimage hU.isQuasiSeparated)
   let e₀ := (CommRingCat.isPushout_tensorProduct ..).flip.isoPushout ≪≫
-    (pushout.congrHom f.app_eq_appLE rfl ≪≫ @asIso _ _ _ _ _ this:)
+    (pushout.congrHom f.app_eq_appLE rfl ≪≫ @asIso _ _ _ _ _ this :)
   let e : Γ(Y, V) ⊗[Γ(S, U)] Γ(X, f ⁻¹ᵁ U) ≃ₐ[Γ(Y, V)] Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
     { toRingEquiv := e₀.commRingCatIsoToRingEquiv,
       commutes' r := by

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -806,7 +806,7 @@ lemma Scheme.Hom.isPullback_resLE
     IsPullback (g.resLE UX UY (by simp [*])) (iY.resLE UT UY (by simp [*]))
       (iX.resLE US UX hUSX) (f.resLE US UT hUST) := by
   refine .paste_horiz (v₁₂ := iY.resLE _ _
-    ((g.preimage_mono hUSX).trans_eq congr(($H.w) ⁻¹ᵁ US):)) ?_ ?_
+    ((g.preimage_mono hUSX).trans_eq congr(($H.w) ⁻¹ᵁ US) :)) ?_ ?_
   · refine (IsOpenImmersion.isPullback _ _ _ _ (by simp) ?_).flip
     simp only [Scheme.opensRange_homOfLE, ← Scheme.Hom.comp_preimage, Scheme.Hom.resLE_comp_ι]
     rw [Scheme.Hom.comp_preimage, ← (g ⁻¹ᵁ UX).ι.image_injective.eq_iff]

Mathlib/AlgebraicGeometry/Spec.lean

@@ -290,7 +290,7 @@ theorem Spec_Γ_naturality {R S : CommRingCat.{u}} (f : R ⟶ S) :
 /-- The counit (`SpecΓIdentity.inv.op`) of the adjunction `Γ ⊣ Spec` is an isomorphism. -/
 @[simps! hom_app inv_app]
 def LocallyRingedSpace.SpecΓIdentity : Spec.toLocallyRingedSpace.rightOp ⋙ Γ ≅ 𝟭 _ :=
-  Iso.symm <| NatIso.ofComponents.{u, u, u + 1, u + 1} (fun R ↦ asIso (toSpecΓ R):)
+  Iso.symm <| NatIso.ofComponents.{u, u, u + 1, u + 1} (fun R ↦ asIso (toSpecΓ R) :)
     fun {X Y} f => by convert Spec_Γ_naturality (R := X) (S := Y) f
 
 end SpecΓ