chore: annotate locations using manual alignment (leanprover-community#33976)

Continuation of leanprover-community#33789: this is required to get useful output from the whitespace linter.

Author: grunweg

Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

@@ -75,6 +75,7 @@ instance : Category (TopModuleCat R) where
   id M := ⟨ContinuousLinearMap.id R M⟩
   comp φ ψ := ⟨ψ.hom' ∘L φ.hom'⟩
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 set_option backward.privateInPublic true in
 set_option backward.privateInPublic.warn false in
 instance : ConcreteCategory (TopModuleCat R) (· →L[R] ·) where

Mathlib/Algebra/GroupWithZero/WithZero.lean

@@ -91,6 +91,7 @@ instance instMulZeroOneClass [MulOneClass α] : MulZeroOneClass (WithZero α) wh
   one_mul := Option.map₂_left_identity one_mul
   mul_one := Option.map₂_right_identity mul_one
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Coercion as a monoid hom. -/
 @[simps apply]
 def coeMonoidHom : α →* WithZero α where

Mathlib/Algebra/Polynomial/Derivation.lean

@@ -106,6 +106,7 @@ variable {R A M : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCom
 
 open Polynomial Module
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /--
 For a derivation `d : A → M` and an element `a : A`, `d.compAEval a` is the
 derivation of `R[X]` which takes a polynomial `f` to `d(aeval a f)`.

Mathlib/Algebra/Polynomial/Taylor.lean

@@ -178,6 +178,7 @@ section CommRing
 
 variable {R : Type*} [CommRing R] (r : R) (f : R[X])
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- `Polynomial.taylor` as an `AlgEquiv` for commutative rings. -/
 noncomputable def taylorEquiv (r : R) : R[X] ≃ₐ[R] R[X] where
   invFun      := taylorAlgHom (-r)

Mathlib/Algebra/Ring/SumsOfSquares.lean

@@ -66,6 +66,7 @@ theorem IsSumSq.add [AddMonoid R] [Mul R] {s₁ s₂ : R}
 namespace AddSubmonoid
 variable {T : Type*} [AddMonoid T] [Mul T] {s : T}
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 variable (T) in
 /--
 In an additive monoid with multiplication `R`, `AddSubmonoid.sumSq R` is the submonoid of sums of

Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

@@ -259,6 +259,7 @@ theorem single_zero (a : G) : (single a 0 : SkewMonoidAlgebra k G) = 0 := by
 theorem single_eq_zero {a : G} {b : k} : single a b = 0 ↔ b = 0 := by
   simp [← toFinsupp_inj]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Group isomorphism between `SkewMonoidAlgebra k G` and `G →₀ k`. -/
 @[simps apply symm_apply]
 def toFinsuppAddEquiv : SkewMonoidAlgebra k G ≃+ (G →₀ k) where
@@ -481,6 +482,7 @@ section mapDomain
 
 variable {G' G'' : Type*} (f : G → G') {g : G' → G''} (v : SkewMonoidAlgebra k G)
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Given `f : G → G'` and `v : SkewMonoidAlgebra k G`, `mapDomain f v : SkewMonoidAlgebra k G'`
 is the finitely supported additive homomorphism whose value at `a : G'` is the sum of `v x` over
 all `x` such that `f x = a`.
@@ -1087,6 +1089,7 @@ variable (k G)
 
 variable [Monoid G] [MulSemiringAction G k]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The embedding of a monoid into its skew monoid algebra. -/
 def of : G →* SkewMonoidAlgebra k G where
   toFun a      := single a 1

Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean

@@ -148,6 +148,7 @@ section domCongr
 
 variable {A : Type*}
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Given `AddCommMonoid A` and `e : G ≃ H`, `domCongr e` is the corresponding `Equiv` between
 `SkewMonoidAlgebra A G` and `SkewMonoidAlgebra A H`. -/
 @[simps apply]
@@ -219,6 +220,7 @@ variable [Semiring k] [Monoid G] [MulSemiringAction G k]
 variable {V : Type*} [AddCommMonoid V] [Module k V] [Module (SkewMonoidAlgebra k G) V]
   [IsScalarTower k (SkewMonoidAlgebra k G) V]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- A submodule over `k` which is stable under scalar multiplication by elements of `G` is a
 submodule over `SkewMonoidAlgebra k G` -/
 def submoduleOfSmulMem (W : Submodule k V) (h : ∀ (g : G) (v : V), v ∈ W → of k G g • v ∈ W) :

Mathlib/Analysis/Normed/Unbundled/AlgebraNorm.lean

@@ -66,6 +66,7 @@ instance : FunLike (AlgebraNorm R S) S ℝ where
     erw [h]
     rfl
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 instance algebraNormClass : AlgebraNormClass (AlgebraNorm R S) R S where
   map_zero f        := f.map_zero'
   map_add_le_add f  := f.add_le'
@@ -88,6 +89,7 @@ theorem extends_norm' (hf1 : f 1 = 1) (a : R) : f (a • (1 : S)) = ‖a‖ := b
 theorem extends_norm (hf1 : f 1 = 1) (a : R) : f (algebraMap R S a) = ‖a‖ := by
   rw [Algebra.algebraMap_eq_smul_one]; exact extends_norm' hf1 _
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The restriction of an algebra norm to a subalgebra. -/
 def restriction (A : Subalgebra R S) (f : AlgebraNorm R S) : AlgebraNorm R A where
   toFun x     := f x.val
@@ -99,6 +101,7 @@ def restriction (A : Subalgebra R S) (f : AlgebraNorm R S) : AlgebraNorm R A whe
     rw [← ZeroMemClass.coe_eq_zero]; exact eq_zero_of_map_eq_zero f hx
   smul' r x := map_smul_eq_mul _ _ _
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The restriction of an algebra norm in a scalar tower. -/
 def isScalarTower_restriction {A : Type*} [CommRing A] [Algebra R A] [Algebra A S]
     [IsScalarTower R A S] (hinj : Function.Injective (algebraMap A S)) (f : AlgebraNorm R S) :
@@ -151,6 +154,7 @@ instance : FunLike (MulAlgebraNorm R S) S ℝ where
     simp only [AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe, DFunLike.coe_fn_eq] at h
     obtain ⟨⟨_, _⟩, _⟩ := f; obtain ⟨⟨_, _⟩, _⟩ := f'; congr
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 instance mulAlgebraNormClass : MulAlgebraNormClass (MulAlgebraNorm R S) R S where
   map_zero f        := f.map_zero'
   map_add_le_add f  := f.add_le'
@@ -180,6 +184,7 @@ namespace MulRingNorm
 
 variable {R : Type*} [NonAssocRing R]
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The ring norm underlying a multiplicative ring norm. -/
 def toRingNorm (f : MulRingNorm R) : RingNorm R where
   toFun       := f

Mathlib/Analysis/Normed/Unbundled/InvariantExtension.lean

@@ -50,6 +50,7 @@ variable {K : Type*} [NormedField K] {L : Type*} [Field L] [Algebra K L]
 namespace IsUltrametricDist
 section algNormOfAlgEquiv
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- Given a normed field `K`, a finite algebraic extension `L/K` and `σ : L ≃ₐ[K] L`, the function
 `L → ℝ` sending `x : L` to `‖ σ x ‖`, where `‖ ⬝ ‖` is any power-multiplicative algebra norm on `L`
 extending the norm on `K`, is an algebra norm on `K`. -/

Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean

@@ -420,6 +420,7 @@ def normRingNorm (R : Type*) [NonUnitalNormedRing R] : RingNorm R :=
 
 open Int
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The seminorm on a `SeminormedRing`, as a `RingSeminorm`. -/
 def SeminormedRing.toRingSeminorm (R : Type*) [SeminormedRing R] : RingSeminorm R where
   toFun     := norm
@@ -428,6 +429,7 @@ def SeminormedRing.toRingSeminorm (R : Type*) [SeminormedRing R] : RingSeminorm
   mul_le'   := norm_mul_le
   neg'      := norm_neg
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The norm on a `NormedRing`, as a `RingNorm`. -/
 @[simps]
 def NormedRing.toRingNorm (R : Type*) [NormedRing R] : RingNorm R where
@@ -443,6 +445,7 @@ theorem NormedRing.toRingNorm_apply (R : Type*) [NormedRing R] (x : R) :
     (NormedRing.toRingNorm R) x = ‖x‖ :=
   rfl
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The norm on a `NormedField`, as a `MulRingNorm`. -/
 def NormedField.toMulRingNorm (R : Type*) [NormedField R] : MulRingNorm R where
   toFun     := norm
@@ -453,6 +456,7 @@ def NormedField.toMulRingNorm (R : Type*) [NormedField R] : MulRingNorm R where
   neg'      := norm_neg
   eq_zero_of_map_eq_zero' x hx := by rw [← norm_eq_zero]; exact hx
 
+set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The norm on a `NormedField`, as an `AbsoluteValue`. -/
 def NormedField.toAbsoluteValue (R : Type*) [NormedField R] : AbsoluteValue R ℝ where
   toFun     := norm