leanprover-community · grunweg · Oct 19, 2025 · Oct 19, 2025 · Oct 19, 2025 · Oct 19, 2025
diff --git a/Archive/Imo/Imo2010Q5.lean b/Archive/Imo/Imo2010Q5.lean
@@ -55,6 +55,7 @@ open Pi Equiv Function
 
 namespace Imo2010Q5
 
+set_option linter.style.whitespace false in -- linter false positive
 /-- The predicate defining states of boxes reachable by the given moves. -/
 inductive Reachable : (Fin 6 → ℕ) → Prop
   /-- The starting position with one coin in each box -/

diff --git a/Archive/Wiedijk100Theorems/BuffonsNeedle.lean b/Archive/Wiedijk100Theorems/BuffonsNeedle.lean
@@ -179,6 +179,7 @@ lemma integrable_needleCrossesIndicator :
       neg_div, sub_neg_eq_add, add_halves, sub_zero, ← ENNReal.ofReal_mul hd.le,
       ENNReal.ofReal_lt_top]
 
+set_option linter.style.whitespace false in
 include hd hB hBₘ in
 /--
 This is a common step in both the short and the long case to simplify the expectation of the

diff --git a/Counterexamples/CliffordAlgebraNotInjective.lean b/Counterexamples/CliffordAlgebraNotInjective.lean
@@ -35,6 +35,7 @@ noncomputable section
 open LinearMap (BilinForm)
 open LinearMap (BilinMap)
 
+set_option linter.style.whitespace false in -- linter false positive
 name_poly_vars X, Y, Z over ZMod 2
 
 namespace Q60596

diff --git a/Counterexamples/HeawoodUnitDistance.lean b/Counterexamples/HeawoodUnitDistance.lean
@@ -29,6 +29,7 @@ namespace SimpleGraph
 
 open Finset
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The Heawood graph, a notable simple graph on 14 vertices. The numbering corresponds to a
 typical [Hamiltonian cycle-and-arcs drawing](https://commons.wikimedia.org/wiki/File:Heawood_Graph.svg). -/
 def heawoodGraph : SimpleGraph (Fin 14) where

diff --git a/Mathlib/Algebra/AffineMonoid/Basic.lean b/Mathlib/Algebra/AffineMonoid/Basic.lean
@@ -16,10 +16,12 @@ monoids.
 
 public section
 
+set_option linter.style.whitespace false in -- linter false positive
 /-- An affine monoid is a finitely generated cancellative torsion-free commutative monoid. -/
 class abbrev IsAffineAddMonoid (M : Type*) [AddCommMonoid M] : Prop :=
   IsCancelAdd M, AddMonoid.FG M, IsAddTorsionFree M
 
+set_option linter.style.whitespace false in -- linter false positive
 /-- An affine monoid is a finitely generated cancellative torsion-free commutative monoid. -/
 @[to_additive]
 class abbrev IsAffineMonoid (M : Type*) [CommMonoid M] : Prop :=

diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean
@@ -907,7 +907,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

diff --git a/Mathlib/Algebra/Category/Grp/EpiMono.lean b/Mathlib/Algebra/Category/Grp/EpiMono.lean
@@ -190,6 +190,7 @@ def g : B →* SX' where
     ext
     simp [mul_smul]
 
+set_option linter.style.whitespace false in -- linter false positive
 local notation "g" => g f
 
 /-- Define `h : B ⟶ S(X')` to be `τ g τ⁻¹`
@@ -203,6 +204,7 @@ def h : B →* SX' where
     ext
     simp
 
+set_option linter.style.whitespace false in -- linter false positive
 local notation "h" => h f
 
 /-!

diff --git a/Mathlib/Algebra/Category/Ring/Basic.lean b/Mathlib/Algebra/Category/Ring/Basic.lean
@@ -150,6 +150,7 @@ lemma hom_inv_apply {R S : SemiRingCat} (e : R ≅ S) (s : S) : e.hom (e.inv s)
 instance : Inhabited SemiRingCat :=
   ⟨of PUnit⟩
 
+set_option linter.style.whitespace false in -- the linter is wrong, even after lean4#11780
 /-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`. -/
 unif_hint forget_obj_eq_coe (R R' : SemiRingCat) where
   R ≟ R' ⊢
@@ -319,6 +320,7 @@ lemma hom_inv_apply {R S : RingCat} (e : R ≅ S) (s : S) : e.hom (e.inv s) = s
 instance : Inhabited RingCat :=
   ⟨of PUnit⟩
 
+set_option linter.style.whitespace false in -- the linter is wrong, even after lean4#11780
 /-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`.
 
 An example where this is needed is in applying
@@ -498,6 +500,7 @@ lemma hom_inv_apply {R S : CommSemiRingCat} (e : R ≅ S) (s : S) : e.hom (e.inv
 instance : Inhabited CommSemiRingCat :=
   ⟨of PUnit⟩
 
+set_option linter.style.whitespace false in -- the linter is wrong, even after lean4#11780
 /-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`. -/
 unif_hint forget_obj_eq_coe (R R' : CommSemiRingCat) where
   R ≟ R' ⊢
@@ -675,6 +678,7 @@ instance : Inhabited CommRingCat :=
 
 lemma forget_obj {R : CommRingCat} : (forget CommRingCat).obj R = R := rfl
 
+set_option linter.style.whitespace false in -- the linter is wrong, even after lean4#11780
 /-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`.
 
 An example where this is needed is in applying `TopCat.Presheaf.restrictOpen` to commutative rings.

diff --git a/Mathlib/Algebra/GroupWithZero/Range.lean b/Mathlib/Algebra/GroupWithZero/Range.lean
@@ -141,8 +141,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₀

diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/MappingCocone.lean b/Mathlib/Algebra/Homology/HomotopyCategory/MappingCocone.lean
@@ -239,7 +239,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)),

diff --git a/Mathlib/Algebra/Homology/Refinements.lean b/Mathlib/Algebra/Homology/Refinements.lean
@@ -67,7 +67,7 @@ lemma comp_homologyπ_eq_iff_up_to_refinements
     (i j : ι) (hi : c.prev j = i)
     {A : C} (z₂ z₂' : A ⟶ K.cycles j) : z₂ ≫ K.homologyπ j = z₂' ≫ K.homologyπ j ↔
       ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i),
-        π ≫ z₂ = π ≫ z₂' + x₁ ≫ K.toCycles i j:= by
+        π ≫ z₂ = π ≫ z₂' + x₁ ≫ K.toCycles i j := by
   subst hi
   exact (K.sc j).comp_homologyπ_eq_iff_up_to_refinements z₂ z₂'
 

diff --git a/Mathlib/Algebra/Homology/SpectralObject/Basic.lean b/Mathlib/Algebra/Homology/SpectralObject/Basic.lean
@@ -120,7 +120,7 @@ def sc₃ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) : ShortComplex C
   ShortComplex.mk _ _ (X.zero₃ f g fg h n₀ n₁ hn₁)
 
 lemma exact₁ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁ := by lia) :
-    (X.sc₁ f g fg h n₀ n₁ hn₁ ).Exact := by
+    (X.sc₁ f g fg h n₀ n₁ hn₁).Exact := by
   subst h
   exact (X.exact₁' n₀ n₁ hn₁ (mk₂ f g)).exact 0
 

diff --git a/Mathlib/Algebra/Homology/SpectralObject/Cycles.lean b/Mathlib/Algebra/Homology/SpectralObject/Cycles.lean
@@ -195,7 +195,7 @@ noncomputable def cyclesMap (α : mk₂ f g ⟶ mk₂ f' g') (n : ℤ) :
       rw [Category.assoc, X.δ_naturality f g f' g'
         (homMk₁ (α.app 0) (α.app 1) (naturality' α 0 1))
           (homMk₁ (α.app 1) (α.app 2) (naturality' α 1 2)) n (n + 1),
-        iCycles_δ_assoc _ _ _ _ _ , zero_comp])
+        iCycles_δ_assoc _ _ _ _ _, zero_comp])
 
 @[reassoc]
 lemma cyclesMap_i (α : mk₂ f g ⟶ mk₂ f' g') (β : mk₁ g ⟶ mk₁ g') (n : ℤ)
@@ -256,8 +256,8 @@ lemma opcyclesMap_comp (α : mk₂ f g ⟶ mk₂ f' g') (α' : mk₂ f' g' ⟶ m
       X.opcyclesMap f g f'' g'' α'' n := by
   subst h
   rw [← cancel_epi (X.pOpcycles f g n),
-    X.p_opcyclesMap_assoc f g f' g' α _ ,
-    X.p_opcyclesMap f' g' f'' g'' α' _ ,
+    X.p_opcyclesMap_assoc f g f' g' α _,
+    X.p_opcyclesMap f' g' f'' g'' α' _,
     ← Functor.map_comp_assoc]
   exact (X.p_opcyclesMap _ _ _ _ _ _ _ (by cat_disch)).symm
 
@@ -483,7 +483,7 @@ lemma pOpcycles_δFromOpcycles (hn₁ : n₀ + 1 = n₁) :
 @[reassoc (attr := simp)]
 lemma fromOpcyles_δ (hn₁ : n₀ + 1 = n₁ := by lia) :
     X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₀ ≫ X.δ f₁ f₂₃ n₀ n₁ hn₁ =
-      X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁  := by
+      X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁ := by
   rw [← cancel_epi (X.pOpcycles f₂ f₃ n₀),
     p_fromOpcycles_assoc, pOpcycles_δFromOpcycles,
     X.δ_naturality f₁ f₂ f₁ f₂₃ (𝟙 _) (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) n₀ n₁,

diff --git a/Mathlib/Algebra/Homology/SpectralObject/Differentials.lean b/Mathlib/Algebra/Homology/SpectralObject/Differentials.lean
@@ -52,7 +52,7 @@ noncomputable def d
   X.descE f₃ f₄ f₅ _ rfl n₀ n₁ n₂ (X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫
     X.toCycles f₁ f₂ _ rfl n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) (by
       rw [X.δ_naturality_assoc (f₁ ≫ f₂) f₃ (f₁ ≫ f₂) (f₃ ≫ f₄)
-        (𝟙 _) (twoδ₂Toδ₁ f₃ f₄  _ rfl) n₁ n₂ rfl hn₂, Functor.map_id, id_comp,
+        (𝟙 _) (twoδ₂Toδ₁ f₃ f₄ _ rfl) n₁ n₂ rfl hn₂, Functor.map_id, id_comp,
         δ_toCycles_assoc .., δToCycles_πE ..]) hn₁
           (by rw [δ_δ_assoc .., zero_comp])
 
@@ -96,7 +96,7 @@ lemma d_d (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia
     X.d f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫
       X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄ = 0 := by
   rw [← cancel_epi (X.πE f₅ f₆ f₇ n₀ n₁ n₂ hn₁ hn₂),
-    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁ ), comp_zero, comp_zero,
+    ← cancel_epi (X.toCycles f₅ f₆ _ rfl n₁), comp_zero, comp_zero,
     X.toCycles_πE_d_assoc f₃ f₄ f₅ f₆ f₇ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
     X.toCycles_πE_d f₁ f₂ f₃ f₄ f₅ _ rfl _ rfl n₁ n₂ n₃ n₄ hn₂ hn₃ hn₄,
     δ_δ_assoc .., zero_comp]
@@ -175,7 +175,7 @@ lemma cyclesMap_Ψ_exact (hn₁ : n₀ + 1 = n₁ := by lia) :
     X.liftCycles f₁₂ f₃ n₀ n₁ hn₁ (z ≫ X.iCycles f₂ f₃ n₀) ?_, ?_⟩ <;> dsimp
   · rw [assoc, ← X.Ψ_fromOpcycles f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ hn₁, reassoc_of% hz, zero_comp]
   · rw [← cancel_mono (X.iCycles f₂ f₃ n₀), id_comp, assoc,
-      X.cyclesMap_i _ _ _ _ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) (𝟙 _) n₀ (by cat_disch) ,
+      X.cyclesMap_i _ _ _ _ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) (𝟙 _) n₀ (by cat_disch),
       Functor.map_id, comp_id, liftCycles_i]
 
 set_option backward.isDefEq.respectTransparency false in
@@ -209,7 +209,7 @@ lemma πE_d_ιE
     (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) :
     X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫
       X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ = X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂ := by
-  rw [← cancel_epi (X.toCycles f₃ f₄ _ rfl n₁ ), toCycles_Ψ ..,
+  rw [← cancel_epi (X.toCycles f₃ f₄ _ rfl n₁), toCycles_Ψ ..,
     X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
     πE_ιE .., toCycles_i_assoc, ← X.δ_naturality_assoc (f₁ ≫ f₂) (f₃ ≫ f₄) f₂ (f₃ ≫ f₄)
       (twoδ₁Toδ₀ f₁ f₂ _ rfl) (𝟙 _) n₁ n₂ rfl hn₂, Functor.map_id, id_comp]

diff --git a/Mathlib/Algebra/Homology/SpectralObject/EpiMono.lean b/Mathlib/Algebra/Homology/SpectralObject/EpiMono.lean
@@ -53,7 +53,7 @@ lemma mono_map (α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂ f₃) (n₀ n₁
     (hα₃ : α.app 3 = 𝟙 _ := by cat_disch) (hn₁ : n₀ + 1 = n₁ := by lia)
     (hn₂ : n₁ + 1 = n₂ := by lia) (hn₃ : n₂ + 1 = n₃ := by lia) :
     Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂) := by
-  have := X.map_ιE  _ _ _ _ _ _ α (𝟙 _) n₀ n₁ n₂
+  have := X.map_ιE _ _ _ _ _ _ α (𝟙 _) n₀ n₁ n₂
   rw [opcyclesMap_id, comp_id] at this
   exact mono_of_mono_fac this
 

diff --git a/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean b/Mathlib/Algebra/Homology/SpectralObject/HasSpectralSequence.lean
@@ -277,7 +277,7 @@ by `data`. The conditions given allow to show that the homology of a page identi
 to the next page. -/
 class HasSpectralSequence : Prop where
   isZero_H_obj_mk₁_i₀_le (r r' : ℤ) (pq : κ) (hpq : ∀ (pq' : κ), ¬ ((c r).Rel pq pq'))
-    (n : ℤ) (hn : n = data.deg pq + 1 )
+    (n : ℤ) (hn : n = data.deg pq + 1)
     (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) :
       IsZero ((X.H n).obj (mk₁ (homOfLE (data.i₀_le r r' pq))))
   isZero_H_obj_mk₁_i₃_le (r r' : ℤ) (pq : κ) (hpq : ∀ (pq' : κ), ¬ ((c r).Rel pq' pq))
@@ -325,7 +325,7 @@ instance (E : SpectralObject C EInt) : E.HasSpectralSequence coreE₂Cohomologic
     exact hpq _ rfl
   isZero_H_obj_mk₁_i₃_le r r' pq hpq n hn hrr' hr := by
     exfalso
-    exact hpq (pq - (r, 1-r)) (by simp)
+    exact hpq (pq - (r, 1 - r)) (by simp)
 
 instance {l : ℕ} (E : SpectralObject C (Fin (l + 1))) :
     E.HasSpectralSequence (coreE₂CohomologicalFin l) where
@@ -375,7 +375,7 @@ variable [Y.IsFirstQuadrant]
 
 lemma isZero₁_of_isFirstQuadrant (i j : EInt) (hij : i ≤ j) (hj : j ≤ (0 : ℤ)) (n : ℤ) :
     IsZero ((Y.H n).obj (mk₁ (homOfLE hij))) :=
-  IsFirstQuadrant.isZero₁ i j hij  hj n
+  IsFirstQuadrant.isZero₁ i j hij hj n
 
 lemma isZero₂_of_isFirstQuadrant (i j : EInt) (hij : i ≤ j) (n : ℤ) (hi : n < i) :
     IsZero ((Y.H n).obj (mk₁ (homOfLE hij))) :=

diff --git a/Mathlib/Algebra/Homology/SpectralObject/Page.lean b/Mathlib/Algebra/Homology/SpectralObject/Page.lean
@@ -103,7 +103,7 @@ lemma shortComplexMap_id (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 =
 
 @[reassoc, simp]
 lemma shortComplexMap_comp (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
-    X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂  =
+    X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂ =
     X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
       X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂ := by
   ext
@@ -621,7 +621,7 @@ lemma cokernelSequenceOpcyclesE_exact
 /-- The map `E^n(f₁, f₂, f₃) ⟶ Z^n(f₁, f₂ ≫ f₃)`. -/
 noncomputable def EToCycles (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) :
     X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.cycles f₁ f₂₃ n₁ :=
-  X.liftCycles  _ _ _ _ hn₂
+  X.liftCycles _ _ _ _ hn₂
     (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₁) (by simp)
 
 @[reassoc (attr := simp)]

diff --git a/Mathlib/Algebra/Module/TransferInstance.lean b/Mathlib/Algebra/Module/TransferInstance.lean
@@ -63,6 +63,7 @@ def linearEquiv (e : α ≃ β) [AddCommMonoid β] [Module R β] :
       simp only [toFun_as_coe, RingHom.id_apply, EmbeddingLike.apply_eq_iff_eq]
       exact Iff.mpr (apply_eq_iff_eq_symm_apply _) rfl }
 
+set_option linter.style.whitespace false in -- the linter is wrong, even after lean4#12006
 variable (R) in
 /-- Transfer `Module.IsTorsionFree` across an `Equiv` -/
 protected lemma moduleIsTorsionFree (e : α ≃ β) [AddCommMonoid β] [Module R β]

diff --git a/Mathlib/Algebra/Order/CauSeq/Basic.lean b/Mathlib/Algebra/Order/CauSeq/Basic.lean
@@ -212,6 +212,7 @@ variable (abv) in
 /-- The constant Cauchy sequence. -/
 def const (x : β) : CauSeq β abv := ⟨fun _ ↦ x, IsCauSeq.const _⟩
 
+set_option linter.style.whitespace false in -- linter false positive
 /-- The constant Cauchy sequence -/
 local notation "const" => const abv
 
@@ -567,6 +568,7 @@ end DivisionRing
 
 section Abs
 
+set_option linter.style.whitespace false in -- false positive in the linter
 /-- The constant Cauchy sequence -/
 local notation "const" => const abs
 

diff --git a/Mathlib/Algebra/Order/GroupWithZero/Range.lean b/Mathlib/Algebra/Order/GroupWithZero/Range.lean
@@ -32,7 +32,7 @@ variable (f) in
 /-- The inclusion of `ValueGroup₀ f` into `WithZero Bˣ` as a homomorphism of monoids with zero. -/
 def orderMonoidWithZeroHom : ValueGroup₀ f →*₀o WithZero Bˣ where
   __ := WithZero.map' (valueGroup f).subtype
-  monotone' := map'_strictMono (Subtype.strictMono_coe _)|>.monotone
+  monotone' := map'_strictMono (Subtype.strictMono_coe _) |>.monotone
 
 lemma monoidWithZeroHom_strictMono :
     StrictMono (orderMonoidWithZeroHom f) :=

diff --git a/Mathlib/Algebra/Polynomial/RuleOfSigns.lean b/Mathlib/Algebra/Polynomial/RuleOfSigns.lean
@@ -126,6 +126,7 @@ section OrderedRing
 
 variable {R : Type*} [Ring R] [LinearOrder R] [IsOrderedRing R] (P : Polynomial R) {x : R}
 
+set_option linter.style.whitespace false in -- linter suggestion is undesirable
 /-- The number of sign changes does not change if we negate. -/
 @[simp]
 theorem signVariations_neg : signVariations (-P) = signVariations P := by

diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
@@ -1442,6 +1442,7 @@ theorem mk_univ_quaternionAlgebra : #(Set.univ : Set ℍ[R,c₁,c₂,c₃]) = #R
 theorem mk_univ_quaternionAlgebra_of_infinite [Infinite R] :
     #(Set.univ : Set ℍ[R,c₁,c₂,c₃]) = #R := by rw [mk_univ_quaternionAlgebra, pow_four]
 
+set_option linter.style.whitespace false in -- linter false positive around s!, TODO fix properly
 /-- Show the quaternion ⟨w, x, y, z⟩ as a string "{ re := w, imI := x, imJ := y, imK := z }".
 
 For the typical case of quaternions over ℝ, each component will show as a Cauchy sequence due to

diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Basic.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Basic.lean
@@ -100,6 +100,7 @@ universe r s u v
 
 variable {R : Type r} {S : Type s} {A F : Type u} {B K : Type v}
 
+set_option linter.style.whitespace false in -- linter false positive
 name_poly_vars X, Y, Z over R
 
 namespace WeierstrassCurve

diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Basic.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Basic.lean
@@ -100,6 +100,7 @@ universe r s u v
 
 variable {R : Type r} {S : Type s} {A F : Type u} {B K : Type v}
 
+set_option linter.style.whitespace false in -- linter false positive
 name_poly_vars X, Y, Z over R
 
 namespace WeierstrassCurve

diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean
@@ -119,6 +119,7 @@ lemma Y_eq_of_Y_ne [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (
   sub_eq_zero.mp <| (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_left <|
     mul_ne_zero (mul_ne_zero hPz hQz) <| sub_ne_zero.mpr hy
 
+set_option linter.style.whitespace false in -- TODO: fix the line break in the proof nicely!
 lemma Y_eq_of_Y_ne' [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
     (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z)
     (hy : P y * Q z ≠ W'.negY Q * P z) : P y * Q z = Q y * P z :=

diff --git a/Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean b/Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean
@@ -242,7 +242,7 @@ instance : InfSet (AbstractSimplicialComplex ι) where
         grind [IsRelLowerSet.mem_of_le, PreAbstractSimplicialComplex.isRelLowerSet_faces,
           mem_iInter]
       singleton_mem v := by
-        grind [Set.mem_iInter, Finset.singleton_nonempty, singleton_mem]  }
+        grind [Set.mem_iInter, Finset.singleton_nonempty, singleton_mem] }
 
 instance : Top (AbstractSimplicialComplex ι) where
   top :=

diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/CompStructTruncated.lean b/Mathlib/AlgebraicTopology/SimplicialSet/CompStructTruncated.lean
@@ -146,6 +146,7 @@ def idCompId (x : X _⦋0⦌₂) :
     CompStruct (.id x) (.id x) (.id x) :=
   idComp _
 
+set_option linter.style.whitespace false in -- linter false positive
 attribute [local simp ←] FunctorToTypes.naturality in
 /-- The image of a `Edge.CompStruct` by a morphism of `2`-truncated
 simplicial sets. -/