style: remove trailing whitespace and modify the linter to detect it (#…

…6519)

Archive/Imo/Imo2011Q3.lean

@@ -54,7 +54,7 @@ theorem imo2011_q3 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) ≤ y * f x + f (f
   · suffices 0 ≤ f 0 from le_antisymm (h_f_nonpos 0) this
     have hno : f (-1) = 0 := h_fx_zero_of_neg (-1) neg_one_lt_zero
     have hp := hxt (-1) (-1)
-    rw [hno] at hp 
+    rw [hno] at hp
     linarith
 #align imo2011_q3 imo2011_q3
 

Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean

@@ -282,7 +282,7 @@ theorem NonUnitalStarSubalgebra.unitization_apply_coe (S : NonUnitalStarSubalgeb
 
 theorem NonUnitalStarSubalgebra.unitization_surjective (S : NonUnitalStarSubalgebra R A) :
     Function.Surjective S.unitization :=
-  have : StarSubalgebra.adjoin R S ≤ 
+  have : StarSubalgebra.adjoin R S ≤
       ((StarSubalgebra.adjoin R (S : Set A)).subtype.comp S.unitization).range :=
     StarSubalgebra.adjoin_le fun a ha ↦ ⟨(⟨a, ha⟩ : S), by simp⟩
   fun x ↦ match this x.property with | ⟨y, hy⟩ => ⟨y, Subtype.ext hy⟩

Mathlib/Algebra/Ring/Equiv.lean

@@ -42,18 +42,18 @@ Equiv, MulEquiv, AddEquiv, RingEquiv, MulAut, AddAut, RingAut
 variable {F α β R S S' : Type*}
 
 
-/-- makes a `NonUnitalRingHom` from the bijective inverse of a `NonUnitalRingHom` -/  
+/-- makes a `NonUnitalRingHom` from the bijective inverse of a `NonUnitalRingHom` -/
 @[simps] def NonUnitalRingHom.inverse
     [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S]
     (f : R →ₙ+* S) (g : S → R)
     (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : S →ₙ+* R :=
   { (f : R →+ S).inverse g h₁ h₂, (f : R →ₙ* S).inverse g h₁ h₂ with toFun := g }
 
-/-- makes a `RingHom` from the bijective inverse of a `RingHom` -/  
+/-- makes a `RingHom` from the bijective inverse of a `RingHom` -/
 @[simps] def RingHom.inverse [NonAssocSemiring R] [NonAssocSemiring S]
     (f : RingHom R S) (g : S → R)
     (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : S →+* R :=
-  { (f : OneHom R S).inverse g h₁, 
+  { (f : OneHom R S).inverse g h₁,
     (f : MulHom R S).inverse g h₁ h₂,
     (f : R →+ S).inverse g h₁ h₂ with toFun := g }
 

Mathlib/Analysis/Convex/Combination.lean

@@ -296,7 +296,7 @@ theorem convexHull_range_eq_exists_affineCombination (v : ι → E) : convexHull
 
 /--
 Convex hull of `s` is equal to the set of all centers of masses of `Finset`s `t`, `z '' t ⊆ s`.
-For universe reasons, you shouldn't use this lemma to prove that a given center of mass belongs 
+For universe reasons, you shouldn't use this lemma to prove that a given center of mass belongs
 to the convex hull. Use convexity of the convex hull instead.
 -/
 theorem convexHull_eq (s : Set E) : convexHull R s =

Mathlib/Analysis/Convex/Cone/Proper.lean

@@ -126,7 +126,7 @@ end SMul
 
 section PositiveCone
 
-variable (𝕜 E) 
+variable (𝕜 E)
 variable [OrderedSemiring 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E]
   [TopologicalSpace E] [OrderClosedTopology E]
 

Mathlib/Analysis/NormedSpace/HomeomorphBall.lean

@@ -117,7 +117,7 @@ def unitBallBall (c : P) (r : ℝ) (hr : 0 < r) : LocalHomeomorph E P :=
 /-- If `r > 0`, then `LocalHomeomorph.univBall c r` is a smooth local homeomorphism
 with `source = Set.univ` and `target = Metric.ball c r`.
 Otherwise, it is the translation by `c`.
-Thus in all cases, it sends `0` to `c`, see `LocalHomeomorph.univBall_apply_zero`. -/ 
+Thus in all cases, it sends `0` to `c`, see `LocalHomeomorph.univBall_apply_zero`. -/
 def univBall (c : P) (r : ℝ) : LocalHomeomorph E P :=
   if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) rfl
   else (IsometryEquiv.vaddConst c).toHomeomorph.toLocalHomeomorph

Mathlib/Analysis/ODE/Gronwall.lean

@@ -165,7 +165,7 @@ theorem dist_le_of_approx_trajectories_ODE_of_mem_set {v : ℝ → E → E} {s :
   apply norm_le_gronwallBound_of_norm_deriv_right_le (hf.sub hg) h_deriv ha
   intro t ht
   have := dist_triangle4_right (f' t) (g' t) (v t (f t)) (v t (g t))
-  rw [dist_eq_norm] at this 
+  rw [dist_eq_norm] at this
   refine' this.trans ((add_le_add (add_le_add (f_bound t ht) (g_bound t ht))
     (hv t (f t) (hfs t ht) (g t) (hgs t ht))).trans _)
   rw [dist_eq_norm, add_comm]
@@ -208,7 +208,7 @@ theorem dist_le_of_trajectories_ODE_of_mem_set {v : ℝ → E → E} {s : ℝ 
   intro t ht
   have :=
     dist_le_of_approx_trajectories_ODE_of_mem_set hv hf hf' f_bound hfs hg hg' g_bound hgs ha t ht
-  rwa [zero_add, gronwallBound_ε0] at this 
+  rwa [zero_add, gronwallBound_ε0] at this
 set_option linter.uppercaseLean3 false in
 #align dist_le_of_trajectories_ODE_of_mem_set dist_le_of_trajectories_ODE_of_mem_set
 
@@ -238,7 +238,7 @@ theorem ODE_solution_unique_of_mem_set {v : ℝ → E → E} {s : ℝ → Set E}
     (hg : ContinuousOn g (Icc a b)) (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t)
     (hgs : ∀ t ∈ Ico a b, g t ∈ s t) (ha : f a = g a) : ∀ t ∈ Icc a b, f t = g t := fun t ht ↦ by
   have := dist_le_of_trajectories_ODE_of_mem_set hv hf hf' hfs hg hg' hgs (dist_le_zero.2 ha) t ht
-  rwa [MulZeroClass.zero_mul, dist_le_zero] at this 
+  rwa [MulZeroClass.zero_mul, dist_le_zero] at this
 set_option linter.uppercaseLean3 false in
 #align ODE_solution_unique_of_mem_set ODE_solution_unique_of_mem_set
 

Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean

@@ -38,7 +38,7 @@ noncomputable def expLocalHomeomorph : LocalHomeomorph ℂ ℂ :=
         rintro ⟨x, y⟩ ⟨h₁ : -π < y, h₂ : y < π⟩
         refine' (not_or_of_imp fun hz => _).symm
         obtain rfl : y = 0 := by
-          rw [exp_im] at hz 
+          rw [exp_im] at hz
           simpa [(Real.exp_pos _).ne', Real.sin_eq_zero_iff_of_lt_of_lt h₁ h₂] using hz
         rw [mem_setOf_eq, ← ofReal_def, exp_ofReal_re]
         exact Real.exp_pos x

Mathlib/CategoryTheory/DifferentialObject.lean

@@ -95,8 +95,8 @@ theorem id_f (X : DifferentialObject S C) : (𝟙 X : X ⟶ X).f = 𝟙 X.obj :=
 #align category_theory.differential_object.id_f CategoryTheory.DifferentialObject.id_f
 
 @[simp]
-theorem comp_f {X Y Z : DifferentialObject S C} (f : X ⟶ Y) (g : Y ⟶ Z) : 
-    (f ≫ g).f = f.f ≫ g.f := 
+theorem comp_f {X Y Z : DifferentialObject S C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (f ≫ g).f = f.f ≫ g.f :=
   rfl
 #align category_theory.differential_object.comp_f CategoryTheory.DifferentialObject.comp_f
 

Mathlib/Data/Real/Sqrt.lean

@@ -467,7 +467,7 @@ theorem real_sqrt_le_nat_sqrt_succ {a : ℕ} : Real.sqrt ↑a ≤ Nat.sqrt a + 1
 /-- Although the instance `IsROrC.toStarOrderedRing` exists, it is locked behind the
 `ComplexOrder` scope because currently the order on `ℂ` is not enabled globally. But we
 want `StarOrderedRing ℝ` to be available globally, so we include this instance separately.
-In addition, providing this instance here makes it available earlier in the import 
+In addition, providing this instance here makes it available earlier in the import
 hierarchy; otherwise in order to access it we would need to import `Data.IsROrC.Basic` -/
 instance : StarOrderedRing ℝ :=
   StarOrderedRing.ofNonnegIff' add_le_add_left fun r => by

Mathlib/Geometry/Euclidean/Inversion/Calculus.lean

@@ -59,7 +59,7 @@ protected nonrec theorem ContDiff.inversion (hc : ContDiff ℝ n c) (hR : ContDi
 protected theorem DifferentiableWithinAt.inversion (hc : DifferentiableWithinAt ℝ c s a)
     (hR : DifferentiableWithinAt ℝ R s a) (hx : DifferentiableWithinAt ℝ x s a) (hne : x a ≠ c a) :
     DifferentiableWithinAt ℝ (fun a ↦ inversion (c a) (R a) (x a)) s a :=
-  -- TODO: Use `.div` #5870 
+  -- TODO: Use `.div` #5870
   (((hR.mul <| (hx.dist ℝ hc hne).inv (dist_ne_zero.2 hne)).pow _).smul (hx.sub hc)).add hc
 
 protected theorem DifferentiableOn.inversion (hc : DifferentiableOn ℝ c s)

Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

@@ -340,8 +340,8 @@ theorem symm_continuousWithinAt_comp_right_iff {X} [TopologicalSpace X] {f : H 
   refine' ⟨fun h => _, fun h => _⟩
   · have := h.comp I.continuousWithinAt (mapsTo_preimage _ _)
     simp_rw [preimage_inter, preimage_preimage, I.left_inv, preimage_id', preimage_range,
-      inter_univ] at this 
-    rwa [Function.comp.assoc, I.symm_comp_self] at this 
+      inter_univ] at this
+    rwa [Function.comp.assoc, I.symm_comp_self] at this
   · rw [← I.left_inv x] at h; exact h.comp I.continuousWithinAt_symm (inter_subset_left _ _)
 #align model_with_corners.symm_continuous_within_at_comp_right_iff ModelWithCorners.symm_continuousWithinAt_comp_right_iff
 
@@ -555,7 +555,7 @@ def contDiffGroupoid : StructureGroupoid H :=
           rw [preimage_inter, inter_assoc, inter_assoc]
           congr 1
           rw [inter_comm]
-        rw [this] at hv 
+        rw [this] at hv
         exact ⟨I.symm ⁻¹' v, v_open.preimage I.continuous_symm, by simpa, hv⟩
       congr := fun {f g u} _ fg hf => by
         apply hf.congr
@@ -623,14 +623,14 @@ theorem contDiffGroupoid_prod {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCor
     (he' : e' ∈ contDiffGroupoid ⊤ I') : e.prod e' ∈ contDiffGroupoid ⊤ (I.prod I') := by
   cases' he with he he_symm
   cases' he' with he' he'_symm
-  simp only at he he_symm he' he'_symm 
+  simp only at he he_symm he' he'_symm
   constructor <;> simp only [LocalEquiv.prod_source, LocalHomeomorph.prod_toLocalEquiv]
   · have h3 := ContDiffOn.prod_map he he'
-    rw [← I.image_eq, ← I'.image_eq, Set.prod_image_image_eq] at h3 
+    rw [← I.image_eq, ← I'.image_eq, Set.prod_image_image_eq] at h3
     rw [← (I.prod I').image_eq]
     exact h3
   · have h3 := ContDiffOn.prod_map he_symm he'_symm
-    rw [← I.image_eq, ← I'.image_eq, Set.prod_image_image_eq] at h3 
+    rw [← I.image_eq, ← I'.image_eq, Set.prod_image_image_eq] at h3
     rw [← (I.prod I').image_eq]
     exact h3
 #align cont_diff_groupoid_prod contDiffGroupoid_prod
@@ -970,7 +970,7 @@ theorem continuousOn_writtenInExtend_iff {f' : LocalHomeomorph M' H'} {g : M →
 in the source is a neighborhood of the preimage, within a set. -/
 theorem extend_preimage_mem_nhdsWithin {x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝[s] x) :
     (f.extend I).symm ⁻¹' t ∈ 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I x := by
-  rwa [← map_extend_symm_nhdsWithin f I h, mem_map] at ht 
+  rwa [← map_extend_symm_nhdsWithin f I h, mem_map] at ht
 #align local_homeomorph.extend_preimage_mem_nhds_within LocalHomeomorph.extend_preimage_mem_nhdsWithin
 
 theorem extend_preimage_mem_nhds {x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝 x) :
@@ -1268,7 +1268,7 @@ in the source is a neighborhood of the preimage, within a set. -/
 theorem extChartAt_preimage_mem_nhdsWithin' {x' : M} (h : x' ∈ (extChartAt I x).source)
     (ht : t ∈ 𝓝[s] x') :
     (extChartAt I x).symm ⁻¹' t ∈ 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x' := by
-  rwa [← map_extChartAt_symm_nhdsWithin' I x h, mem_map] at ht 
+  rwa [← map_extChartAt_symm_nhdsWithin' I x h, mem_map] at ht
 #align ext_chart_at_preimage_mem_nhds_within' extChartAt_preimage_mem_nhdsWithin'
 
 /-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of the

Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean

@@ -119,7 +119,7 @@ theorem SmoothFiberwiseLinear.locality_aux₁ (e : LocalHomeomorph (B × F) (B 
             (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ((φ x).symm : F →L[𝕜] F)) u),
             (e.restr (u ×ˢ univ)).EqOnSource
               (FiberwiseLinear.localHomeomorph φ hu hφ.continuousOn h2φ.continuousOn) := by
-  rw [SetCoe.forall'] at h 
+  rw [SetCoe.forall'] at h
   choose s hs hsp φ u hu hφ h2φ heφ using h
   have hesu : ∀ p : e.source, e.source ∩ s p = u p ×ˢ univ := by
     intro p
@@ -132,7 +132,7 @@ theorem SmoothFiberwiseLinear.locality_aux₁ (e : LocalHomeomorph (B × F) (B 
   have heu : ∀ p : e.source, ∀ q : B × F, q.fst ∈ u p → q ∈ e.source := by
     intro p q hq
     have : q ∈ u p ×ˢ (univ : Set F) := ⟨hq, trivial⟩
-    rw [← hesu p] at this 
+    rw [← hesu p] at this
     exact this.1
   have he : e.source = (Prod.fst '' e.source) ×ˢ (univ : Set F) := by
     apply HasSubset.Subset.antisymm
@@ -171,7 +171,7 @@ theorem SmoothFiberwiseLinear.locality_aux₂ (e : LocalHomeomorph (B × F) (B 
       SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ((Φ x).symm : F →L[𝕜] F)) U),
       e.EqOnSource (FiberwiseLinear.localHomeomorph Φ hU₀ hΦ.continuousOn h2Φ.continuousOn) := by
   classical
-  rw [SetCoe.forall'] at h 
+  rw [SetCoe.forall'] at h
   choose! φ u hu hUu hux hφ h2φ heφ using h
   have heuφ : ∀ x : U, EqOn e (fun q => (q.1, φ x q.1 q.2)) (u x ×ˢ univ) := fun x p hp ↦ by
     refine' (heφ x).2 _
@@ -214,7 +214,7 @@ theorem SmoothFiberwiseLinear.locality_aux₂ (e : LocalHomeomorph (B × F) (B 
     intro y hy
     rw [hΦφ ⟨x, hx⟩ y hy]
   refine' ⟨Φ, U, hU', hΦ, h2Φ, hU, fun p hp => _⟩
-  rw [hU] at hp 
+  rw [hU] at hp
   rw [heuφ ⟨p.fst, hp.1⟩ ⟨hux _, hp.2⟩]
   -- porting note: replaced `congrm` with manual `congr_arg`
   refine congr_arg (Prod.mk _) ?_

Mathlib/Geometry/Manifold/WhitneyEmbedding.lean

@@ -67,10 +67,10 @@ theorem embeddingPiTangent_coe :
 
 theorem embeddingPiTangent_injOn : InjOn f.embeddingPiTangent s := by
   intro x hx y _ h
-  simp only [embeddingPiTangent_coe, funext_iff] at h 
+  simp only [embeddingPiTangent_coe, funext_iff] at h
   obtain ⟨h₁, h₂⟩ := Prod.mk.inj_iff.1 (h (f.ind x hx))
-  rw [f.apply_ind x hx] at h₂ 
-  rw [← h₂, f.apply_ind x hx, one_smul, one_smul] at h₁ 
+  rw [f.apply_ind x hx] at h₂
+  rw [← h₂, f.apply_ind x hx, one_smul, one_smul] at h₁
   have := f.mem_extChartAt_source_of_eq_one h₂.symm
   exact (extChartAt I (f.c _)).injOn (f.mem_extChartAt_ind_source x hx) this h₁
 #align smooth_bump_covering.embedding_pi_tangent_inj_on SmoothBumpCovering.embeddingPiTangent_injOn

Mathlib/MeasureTheory/Integral/TorusIntegral.lean

@@ -253,7 +253,7 @@ theorem torusIntegral_succAbove {f : ℂⁿ⁺¹ → E} {c : ℂⁿ⁺¹} {R : 
     simp only [funext_iff, i.forall_iff_succAbove, circleMap, Fin.insertNth_apply_same,
       eq_self_iff_true, Fin.insertNth_apply_succAbove, imp_true_iff, and_self_iff]
   · have := hf.function_integrable
-    rwa [← hem.integrableOn_comp_preimage e.measurableEmbedding, heπ] at this 
+    rwa [← hem.integrableOn_comp_preimage e.measurableEmbedding, heπ] at this
 #align torus_integral_succ_above torusIntegral_succAbove
 
 /-- Recurrent formula for `torusIntegral`, see also `torusIntegral_succAbove`. -/

Mathlib/NumberTheory/LegendreSymbol/Basic.lean

@@ -178,7 +178,7 @@ theorem sq_one {a : ℤ} (ha : (a : ZMod p) ≠ 0) : legendreSym p a ^ 2 = 1 :=
 
 /-- The Legendre symbol of `a^2` at `p` is 1 if `p ∤ a`. -/
 theorem sq_one' {a : ℤ} (ha : (a : ZMod p) ≠ 0) : legendreSym p (a ^ 2) = 1 := by
-  dsimp only [legendreSym] 
+  dsimp only [legendreSym]
   rw [Int.cast_pow]
   exact quadraticChar_sq_one' ha
 #align legendre_sym.sq_one' legendreSym.sq_one'

Mathlib/NumberTheory/Liouville/Measure.lean

@@ -40,7 +40,7 @@ theorem setOf_liouvilleWith_subset_aux :
           |x - (a : ℤ) / b| < 1 / (b : ℝ) ^ (2 + 1 / n : ℝ) } := by
   rintro x ⟨p, hp, hxp⟩
   rcases exists_nat_one_div_lt (sub_pos.2 hp) with ⟨n, hn⟩
-  rw [lt_sub_iff_add_lt'] at hn 
+  rw [lt_sub_iff_add_lt'] at hn
   suffices ∀ y : ℝ, LiouvilleWith p y → y ∈ Ico (0 : ℝ) 1 → ∃ᶠ b : ℕ in atTop,
       ∃ a ∈ Finset.Icc (0 : ℤ) b, |y - a / b| < 1 / (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ) by
     simp only [mem_iUnion, mem_preimage]
@@ -51,7 +51,7 @@ theorem setOf_liouvilleWith_subset_aux :
   clear hxp x; intro x hxp hx01
   refine' ((hxp.frequently_lt_rpow_neg hn).and_eventually (eventually_ge_atTop 1)).mono _
   rintro b ⟨⟨a, -, hlt⟩, hb⟩
-  rw [rpow_neg b.cast_nonneg, ← one_div, ← Nat.cast_succ] at hlt 
+  rw [rpow_neg b.cast_nonneg, ← one_div, ← Nat.cast_succ] at hlt
   refine' ⟨a, _, hlt⟩
   replace hb : (1 : ℝ) ≤ b; exact Nat.one_le_cast.2 hb
   have hb0 : (0 : ℝ) < b := zero_lt_one.trans_le hb
@@ -63,7 +63,7 @@ theorem setOf_liouvilleWith_subset_aux :
         rpow_le_rpow_of_exponent_le hb (one_le_two.trans ?_)
     simpa using n.cast_add_one_pos.le
   rw [sub_div' _ _ _ hb0.ne', abs_div, abs_of_pos hb0, div_lt_div_right hb0, abs_sub_lt_iff,
-    sub_lt_iff_lt_add, sub_lt_iff_lt_add, ← sub_lt_iff_lt_add'] at hlt 
+    sub_lt_iff_lt_add, sub_lt_iff_lt_add, ← sub_lt_iff_lt_add'] at hlt
   rw [Finset.mem_Icc, ← Int.lt_add_one_iff, ← Int.lt_add_one_iff, ← neg_lt_iff_pos_add, add_comm, ←
     @Int.cast_lt ℝ, ← @Int.cast_lt ℝ]
   push_cast

Mathlib/Order/Filter/CountableSeparatingOn.lean

@@ -135,7 +135,7 @@ with countable intersections property. Let `p : Set α → Prop` be a property s
 countable family of sets satisfying `p` and separating points of `α`. Then `l` is supported on
 a subsingleton: there exists a subsingleton `t` such that `t ∈ l`.
 
-With extra `Nonempty`/`Set.Nonempty` assumptions one can ensure that `t` is a singleton `{x}`. 
+With extra `Nonempty`/`Set.Nonempty` assumptions one can ensure that `t` is a singleton `{x}`.
 
 If `s ∈ l`, then it suffices to assume that the countable family separates only points of `s`.
 -/

Mathlib/Order/Irreducible.lean

@@ -113,7 +113,7 @@ theorem SupIrred.finset_sup_eq (ha : SupIrred a) (h : s.sup f = a) : ∃ i ∈ s
   induction' s using Finset.induction with i s _ ih
   · simpa [ha.ne_bot] using h.symm
   simp only [exists_prop, exists_mem_insert] at ih ⊢
-  rw [sup_insert] at h 
+  rw [sup_insert] at h
   exact (ha.2 h).imp_right ih
 #align sup_irred.finset_sup_eq SupIrred.finset_sup_eq
 
@@ -136,7 +136,7 @@ theorem exists_supIrred_decomposition (a : α) :
   rintro a ih
   by_cases ha : SupIrred a
   · exact ⟨{a}, by simp [ha]⟩
-  rw [not_supIrred] at ha 
+  rw [not_supIrred] at ha
   obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha
   · exact ⟨∅, by simp [ha.eq_bot]⟩
   obtain ⟨s, rfl, hs⟩ := ih _ hb

Mathlib/Tactic/Nontriviality/Core.lean

@@ -61,7 +61,7 @@ The `nontriviality` tactic will first look for strict inequalities amongst the h
 and use these to derive the `Nontrivial` instance directly.
 
 Otherwise, it will perform a case split on `Subsingleton α ∨ Nontrivial α`, and attempt to discharge
-the `Subsingleton` goal using `simp [h₁, h₂, ..., hₙ, nontriviality]`, where `[h₁, h₂, ..., hₙ]` is 
+the `Subsingleton` goal using `simp [h₁, h₂, ..., hₙ, nontriviality]`, where `[h₁, h₂, ..., hₙ]` is
 a list of additional `simp` lemmas that can be passed to `nontriviality` using the syntax
 `nontriviality α using h₁, h₂, ..., hₙ`.
 

Mathlib/Topology/Sheaves/Functors.lean

@@ -51,7 +51,7 @@ set_option linter.uppercaseLean3 false in
 #align Top.presheaf.sheaf_condition_pairwise_intersections.map_diagram TopCat.Presheaf.SheafConditionPairwiseIntersections.map_diagram
 
 theorem mapCocone :
-    HEq ((Opens.map f).mapCocone (Pairwise.cocone U)) 
+    HEq ((Opens.map f).mapCocone (Pairwise.cocone U))
       (Pairwise.cocone ((Opens.map f).obj ∘ U)) := by
   unfold Functor.mapCocone Cocones.functoriality; dsimp; congr
   iterate 2 rw [map_diagram]; rw [Opens.map_iSup]

scripts/lint-style.py

@@ -50,6 +50,7 @@
 ERR_DOT = 12 # isolated or low focusing dot
 ERR_SEM = 13 # the substring " ;"
 ERR_WIN = 14 # Windows line endings "\r\n"
+ERR_TWS = 15 # Trailing whitespace
 
 exceptions = []
 
@@ -148,11 +149,14 @@ def set_option_check(lines, path):
                 errors += [(ERR_OPT, line_nr, path)]
     return errors
 
-def windows_line_endings_check(lines, path):
+def line_endings_check(lines, path):
     errors = []
     for line_nr, line in enumerate(lines, 1):
         if "\r\n" in line:
             errors += [(ERR_WIN, line_nr, path)]
+        line = line.rstrip("\r\n")
+        if line.endswith(" "):
+            errors += [(ERR_TWS, line_nr, path)]
     return errors
 
 def long_lines_check(lines, path):
@@ -305,11 +309,13 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_SEM", "Line contains a space before a semicolon")
         if errno == ERR_WIN:
             output_message(path, line_nr, "ERR_WIN", "Windows line endings (\\r\\n) detected")
+        if errno == ERR_TWS:
+            output_message(path, line_nr, "ERR_TWS", "Trailing whitespece detected on line")
 
 def lint(path):
     with path.open(encoding="utf-8", newline="") as f:
         lines = f.readlines()
-        errs = windows_line_endings_check(lines, path)
+        errs = line_endings_check(lines, path)
         format_errors(errs)
         lines = [line.rstrip() + "\n" for line in lines]