chore: whitespace adaptations (#24488)

Found by #24465.

Author: adomani

Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

@@ -1150,8 +1150,7 @@ See `card_le_card_mul_self'` for the version with right-cancellative multiplicat
 -/
 @[to_additive
 "The size of `s + s` is at least the size of `s`, version with left-cancellative addition.
-See `card_le_card_add_self'` for the version with right-cancellative addition."
-]
+See `card_le_card_add_self'` for the version with right-cancellative addition."]
 theorem card_le_card_mul_self {s : Finset α} : #s ≤ #(s * s) := by
   cases s.eq_empty_or_nonempty <;> simp [card_le_card_mul_left, *]
 

Mathlib/Algebra/Group/UniqueProds/Basic.lean

@@ -604,7 +604,7 @@ open MulOpposite in
   multiplication is strictly monotone w.r.t. the first argument, then `G` has `TwoUniqueProds`. -/
 @[to_additive
   "This instance asserts that if `G` has a left-cancellative addition, a linear order, and
-  addition is strictly monotone w.r.t. the first argument, then `G` has `TwoUniqueSums`." ]
+  addition is strictly monotone w.r.t. the first argument, then `G` has `TwoUniqueSums`."]
 instance (priority := 100) of_covariant_left [IsLeftCancelMul G]
     [LinearOrder G] [MulRightStrictMono G] :
     TwoUniqueProds G :=

Mathlib/Algebra/Order/Floor/Defs.lean

@@ -304,7 +304,7 @@ private theorem int_floor_nonneg_of_pos [Ring α] [LinearOrder α] [FloorRing α
   int_floor_nonneg ha.le
 
 /-- Extension for the `positivity` tactic: `Int.floor` is nonnegative if its input is. -/
-@[positivity ⌊ _ ⌋]
+@[positivity ⌊_⌋]
 def evalIntFloor : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(ℤ), ~q(@Int.floor $α' $ir $io $j $a) =>
@@ -323,7 +323,7 @@ private theorem nat_ceil_pos [Semiring α] [LinearOrder α] [FloorSemiring α] {
   Nat.ceil_pos.2
 
 /-- Extension for the `positivity` tactic: `Nat.ceil` is positive if its input is. -/
-@[positivity ⌈ _ ⌉₊]
+@[positivity ⌈_⌉₊]
 def evalNatCeil : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(ℕ), ~q(@Nat.ceil $α' $ir $io $j $a) =>
@@ -341,7 +341,7 @@ private theorem int_ceil_pos [Ring α] [LinearOrder α] [FloorRing α] {a : α}
   Int.ceil_pos.2
 
 /-- Extension for the `positivity` tactic: `Int.ceil` is positive/nonnegative if its input is. -/
-@[positivity ⌈ _ ⌉]
+@[positivity ⌈_⌉]
 def evalIntCeil : PositivityExt where eval {u α} _zα _pα e := do
   match u, α, e with
   | 0, ~q(ℤ), ~q(@Int.ceil $α' $ir $io $j $a) =>

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

@@ -524,7 +524,8 @@ theorem HasFDerivWithinAt.of_not_accPt (h : ¬AccPt x (𝓟 s)) : HasFDerivWithi
 /-- If `x` is isolated in `s`, then `f` has any derivative at `x` within `s`,
 as this statement is empty. -/
 @[deprecated HasFDerivWithinAt.of_not_accPt (since := "2025-04-20")]
-theorem HasFDerivWithinAt.of_nhdsWithin_eq_bot (h : 𝓝[s\{x}] x = ⊥) : HasFDerivWithinAt f f' s x :=
+theorem HasFDerivWithinAt.of_nhdsWithin_eq_bot (h : 𝓝[s \ {x}] x = ⊥) :
+    HasFDerivWithinAt f f' s x :=
   .of_not_accPt <| by rwa [accPt_principal_iff_nhdsWithin, not_neBot]
 
 /-- If `x` is not in the closure of `s`, then `f` has any derivative at `x` within `s`,

Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

@@ -441,7 +441,7 @@ irreducible_def eLpNormLESNormFDerivOneConst (p : ℝ) : ℝ≥0 :=
 compactly-supported function `u` on a normed space `E` of finite dimension `n ≥ 2`, equipped
 with Haar measure. Then the `Lᵖ` norm of `u`, where `p := n / (n - 1)`, is bounded above by
 a constant times the `L¹` norm of the Fréchet derivative of `u`. -/
-theorem eLpNorm_le_eLpNorm_fderiv_one  {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
+theorem eLpNorm_le_eLpNorm_fderiv_one {u : E → F} (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
     {p : ℝ≥0} (hp : NNReal.HolderConjugate (finrank ℝ E) p) :
     eLpNorm u p μ ≤ eLpNormLESNormFDerivOneConst μ p * eLpNorm (fderiv ℝ u) 1 μ := by
   have h0p : 0 < (p : ℝ) := hp.coe.symm.pos
@@ -468,7 +468,7 @@ the Fréchet derivative of `u`.
 
 Note: The codomain of `u` needs to be a Hilbert space.
 -/
-theorem eLpNorm_le_eLpNorm_fderiv_of_eq_inner  {u : E → F'}
+theorem eLpNorm_le_eLpNorm_fderiv_of_eq_inner {u : E → F'}
     (hu : ContDiff ℝ 1 u) (h2u : HasCompactSupport u)
     {p p' : ℝ≥0} (hp : 1 ≤ p) (hn : 0 < finrank ℝ E)
     (hp' : (p' : ℝ)⁻¹ = p⁻¹ - (finrank ℝ E : ℝ)⁻¹) :

Mathlib/CategoryTheory/Monoidal/Subcategory.lean

@@ -126,7 +126,7 @@ variable {P} {P' : ObjectProperty C} [P'.IsMonoidal] (h : P ≤ P')
 
 /-- An inequality `P ≤ P'` between monoidal properties of objects induces
 a monoidal functor between full monoidal subcategories. -/
-instance  : (ιOfLE h).Monoidal :=
+instance : (ιOfLE h).Monoidal :=
   Functor.CoreMonoidal.toMonoidal
     { εIso := Iso.refl _
       μIso := fun _ _ ↦ Iso.refl _ }

Mathlib/Computability/Language.lean

@@ -388,7 +388,7 @@ end Language
 /-- Symbols for use by all kinds of grammars. -/
 inductive Symbol (T N : Type*)
   /-- Terminal symbols (of the same type as the language) -/
-  | terminal    (t : T) : Symbol T N
+  | terminal (t : T) : Symbol T N
   /-- Nonterminal symbols (must not be present when the word being generated is finalized) -/
   | nonterminal (n : N) : Symbol T N
 deriving

Mathlib/Condensed/TopCatAdjunction.lean

@@ -9,8 +9,8 @@ import Mathlib.Topology.Category.CompactlyGenerated
 
 # The adjunction between condensed sets and topological spaces
 
-This file defines the functor `condensedSetToTopCat : CondensedSet.{u} ⥤ TopCat.{u+1}` which is
-left adjoint to `topCatToCondensedSet : TopCat.{u+1} ⥤ CondensedSet.{u}`. We prove that the counit
+This file defines the functor `condensedSetToTopCat : CondensedSet.{u} ⥤ TopCat.{u + 1}` which is
+left adjoint to `topCatToCondensedSet : TopCat.{u + 1} ⥤ CondensedSet.{u}`. We prove that the counit
 is bijective (but not in general an isomorphism) and conclude that the right adjoint is faithful.
 
 The counit is an isomorphism for compactly generated spaces, and we conclude that the functor
@@ -26,7 +26,7 @@ variable (X : CondensedSet.{u})
 /-- Auxiliary definition to define the topology on `X(*)` for a condensed set `X`. -/
 private def CondensedSet.coinducingCoprod :
     (Σ (i : (S : CompHaus.{u}) × X.val.obj ⟨S⟩), i.fst) → X.val.obj ⟨of PUnit⟩ :=
-  fun ⟨⟨_, i⟩, s⟩ ↦ X.val.map ((of PUnit.{u+1}).const s).op i
+  fun ⟨⟨_, i⟩, s⟩ ↦ X.val.map ((of PUnit.{u + 1}).const s).op i
 
 /-- Let `X` be a condensed set. We define a topology on `X(*)` as the quotient topology of
 all the maps from compact Hausdorff `S` spaces to `X(*)`, corresponding to elements of `X(S)`.
@@ -35,7 +35,7 @@ local instance : TopologicalSpace (X.val.obj ⟨CompHaus.of PUnit⟩) :=
   TopologicalSpace.coinduced (coinducingCoprod X) inferInstance
 
 /-- The object part of the functor `CondensedSet ⥤ TopCat` -/
-abbrev CondensedSet.toTopCat : TopCat.{u+1} := TopCat.of (X.val.obj ⟨of PUnit⟩)
+abbrev CondensedSet.toTopCat : TopCat.{u + 1} := TopCat.of (X.val.obj ⟨of PUnit⟩)
 
 namespace CondensedSet
 
@@ -59,22 +59,23 @@ def toTopCatMap : X.toTopCat ⟶ Y.toTopCat :=
       apply continuous_sigma
       intro ⟨S, x⟩
       simp only [Function.comp_apply, coinducingCoprod]
-      rw [show (fun (a : S) ↦ f.val.app ⟨of PUnit⟩ (X.val.map ((of PUnit.{u+1}).const a).op x)) = _
-        from funext fun a ↦ NatTrans.naturality_apply f.val ((of PUnit.{u+1}).const a).op x]
+      rw [show (fun (a : S) ↦
+          f.val.app ⟨of PUnit⟩ (X.val.map ((of PUnit.{u + 1}).const a).op x)) = _
+        from funext fun a ↦ NatTrans.naturality_apply f.val ((of PUnit.{u + 1}).const a).op x]
       exact continuous_coinducingCoprod Y _ }
 
 end CondensedSet
 
 /-- The functor `CondensedSet ⥤ TopCat` -/
 @[simps]
-def condensedSetToTopCat : CondensedSet.{u} ⥤ TopCat.{u+1} where
+def condensedSetToTopCat : CondensedSet.{u} ⥤ TopCat.{u + 1} where
   obj X := X.toTopCat
   map f := toTopCatMap f
 
 namespace CondensedSet
 
 /-- The counit of the adjunction `condensedSetToTopCat ⊣ topCatToCondensedSet` -/
-def topCatAdjunctionCounit (X : TopCat.{u+1}) : X.toCondensedSet.toTopCat ⟶ X :=
+def topCatAdjunctionCounit (X : TopCat.{u + 1}) : X.toCondensedSet.toTopCat ⟶ X :=
   TopCat.ofHom
   { toFun x := x.1 PUnit.unit
     continuous_toFun := by
@@ -92,13 +93,13 @@ def topCatAdjunctionCounit (X : TopCat.{u+1}) : X.toCondensedSet.toTopCat ⟶ X
 /-- The counit of the adjunction `condensedSetToTopCat ⊣ topCatToCondensedSet` is always bijective,
 but not an isomorphism in general (the inverse isn't continuous unless `X` is compactly generated).
 -/
-def topCatAdjunctionCounitEquiv (X : TopCat.{u+1}) : X.toCondensedSet.toTopCat ≃ X where
+def topCatAdjunctionCounitEquiv (X : TopCat.{u + 1}) : X.toCondensedSet.toTopCat ≃ X where
   toFun := topCatAdjunctionCounit X
   invFun x := ContinuousMap.const _ x
   left_inv _ := rfl
   right_inv _ := rfl
 
-lemma topCatAdjunctionCounit_bijective (X : TopCat.{u+1}) :
+lemma topCatAdjunctionCounit_bijective (X : TopCat.{u + 1}) :
     Function.Bijective (topCatAdjunctionCounit X) :=
   (topCatAdjunctionCounitEquiv X).bijective
 
@@ -107,7 +108,7 @@ lemma topCatAdjunctionCounit_bijective (X : TopCat.{u+1}) :
 def topCatAdjunctionUnit (X : CondensedSet.{u}) : X ⟶ X.toTopCat.toCondensedSet where
   val := {
     app := fun S x ↦ {
-      toFun := fun s ↦ X.val.map ((of PUnit.{u+1}).const s).op x
+      toFun := fun s ↦ X.val.map ((of PUnit.{u + 1}).const s).op x
       continuous_toFun := by
         suffices ∀ (i : (T : CompHaus.{u}) × X.val.obj ⟨T⟩),
           Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩
@@ -137,25 +138,26 @@ instance : topCatToCondensedSet.Faithful := topCatAdjunction.faithful_R_of_epi_c
 
 open CompactlyGenerated
 
-instance (X : CondensedSet.{u}) : UCompactlyGeneratedSpace.{u, u+1} X.toTopCat := by
+instance (X : CondensedSet.{u}) : UCompactlyGeneratedSpace.{u, u + 1} X.toTopCat := by
   apply uCompactlyGeneratedSpace_of_continuous_maps
   intro Y _ f h
   rw [continuous_coinduced_dom, continuous_sigma_iff]
   exact fun ⟨S, s⟩ ↦ h S ⟨_, continuous_coinducingCoprod X _⟩
 
-instance (X : CondensedSet.{u}) : UCompactlyGeneratedSpace.{u, u+1} (condensedSetToTopCat.obj X) :=
-  inferInstanceAs (UCompactlyGeneratedSpace.{u, u+1} X.toTopCat)
+instance (X : CondensedSet.{u}) :
+    UCompactlyGeneratedSpace.{u, u + 1} (condensedSetToTopCat.obj X) :=
+  inferInstanceAs (UCompactlyGeneratedSpace.{u, u + 1} X.toTopCat)
 
 /-- The functor from condensed sets to topological spaces lands in compactly generated spaces. -/
-def condensedSetToCompactlyGenerated : CondensedSet.{u} ⥤ CompactlyGenerated.{u, u+1} where
+def condensedSetToCompactlyGenerated : CondensedSet.{u} ⥤ CompactlyGenerated.{u, u + 1} where
   obj X := CompactlyGenerated.of (condensedSetToTopCat.obj X)
   map f := toTopCatMap f
 
 /--
 The functor from topological spaces to condensed sets restricted to compactly generated spaces.
 -/
 noncomputable def compactlyGeneratedToCondensedSet :
-    CompactlyGenerated.{u, u+1} ⥤ CondensedSet.{u} :=
+    CompactlyGenerated.{u, u + 1} ⥤ CondensedSet.{u} :=
   compactlyGeneratedToTop ⋙ topCatToCondensedSet
 
 

Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean

@@ -77,7 +77,7 @@ typeclass synthesis issues on complex `Module` goals.  To convert into a form
 that uses the ideal of `R ⧸ I ^ (n + 1)`, compose with
 `Ideal.powQuotPowSuccEquivMapMkPowSuccPow`. -/
 noncomputable
-def quotEquivPowQuotPowSuccEquiv (h : I.IsPrincipal) (h': I ≠ ⊥) (n : ℕ) :
+def quotEquivPowQuotPowSuccEquiv (h : I.IsPrincipal) (h' : I ≠ ⊥) (n : ℕ) :
     (R ⧸ I) ≃ (I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R)) :=
   quotEquivPowQuotPowSucc h h' n