chore: annotate manual alignment (leanprover-community#33789)

grunweg · grunweg · commit 3c3271860241 · 2026-01-09T18:15:22.000Z
The whitespace linter does not support this: disable the linter in these instances. Extracted from leanprover-community#30658 to minimise the diff.
diff --git a/Archive/Arithcc.lean b/Archive/Arithcc.lean
@@ -265,6 +265,7 @@ theorem write_eq_implies_stateEq {t : Register} {v : Word} {ζ₁ ζ₂ : State}
   rwa [if_neg (ne_of_lt hr)] at h
 
 set_option linter.flexible false in
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The main **compiler correctness theorem**.
 
 Unlike Theorem 1 in the paper, both `map` and the assumption on `t` are explicit.
diff --git a/Archive/Examples/IfNormalization/Result.lean b/Archive/Examples/IfNormalization/Result.lean
@@ -49,6 +49,7 @@ We don't want a `simp` lemma for `(ite i t e).eval` in general, only once we kno
   | .ite i t e => 2 * normSize i + max (normSize t) (normSize e) + 1
 
 set_option linter.flexible false in
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Normalizes the expression at the same time as assigning all variables in
 `e` to the literal Booleans given by `l` -/
 def normalize (l : AList (fun _ : ℕ => Bool)) :
diff --git a/Archive/Examples/Kuratowski.lean b/Archive/Examples/Kuratowski.lean
@@ -81,6 +81,7 @@ theorem isOpen_of_mem_theOpenSix (h : t ∈ theOpenSix s) : IsOpen t := by
 theorem mem_theOpenSix_iff : t ∈ theOpenSix s ↔ tᶜ ∈ theClosedSix s := by
   conv_lhs => rw [theOpenSix, ← compl_compl t, Multiset.mem_map_of_injective compl_injective]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Six inequalities that suffice to deduce the six closed sets obtained from a given set
 contain no duplicates. -/
 def TheSixIneq (s : Set X) : Prop :=
diff --git a/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean b/Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean
@@ -94,12 +94,14 @@ def const : 𝟭 _ ⟶ I R G where
 
 namespace MultiInd
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The n-th functor taking `M` to `C(G, C(G,...,C(G, M)))` (with n `G`s).
 These functors form a complex, see `MultiInd.complex`. -/
 def functor : ℕ → Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G
   | 0     => 𝟭 _
   | n + 1 => functor n ⋙ I R G
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The differential map in `MultiInd.complex`. -/
 def d : ∀ n : ℕ, functor R G n ⟶ functor R G (n + 1)
   | 0     => const R G
diff --git a/Mathlib/Algebra/Group/Int/Defs.lean b/Mathlib/Algebra/Group/Int/Defs.lean
@@ -66,7 +66,8 @@ These also prevent non-computable instances like `Int.instNormedCommRing` being
 these instances non-computably.
 -/
 
-set_option linter.style.whitespace false
+section
+set_option linter.style.whitespace false -- manual alignment is not recognised
 
 instance instAddCommMonoid    : AddCommMonoid ℤ    := by infer_instance
 instance instAddMonoid        : AddMonoid ℤ        := by infer_instance
@@ -77,6 +78,8 @@ instance instAddGroup         : AddGroup ℤ         := by infer_instance
 instance instAddCommSemigroup : AddCommSemigroup ℤ := by infer_instance
 instance instAddSemigroup     : AddSemigroup ℤ     := by infer_instance
 
+end
+
 -- This lemma is higher priority than later `_root_.nsmul_eq_mul` so that the `simpNF` is happy
 @[simp high] protected lemma nsmul_eq_mul (n : ℕ) (a : ℤ) : n • a = n * a := rfl
 
diff --git a/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean b/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean
@@ -174,6 +174,7 @@ lemma pairwise_baseOf_div_notMem [InvolutiveInv ι] [CommGroup S] [IsOrderedMono
     (baseOf v f).Pairwise fun i j ↦ v i / v j ∉ range v :=
   pairwise_div_notMem_range' v hv_inv f hf (baseOf v f) (.refl _)
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 @[to_additive]
 lemma mem_or_inv_mem_closure_baseOf [Finite ι] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S]
     (v : ι → G) (hv_inv : ∀ i, v i⁻¹ = (v i)⁻¹)
diff --git a/Mathlib/Algebra/Group/Nat/Defs.lean b/Mathlib/Algebra/Group/Nat/Defs.lean
@@ -66,7 +66,7 @@ instance instIsAddTorsionFree : IsAddTorsionFree ℕ where
 These also prevent non-computable instances being used to construct these instances non-computably.
 -/
 
-set_option linter.style.whitespace false
+set_option linter.style.whitespace false -- manual alignment is not recognised
 
 instance instAddCommMonoid    : AddCommMonoid ℕ    := by infer_instance
 instance instAddMonoid        : AddMonoid ℕ        := by infer_instance
diff --git a/Mathlib/Algebra/Lie/LieTheorem.lean b/Mathlib/Algebra/Lie/LieTheorem.lean
@@ -164,6 +164,7 @@ variable {V : Type*} [AddCommGroup V] [Module k V] [LieRingModule L V] [LieModul
 
 variable [CharZero k] [Module.Finite k V]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 open Submodule in
 theorem exists_nontrivial_weightSpace_of_lieIdeal [LieModule.IsTriangularizable k L V]
     (A : LieIdeal k L) (hA : IsCoatom A.toSubmodule)
diff --git a/Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean b/Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
@@ -64,6 +64,7 @@ theorem apply_intCast_le_one_of_isNonarchimedean [IsStrictOrderedRing R]
   obtain ⟨a, rfl | rfl⟩ := Int.eq_nat_or_neg n <;>
   simp [apply_natCast_le_one_of_isNonarchimedean hna]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 lemma add_eq_right_of_lt {F α : Type*} [AddGroup α] [FunLike F α R]
     [AddGroupSeminormClass F α R] {f : F} (hna : IsNonarchimedean f) {x y : α}
     (h_lt : f x < f y) : f (x + y) = f y := by
@@ -78,6 +79,7 @@ lemma add_eq_right_of_lt {F α : Type*} [AddGroup α] [FunLike F α R]
       exact max_lt h_lt <| lt_of_le_of_ne h1 h
     _   = f y := max_self (f y)
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 lemma add_eq_left_of_lt {F α : Type*} [AddGroup α] [FunLike F α R]
     [AddGroupSeminormClass F α R] {f : F} (hna : IsNonarchimedean f) {x y : α}
     (h_lt : f y < f x) : f (x + y) = f x := by
diff --git a/Mathlib/Algebra/Polynomial/Basic.lean b/Mathlib/Algebra/Polynomial/Basic.lean
@@ -174,6 +174,7 @@ theorem ofFinsupp_smul {S : Type*} [SMulZeroClass S R] (a : S) (b) :
     (⟨a • b⟩ : R[X]) = (a • ⟨b⟩ : R[X]) :=
   rfl
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 @[simp]
 theorem ofFinsupp_pow (a) (n : ℕ) : (⟨a ^ n⟩ : R[X]) = ⟨a⟩ ^ n := by
   change _ = npowRec n _
diff --git a/Mathlib/Algebra/Ring/Int/Defs.lean b/Mathlib/Algebra/Ring/Int/Defs.lean
@@ -81,7 +81,7 @@ These also prevent non-computable instances like `Int.normedCommRing` being used
 these instances non-computably.
 -/
 
-set_option linter.style.whitespace false
+set_option linter.style.whitespace false -- manual alignment is not recognised
 
 instance instCommSemiring : CommSemiring ℤ := inferInstance
 instance instSemiring     : Semiring ℤ     := inferInstance
diff --git a/Mathlib/Algebra/Ring/SumsOfSquares.lean b/Mathlib/Algebra/Ring/SumsOfSquares.lean
@@ -31,6 +31,7 @@ We introduce a predicate for sums of squares in a ring.
 
 variable {R : Type*}
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /--
 The property of being a sum of squares is defined inductively by:
 `0 : R` is a sum of squares and if `s : R` is a sum of squares,
@@ -41,6 +42,7 @@ inductive IsSumSq [Mul R] [Add R] [Zero R] : R → Prop
   | zero                                    : IsSumSq 0
   | sq_add (a : R) {s : R} (hs : IsSumSq s) : IsSumSq (a * a + s)
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Alternative induction scheme for `IsSumSq` which uses `IsSquare`. -/
 theorem IsSumSq.rec' [Mul R] [Add R] [Zero R]
     {motive : (s : R) → (h : IsSumSq s) → Prop}
@@ -205,6 +207,7 @@ theorem IsSumSq.prod [CommSemiring R] {ι : Type*} {I : Finset ι} {x : ι → R
     (hx : ∀ i ∈ I, IsSumSq <| x i) : IsSumSq (∏ i ∈ I, x i) := by
   simpa using prod_mem (S := Subsemiring.sumSq R) (by simpa)
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /--
 In a linearly ordered semiring with the property `a ≤ b → ∃ c, a + c = b` (e.g. `ℕ`),
 sums of squares are non-negative.
diff --git a/Mathlib/Algebra/Star/RingQuot.lean b/Mathlib/Algebra/Star/RingQuot.lean
@@ -24,6 +24,7 @@ section StarRing
 
 variable [StarRing R]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 theorem Rel.star (hr : ∀ a b, r a b → r (star a) (star b))
     ⦃a b : R⦄ (h : Rel r a b) : Rel r (star a) (star b) := by
   induction h with
diff --git a/Mathlib/AlgebraicGeometry/IdealSheaf/Functorial.lean b/Mathlib/AlgebraicGeometry/IdealSheaf/Functorial.lean
@@ -118,7 +118,9 @@ variable (I I₁ I₂ : X.IdealSheafData) (J J₁ J₂ : Y.IdealSheafData) (f :
 /-- Pushforward and pullback of ideal sheaves forms a Galois connection. -/
 lemma map_gc : GaloisConnection (comap · f) (map · f) := fun _ _ ↦ le_map_iff_comap_le.symm
 
-set_option linter.style.whitespace false
+section
+set_option linter.style.whitespace false -- manual alignment is not recognised
+
 lemma map_mono          : Monotone (map · f)                          := (map_gc f).monotone_u
 lemma comap_mono        : Monotone (comap · f)                        := (map_gc f).monotone_l
 lemma le_map_comap      : J ≤ (J.comap f).map f                       := (map_gc f).le_u_l J
@@ -127,7 +129,8 @@ lemma comap_map_le      : (I.map f).comap f ≤ I                       := (map_
 @[simp] lemma comap_bot : comap ⊥ f = ⊥                               := (map_gc f).l_bot
 @[simp] lemma map_inf   : map (I₁ ⊓ I₂) f = map I₁ f ⊓ map I₂ f       := (map_gc f).u_inf
 @[simp] lemma comap_sup : comap (J₁ ⊔ J₂) f = comap J₁ f ⊔ comap J₂ f := (map_gc f).l_sup
-set_option linter.style.whitespace true
+
+end
 
 end gc
 
diff --git a/Mathlib/Analysis/Complex/HasPrimitives.lean b/Mathlib/Analysis/Complex/HasPrimitives.lean
@@ -140,6 +140,7 @@ section ContinuousOnBall
 variable (f_cont : ContinuousOn f (ball c r)) {z : ℂ} (hz : z ∈ ball c r)
 include f_cont hz
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 omit [CompleteSpace E] in
 /-- If a function `f` `IsConservativeOn` on a disk of center `c`, then for points `z` in this disk,
 the wedge integral from `c` to `z` is additive under a detour through a nearby point `w`. -/
diff --git a/Mathlib/Analysis/Complex/Liouville.lean b/Mathlib/Analysis/Complex/Liouville.lean
@@ -129,6 +129,7 @@ theorem exists_eq_const_of_bounded {f : E → F} (hf : Differentiable ℂ f)
     (hb : IsBounded (range f)) : ∃ c, f = const E c :=
   (hf.exists_const_forall_eq_of_bounded hb).imp fun _ => funext
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- A corollary of Liouville's theorem where the function tends to a finite value at infinity
 (i.e., along `Filter.cocompact`, which in proper spaces coincides with `Bornology.cobounded`). -/
 theorem eq_const_of_tendsto_cocompact [Nontrivial E] {f : E → F} (hf : Differentiable ℂ f) {c : F}
diff --git a/Mathlib/Analysis/Normed/Algebra/Spectrum.lean b/Mathlib/Analysis/Normed/Algebra/Spectrum.lean
@@ -209,6 +209,7 @@ open NNReal
 
 variable {A : Type*} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] [NormOneClass A]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 theorem le_nnnorm_of_mem {a : A} {r : ℝ≥0} (hr : r ∈ spectrum ℝ≥0 a) :
     r ≤ ‖a‖₊ := calc
   r ≤ ‖(r : ℝ)‖ := Real.le_norm_self _
diff --git a/Mathlib/Analysis/Normed/Group/Tannery.lean b/Mathlib/Analysis/Normed/Group/Tannery.lean
@@ -23,6 +23,7 @@ public section
 
 open Filter Topology
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- **Tannery's theorem**: topological sums commute with termwise limits, when the norms of the
 summands are eventually uniformly bounded by a summable function.
 
diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean
@@ -356,6 +356,7 @@ theorem is_real_TFAE (z : K) :
   tfae_have 5 → 1 := fun hz => by rwa [isSelfAdjoint_iff] at hz
   tfae_finish
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 theorem conj_eq_iff_real {z : K} : conj z = z ↔ ∃ r : ℝ, z = (r : K) :=
   calc
     _ ↔ ∃ r : ℝ, (r : K) = z := (is_real_TFAE z).out 0 1
diff --git a/Mathlib/Analysis/SpecialFunctions/CompareExp.lean b/Mathlib/Analysis/SpecialFunctions/CompareExp.lean
@@ -95,6 +95,7 @@ theorem tendsto_norm (hl : IsExpCmpFilter l) : Tendsto norm l atTop :=
 theorem isLittleO_log_re_re (hl : IsExpCmpFilter l) : (fun z => Real.log z.re) =o[l] re :=
   Real.isLittleO_log_id_atTop.comp_tendsto hl.tendsto_re
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 theorem isLittleO_im_pow_exp_re (hl : IsExpCmpFilter l) (n : ℕ) :
     (fun z : ℂ => z.im ^ n) =o[l] fun z => Real.exp z.re :=
   flip IsLittleO.of_pow two_ne_zero <|
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean b/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
@@ -179,6 +179,7 @@ lemma norm_log_one_add_sub_self_le {z : ℂ} (hz : ‖z‖ < 1) :
   · simp [logTaylor_succ, logTaylor_zero, sub_eq_add_neg]
   · norm_num
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 open scoped Topology in
 lemma log_sub_logTaylor_isBigO (n : ℕ) :
     (fun z ↦ log (1 + z) - logTaylor (n + 1) z) =O[𝓝 0] fun z ↦ z ^ (n + 1) := by
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Basic.lean
@@ -98,6 +98,7 @@ evaluates on `2 * cos θ` to the value `sin ((n + 1) * θ) / sin θ`. -/
 theorem S_two_mul_complex_cos (n : ℤ) : (S ℂ n).eval (2 * cos θ) * sin θ = sin ((n + 1) * θ) := by
   simp [S_eq_U_comp_half_mul_X]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cosh θ` to the
 value `cosh (n * θ)`. -/
 @[simp]
@@ -108,6 +109,7 @@ theorem T_complex_cosh (n : ℤ) : (T ℂ n).eval (cosh θ) = cosh (n * θ) := c
   _ = cos (n * θ * I)                   := by rw [mul_assoc]
   _ = cosh (n * θ)                      := cos_mul_I (n * θ)
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cosh θ` to the
 value `sinh ((n + 1) * θ) / sinh θ`. -/
 @[simp]
diff --git a/Mathlib/CategoryTheory/Category/Factorisation.lean b/Mathlib/CategoryTheory/Category/Factorisation.lean
@@ -29,6 +29,7 @@ universe v u
 
 variable {C : Type u} [Category.{v} C]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Factorisations of a morphism `f` as a structure, containing, one object, two morphisms,
 and the condition that their composition equals `f`. -/
 structure Factorisation {X Y : C} (f : X ⟶ Y) where
diff --git a/Mathlib/CategoryTheory/Iso.lean b/Mathlib/CategoryTheory/Iso.lean
@@ -71,7 +71,7 @@ variable {C : Type u} [Category.{v} C] {X Y Z : C}
 
 namespace Iso
 
-set_option linter.style.whitespace false in -- false positive, calc blocks
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 @[ext, grind ext]
 theorem ext ⦃α β : X ≅ Y⦄ (w : α.hom = β.hom) : α = β :=
   suffices α.inv = β.inv by grind [Iso]
diff --git a/Mathlib/Combinatorics/Additive/VerySmallDoubling.lean b/Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
@@ -609,6 +609,7 @@ private lemma IsAtom.eq_of_inter_nonempty (hK : K ≤ 1) (hS : S.Nonempty)
   replace hB := eq_of_subset_of_card_le inter_subset_right hB
   exact hA.symm.trans hB
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- For `K < 1` and `S ⊆ G` finite and nonempty, the value of connectivity is attained by a
 nonempty finite subset of `G`. That is, a fragment for given `K` and `S` exists. -/
 private lemma exists_nonempty_isFragment (hK : K < 1) (hS : S.Nonempty) :
@@ -717,6 +718,7 @@ private lemma exists_subgroup_isAtom (hK : K < 1) (hS : S.Nonempty) :
   · simpa only [← mem_coe, coe_smul_finset] using H.mem_carrier
   · simpa [Set.toFinset_smul_set, toFinset_coe, H] using IsAtom.smul_finset n⁻¹ hN
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- If `S` is nonempty such that there is `A` with `|S| ≤ |A|` such that `|A * S| ≤ (2 - ε) * |S|`
 for some `0 < ε ≤ 1`, then there is a finite subgroup `H` of `G` of size `|H| ≤ (2 / ε - 1) * |S|`
 such that `S` is covered by at most `2 / ε - 1` right cosets of `H`. -/
diff --git a/Mathlib/Data/Fin/Tuple/Curry.lean b/Mathlib/Data/Fin/Tuple/Curry.lean
@@ -35,6 +35,7 @@ namespace Function.FromTypes
 
 open Matrix (vecCons vecHead vecTail vecEmpty)
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Uncurry all the arguments of `Function.FromTypes p τ` to get
 a function from a tuple.
 
@@ -44,6 +45,7 @@ def uncurry : {n : ℕ} → {p : Fin n → Type u} → {τ : Type u} →
   | 0    , _, _, f => fun _    => f
   | _ + 1, _, _, f => fun args => (f (args 0)).uncurry (args ∘' Fin.succ)
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Curry all the arguments of `Function.FromTypes p τ` to get a function from a tuple. -/
 def curry : {n : ℕ} → {p : Fin n → Type u} → {τ : Type u} →
     (((i : Fin n) → p i) → τ) → Function.FromTypes p τ
diff --git a/Mathlib/Data/List/Sort.lean b/Mathlib/Data/List/Sort.lean
@@ -249,6 +249,7 @@ alias sorted_insertionSort := pairwise_insertionSort
 
 end TotalAndTransitive
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /--
 If `c` is a sorted sublist of `l`, then `c` is still a sublist of `insertionSort r l`.
 -/
@@ -274,6 +275,7 @@ theorem pair_sublist_insertionSort {a b : α} {l : List α} (hab : r a b) (h : [
 
 variable [Std.Antisymm r] [IsTotal α r] [IsTrans α r]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /--
 A version of `insertionSort_stable` which only assumes `c <+~ l` (instead of `c <+ l`), but
 additionally requires `Std.Antisymm r`, `IsTotal α r` and `IsTrans α r`.
diff --git a/Mathlib/Data/Nat/ChineseRemainder.lean b/Mathlib/Data/Nat/ChineseRemainder.lean
@@ -58,6 +58,7 @@ lemma modEq_list_map_prod_iff {a b} {s : ι → ℕ} {l : List ι} (co : l.Pairw
 
 variable (a s : ι → ℕ)
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The natural number less than `(l.map s).prod` congruent to
 `a i` mod `s i` for all  `i ∈ l`. -/
 def chineseRemainderOfList : (l : List ι) → l.Pairwise (Coprime on s) →
diff --git a/Mathlib/Data/Num/Bitwise.lean b/Mathlib/Data/Num/Bitwise.lean
@@ -113,6 +113,7 @@ instance : HShiftLeft PosNum Nat PosNum where hShiftLeft := PosNum.shiftl
 
 @[simp] lemma shiftl_eq_shiftLeft (p : PosNum) (n : Nat) : p.shiftl n = p <<< n := rfl
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 -- This shows that the tail-recursive definition is the same as the more naïve recursion.
 theorem shiftl_succ_eq_bit0_shiftl : ∀ (p : PosNum) (n : Nat), p <<< n.succ = bit0 (p <<< n)
   | _, 0       => rfl
diff --git a/Mathlib/Data/Prod/Basic.lean b/Mathlib/Data/Prod/Basic.lean
@@ -155,6 +155,7 @@ instance {r : α → α → Prop} {s : β → β → Prop} [Std.Refl s] : Std.Re
 instance [Std.Irrefl r] [Std.Irrefl s] : Std.Irrefl (Prod.Lex r s) :=
   ⟨by rintro ⟨i, a⟩ (⟨_, _, h⟩ | ⟨_, h⟩) <;> exact irrefl _ h⟩
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 @[trans]
 theorem Lex.trans {r : α → α → Prop} {s : β → β → Prop} [IsTrans α r] [IsTrans β s] :
     ∀ {x y z : α × β}, Prod.Lex r s x y → Prod.Lex r s y z → Prod.Lex r s x z
diff --git a/Mathlib/LinearAlgebra/Complex/Module.lean b/Mathlib/LinearAlgebra/Complex/Module.lean
@@ -499,6 +499,7 @@ lemma realPart_ofReal (r : ℝ) : (ℜ (r : ℂ) : ℂ) = r := by
 lemma imaginaryPart_ofReal (r : ℝ) : ℑ (r : ℂ) = 0 := by
   ext1; simp [imaginaryPart_apply_coe, conj_ofReal]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 lemma Complex.coe_realPart (z : ℂ) : (ℜ z : ℂ) = z.re := calc
   (ℜ z : ℂ) = (↑(ℜ (↑z.re + ↑z.im * I))) := by congrm (ℜ $((re_add_im z).symm))
   _         = z.re                       := by
diff --git a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@@ -226,6 +226,7 @@ lemma hasUnifEigenvalue_iff_mem_spectrum [FiniteDimensional K V] {f : End K V} {
 
 alias ⟨_, HasUnifEigenvalue.of_mem_spectrum⟩ := hasUnifEigenvalue_iff_mem_spectrum
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 lemma genEigenspace_div (f : End K V) (a b : K) (hb : b ≠ 0) :
     genEigenspace f (a / b) 1 = LinearMap.ker (b • f - a • 1) :=
   calc
diff --git a/Mathlib/LinearAlgebra/RootSystem/Base.lean b/Mathlib/LinearAlgebra/RootSystem/Base.lean
@@ -328,6 +328,7 @@ variable {P : RootPairing ι R M N} (b : P.Base)
 
 include b
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 lemma exists_root_eq_sum_nat_or_neg (i : ι) :
     ∃ f : ι → ℕ, f.support ⊆ b.support ∧
       (P.root i =   ∑ j ∈ b.support, f j • P.root j ∨
diff --git a/Mathlib/LinearAlgebra/RootSystem/RootPositive.lean b/Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
@@ -186,6 +186,7 @@ lemma pairingIn_mul_eq_pairingIn_mul_swap :
   simpa only [← (algebraMap_injective S R).eq_iff, algebraMap_pairingIn, map_mul,
     B.algebraMap_rootLength] using B.toInvariantForm.pairing_mul_eq_pairing_mul_swap i j
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 @[simp]
 lemma zero_lt_apply_root_root_iff [IsStrictOrderedRing S]
     (hi : P.root i ∈ span S (range P.root) := subset_span (mem_range_self i))
diff --git a/Mathlib/Logic/Function/FromTypes.lean b/Mathlib/Logic/Function/FromTypes.lean
@@ -25,6 +25,7 @@ namespace Function
 
 open Matrix (vecCons vecHead vecTail vecEmpty)
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The type of `n`-ary functions `p 0 → p 1 → ... → p (n - 1) → τ`. -/
 def FromTypes : {n : ℕ} → (Fin n → Type u) → Type u → Type u
   | 0    , _, τ => τ
@@ -65,6 +66,7 @@ def fromTypes_cons_equiv {n} (α : Type u) (p : Fin n → Type u) (τ : Type u)
 
 namespace FromTypes
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Constant `n`-ary function with value `t`. -/
 def const : {n : ℕ} → (p : Fin n → Type u) → {τ : Type u} → (t : τ) → FromTypes p τ
   | 0,     _, _, t => t
diff --git a/Mathlib/MeasureTheory/Function/UnifTight.lean b/Mathlib/MeasureTheory/Function/UnifTight.lean
@@ -235,6 +235,7 @@ private theorem unifTight_of_tendsto_Lp (hp' : p ≠ ∞) (hf : ∀ n, MemLp (f
   · exact unifTight_const hp' hg
   · exact unifTight_of_tendsto_Lp_zero hp' (fun n => (hf n).sub hg) hfg
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /- Next we deal with the forward direction. The `MemLp` and `TendstoInMeasure` hypotheses
 are unwrapped and strengthened (by known lemmas) to also have the `StronglyMeasurable`
 and a.e. convergence hypotheses. The bulk of the proof is done under these stronger hypotheses. -/
diff --git a/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean b/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean
diff --git a/Mathlib/Order/Filter/Prod.lean b/Mathlib/Order/Filter/Prod.lean
diff --git a/Mathlib/Order/Interval/Finset/Basic.lean b/Mathlib/Order/Interval/Finset/Basic.lean
diff --git a/Mathlib/Order/PrimeSeparator.lean b/Mathlib/Order/PrimeSeparator.lean
diff --git a/Mathlib/RingTheory/Polynomial/Resultant/Basic.lean b/Mathlib/RingTheory/Polynomial/Resultant/Basic.lean
