chore: replace λ by fun (#11301)

Per the style guidelines, `λ` is disallowed in mathlib.
This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon.

Notes
- In lines I was modifying anyway, I also converted `=>` to `↦`.
- Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`.
- Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced.

<!-- The text above the `

Mathlib/Algebra/BigOperators/Order.lean

@@ -754,9 +754,9 @@ theorem prod_mono' : Monotone fun f : ι → M ↦ ∏ i, f i := fun _ _ hfg ↦
 #align fintype.sum_mono Fintype.sum_mono
 
 @[to_additive sum_nonneg]
-lemma one_le_prod (hf : 1 ≤ f) : 1 ≤ ∏ i, f i := Finset.one_le_prod' λ _ _ ↦ hf _
+lemma one_le_prod (hf : 1 ≤ f) : 1 ≤ ∏ i, f i := Finset.one_le_prod' fun _ _ ↦ hf _
 
-@[to_additive] lemma prod_le_one (hf : f ≤ 1) : ∏ i, f i ≤ 1 := Finset.prod_le_one' λ _ _ ↦ hf _
+@[to_additive] lemma prod_le_one (hf : f ≤ 1) : ∏ i, f i ≤ 1 := Finset.prod_le_one' fun _ _ ↦ hf _
 
 @[to_additive]
 lemma prod_eq_one_iff_of_one_le (hf : 1 ≤ f) : ∏ i, f i = 1 ↔ f = 1 :=
@@ -781,11 +781,11 @@ theorem prod_strictMono' : StrictMono fun f : ι → M ↦ ∏ x, f x :=
 
 @[to_additive sum_pos]
 lemma one_lt_prod (hf : 1 < f) : 1 < ∏ i, f i :=
-  Finset.one_lt_prod' (λ _ _ ↦ hf.le _) <| by simpa using (Pi.lt_def.1 hf).2
+  Finset.one_lt_prod' (fun _ _ ↦ hf.le _) <| by simpa using (Pi.lt_def.1 hf).2
 
 @[to_additive]
 lemma prod_lt_one (hf : f < 1) : ∏ i, f i < 1 :=
-  Finset.prod_lt_one' (λ _ _ ↦ hf.le _) <| by simpa using (Pi.lt_def.1 hf).2
+  Finset.prod_lt_one' (fun _ _ ↦ hf.le _) <| by simpa using (Pi.lt_def.1 hf).2
 
 @[to_additive sum_pos_iff_of_nonneg]
 lemma one_lt_prod_iff_of_one_le (hf : 1 ≤ f) : 1 < ∏ i, f i ↔ 1 < f := by

Mathlib/Algebra/Field/ULift.lean

@@ -21,7 +21,7 @@ variable {α : Type u} {x y : ULift.{v} α}
 
 namespace ULift
 
-instance [RatCast α] : RatCast (ULift α) := ⟨λ a ↦ up a⟩
+instance [RatCast α] : RatCast (ULift α) := ⟨(up ·)⟩
 
 @[simp, norm_cast]
 theorem up_ratCast [RatCast α] (q : ℚ) : up (q : α) = q :=

Mathlib/Algebra/GCDMonoid/Multiset.lean

@@ -235,7 +235,7 @@ theorem extract_gcd' (s t : Multiset α) (hs : ∃ x, x ∈ s ∧ x ≠ (0 : α)
 converted to `Multiset.replicate` format yet, so I made some ad hoc ones in `Data.Multiset.Basic`
 using the originals. -/
 /- Porting note: The old proof used a strange form
-`have := _, refine ⟨s.pmap @f (λ _, id), this, extract_gcd' s _ h this⟩,`
+`have := _, refine ⟨s.pmap @f (fun _ ↦ id), this, extract_gcd' s _ h this⟩,`
 so I rearranged the proof slightly. -/
 theorem extract_gcd (s : Multiset α) (hs : s ≠ 0) :
     ∃ t : Multiset α, s = t.map (s.gcd * ·) ∧ t.gcd = 1 := by

Mathlib/Algebra/Group/Opposite.lean

@@ -381,8 +381,8 @@ instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne 
 
 instance addCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne αᵃᵒᵖ :=
   { AddOpposite.addCommMonoidWithOne α, AddOpposite.addCommGroup α, AddOpposite.intCast α with
-    intCast_ofNat := λ _ ↦ congr_arg op <| Int.cast_ofNat _
-    intCast_negSucc := λ _ ↦ congr_arg op <| Int.cast_negSucc _ }
+    intCast_ofNat := fun _ ↦ congr_arg op <| Int.cast_ofNat _
+    intCast_negSucc := fun _ ↦ congr_arg op <| Int.cast_negSucc _ }
 
 variable {α}
 

Mathlib/Algebra/Group/ULift.lean

@@ -143,9 +143,9 @@ instance commMonoid [CommMonoid α] : CommMonoid (ULift α) :=
 #align ulift.comm_monoid ULift.commMonoid
 #align ulift.add_comm_monoid ULift.addCommMonoid
 
-instance natCast [NatCast α] : NatCast (ULift α) := ⟨λ a ↦ up a⟩
+instance natCast [NatCast α] : NatCast (ULift α) := ⟨(up ·)⟩
 #align ulift.has_nat_cast ULift.natCast
-instance intCast [IntCast α] : IntCast (ULift α) := ⟨λ a ↦ up a⟩
+instance intCast [IntCast α] : IntCast (ULift α) := ⟨(up ·)⟩
 #align ulift.has_int_cast ULift.intCast
 
 @[simp, norm_cast]
@@ -182,7 +182,7 @@ theorem down_intCast [IntCast α] (n : ℤ) : down (n : ULift α) = n :=
 
 instance addMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne (ULift α) :=
   { ULift.one, ULift.addMonoid with
-      natCast := fun n => ⟨n⟩
+      natCast := (⟨·⟩)
       natCast_zero := congr_arg ULift.up Nat.cast_zero,
       natCast_succ := fun _ => congr_arg ULift.up (Nat.cast_succ _) }
 #align ulift.add_monoid_with_one ULift.addMonoidWithOne
@@ -222,7 +222,7 @@ instance commGroup [CommGroup α] : CommGroup (ULift α) :=
 
 instance addGroupWithOne [AddGroupWithOne α] : AddGroupWithOne (ULift α) :=
   { ULift.addMonoidWithOne, ULift.addGroup with
-      intCast := fun n => ⟨n⟩,
+      intCast := (⟨·⟩),
       intCast_ofNat := fun _ => congr_arg ULift.up (Int.cast_ofNat _),
       intCast_negSucc := fun _ => congr_arg ULift.up (Int.cast_negSucc _) }
 #align ulift.add_group_with_one ULift.addGroupWithOne

Mathlib/Algebra/Homology/HomologicalComplexLimits.lean

@@ -181,7 +181,7 @@ def preservesLimitsOfShapeOfEval {D : Type*} [Category D]
     (G : D ⥤ HomologicalComplex C c)
     (_ : ∀ (i : ι), PreservesLimitsOfShape J (G ⋙ eval C c i)) :
     PreservesLimitsOfShape J G :=
-  ⟨fun {_} => ⟨fun hs =>  isLimitOfEval _ _
+  ⟨fun {_} => ⟨fun hs ↦ isLimitOfEval _ _
     (fun i => isLimitOfPreserves (G ⋙ eval C c i) hs)⟩⟩
 
 /-- A functor `D ⥤ HomologicalComplex C c` preserves colimits of shape `J`
@@ -190,7 +190,7 @@ def preservesColimitsOfShapeOfEval {D : Type*} [Category D]
     (G : D ⥤ HomologicalComplex C c)
     (_ : ∀ (i : ι), PreservesColimitsOfShape J (G ⋙ eval C c i)) :
     PreservesColimitsOfShape J G :=
-  ⟨fun {_} => ⟨fun hs =>  isColimitOfEval _ _
+  ⟨fun {_} => ⟨fun hs ↦ isColimitOfEval _ _
     (fun i => isColimitOfPreserves (G ⋙ eval C c i) hs)⟩⟩
 
 end HomologicalComplex

Mathlib/Algebra/Module/Injective.lean

@@ -445,7 +445,7 @@ protected theorem extension_property (h : Module.Baer R Q)
     { toFun := ((extensionOfMax f g).toLinearPMap
         ⟨·, (extensionOfMax_to_submodule_eq_top f g h).symm ▸ ⟨⟩⟩)
       map_add' := fun x y ↦ by rw [← LinearPMap.map_add]; congr
-      map_smul' := fun r x ↦  by rw [← LinearPMap.map_smul]; dsimp } <|
+      map_smul' := fun r x ↦ by rw [← LinearPMap.map_smul]; dsimp } <|
     LinearMap.ext fun x ↦ ((extensionOfMax f g).is_extension x).symm
 
 theorem extension_property_addMonoidHom (h : Module.Baer ℤ Q)

Mathlib/Algebra/Module/Zlattice.lean

@@ -481,7 +481,7 @@ theorem Zlattice.rank : finrank ℤ L = finrank K E := by
     have h_mapsto : Set.MapsTo (fun n : ℤ => Zspan.fract e (n • v)) Set.univ
         (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ (L : Set E)) := by
       rw [Set.mapsTo_inter, Set.mapsTo_univ_iff, Set.mapsTo_univ_iff]
-      refine ⟨fun _ =>  mem_closedBall_zero_iff.mpr (Zspan.norm_fract_le e _), fun _ => ?_⟩
+      refine ⟨fun _ ↦ mem_closedBall_zero_iff.mpr (Zspan.norm_fract_le e _), fun _ => ?_⟩
       · change _ ∈ AddSubgroup.toIntSubmodule L
         rw [← h_spanL]
         refine sub_mem ?_ ?_

Mathlib/Algebra/Order/UpperLower.lean

@@ -161,7 +161,7 @@ theorem Ici_one : Ici (1 : α) = 1 :=
 
 @[to_additive]
 instance : MulAction α (UpperSet α) :=
-  SetLike.coe_injective.mulAction _ (λ _ _ => rfl)
+  SetLike.coe_injective.mulAction _ (fun _ _ => rfl)
 
 @[to_additive]
 instance commSemigroup : CommSemigroup (UpperSet α) :=
@@ -223,7 +223,7 @@ theorem Iic_one : Iic (1 : α) = 1 :=
 
 @[to_additive]
 instance : MulAction α (LowerSet α) :=
-  SetLike.coe_injective.mulAction _ (λ _ _ => rfl)
+  SetLike.coe_injective.mulAction _ (fun _ _ => rfl)
 
 @[to_additive]
 instance commSemigroup : CommSemigroup (LowerSet α) :=

Mathlib/Algebra/Quaternion.lean

@@ -393,7 +393,7 @@ theorem coe_smul [SMulZeroClass S R] (s : S) (r : R) :
 
 instance : AddCommGroup ℍ[R,c₁,c₂] :=
   (equivProd c₁ c₂).injective.addCommGroup _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
-    (λ _ _ ↦ rfl) (λ _ _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
 
 instance : AddCommGroupWithOne ℍ[R,c₁,c₂] where
   natCast n := ((n : R) : ℍ[R,c₁,c₂])

Mathlib/Algebra/SMulWithZero.lean

@@ -161,7 +161,7 @@ instance MonoidWithZero.toOppositeMulActionWithZero : MulActionWithZero Rᵐᵒ
 
 protected lemma MulActionWithZero.subsingleton
     [MulActionWithZero R M] [Subsingleton R] : Subsingleton M :=
-  ⟨λ x y => by
+  ⟨fun x y => by
     rw [← one_smul R x, ← one_smul R y, Subsingleton.elim (1 : R) 0, zero_smul, zero_smul]⟩
 #align mul_action_with_zero.subsingleton MulActionWithZero.subsingleton
 

Mathlib/Analysis/Analytic/Constructions.lean

@@ -61,7 +61,7 @@ lemma FormalMultilinearSeries.radius_prod_eq_min
     rw [lt_min_iff] at hr
     have := ((p.isLittleO_one_of_lt_radius hr.1).add
       (q.isLittleO_one_of_lt_radius hr.2)).isBigO
-    refine (p.prod q).le_radius_of_isBigO ((isBigO_of_le _ λ n ↦ ?_).trans this)
+    refine (p.prod q).le_radius_of_isBigO ((isBigO_of_le _ fun n ↦ ?_).trans this)
     rw [norm_mul, norm_norm, ← add_mul, norm_mul]
     refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
     rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]

Mathlib/Analysis/Convex/Combination.lean

@@ -242,7 +242,7 @@ theorem Finset.centerMass_mem_convexHull (t : Finset ι) {w : ι → R} (hw₀ :
 lemma Finset.centerMass_mem_convexHull_of_nonpos (t : Finset ι) (hw₀ : ∀ i ∈ t, w i ≤ 0)
     (hws : ∑ i in t, w i < 0) (hz : ∀ i ∈ t, z i ∈ s) : t.centerMass w z ∈ convexHull R s := by
   rw [← centerMass_neg_left]
-  exact Finset.centerMass_mem_convexHull _ (λ _i hi ↦ neg_nonneg.2 <| hw₀ _ hi) (by simpa) hz
+  exact Finset.centerMass_mem_convexHull _ (fun _i hi ↦ neg_nonneg.2 <| hw₀ _ hi) (by simpa) hz
 
 /-- A refinement of `Finset.centerMass_mem_convexHull` when the indexed family is a `Finset` of
 the space. -/

Mathlib/Analysis/Convex/Radon.lean

@@ -37,7 +37,7 @@ theorem radon_partition (h : ¬ AffineIndependent 𝕜 f) :
   have hI : 0 < ∑ i in I, w i := by
     rcases exists_pos_of_sum_zero_of_exists_nonzero _ h_wsum ⟨nonzero_w_index, h1, h2⟩
       with ⟨pos_w_index, h1', h2'⟩
-    exact sum_pos' (λ _i hi ↦ (mem_filter.1 hi).2)
+    exact sum_pos' (fun _i hi ↦ (mem_filter.1 hi).2)
       ⟨pos_w_index, by simp only [I, mem_filter, h1', h2'.le, and_self, h2']⟩
   have hp : centerMass J w f = p := Finset.centerMass_of_sum_add_sum_eq_zero hJI <| by
     simpa only [← h_vsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) _

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

@@ -400,7 +400,7 @@ open Asymptotics in
 /-- Useful to use together with `Continuous.comp₂`. -/
 theorem IsBoundedBilinearMap.continuous (h : IsBoundedBilinearMap 𝕜 f) : Continuous f := by
   refine continuous_iff_continuousAt.2 fun x ↦ tendsto_sub_nhds_zero_iff.1 ?_
-  suffices Tendsto (λ y : E × F ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0)) by
+  suffices Tendsto (fun y : E × F ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0)) by
     simpa only [h.map_sub_left, h.map_sub_right, sub_add_sub_cancel, zero_add] using this
   apply Tendsto.add
   · rw [← isLittleO_one_iff ℝ, ← one_mul 1]

Mathlib/Analysis/NormedSpace/LpEquiv.lean

@@ -15,9 +15,9 @@ import Mathlib.Topology.ContinuousFunction.Bounded
 In this file we collect a variety of equivalences among various $L^p$ spaces.  In particular,
 when `α` is a `Fintype`, given `E : α → Type u` and `p : ℝ≥0∞`, there is a natural linear isometric
 equivalence `lpPiLpₗᵢₓ : lp E p ≃ₗᵢ PiLp p E`. In addition, when `α` is a discrete topological
-space, the bounded continuous functions `α →ᵇ β` correspond exactly to `lp (λ _, β) ∞`. Here there
-can be more structure, including ring and algebra structures, and we implement these equivalences
-accordingly as well.
+space, the bounded continuous functions `α →ᵇ β` correspond exactly to `lp (fun _ ↦ β) ∞`.
+Here there can be more structure, including ring and algebra structures,
+and we implement these equivalences accordingly as well.
 
 We keep this as a separate file so that the various $L^p$ space files don't import the others.
 

Mathlib/Analysis/SpecialFunctions/Exp.lean

@@ -68,7 +68,7 @@ theorem locally_lipschitz_exp {r : ℝ} (hr_nonneg : 0 ≤ r) (hr_le : r ≤ 1)
 theorem continuous_exp : Continuous exp :=
   continuous_iff_continuousAt.mpr fun x =>
     continuousAt_of_locally_lipschitz zero_lt_one (2 * ‖exp x‖)
-      (λ y => by
+      (fun y ↦ by
         convert locally_lipschitz_exp zero_le_one le_rfl x y using 2
         congr
         ring)

Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

@@ -57,7 +57,7 @@ lemma tendsto_rpow_atTop_of_base_lt_one (b : ℝ) (hb₀ : -1 < b) (hb₁ : b <
     Tendsto (rpow b) atTop (𝓝 (0:ℝ)) := by
   show Tendsto (fun z => b^z) atTop (𝓝 0)
   rcases lt_trichotomy b 0 with hb|rfl|hb
-  case inl =>   -- b < 0
+  case inl => -- b < 0
     simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]
     rw [← isLittleO_const_iff (c := (1:ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]
     refine IsLittleO.mul_isBigO ?exp ?cos
@@ -69,12 +69,12 @@ lemma tendsto_rpow_atTop_of_base_lt_one (b : ℝ) (hb₀ : -1 < b) (hb₁ : b <
     case cos =>
       rw [isBigO_iff]
       exact ⟨1, eventually_of_forall fun x => by simp [Real.abs_cos_le_one]⟩
-  case inr.inl =>  -- b = 0
+  case inr.inl => -- b = 0
     refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)
     rw [tendsto_pure]
     filter_upwards [eventually_ne_atTop 0] with _ hx
     simp [hx]
-  case inr.inr =>   -- b > 0
+  case inr.inr => -- b > 0
     simp_rw [Real.rpow_def_of_pos hb]
     refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
     exact (log_neg_iff hb).mpr hb₁

Mathlib/Analysis/SpecificLimits/Basic.lean

@@ -693,7 +693,7 @@ theorem tendsto_nat_ceil_div_atTop : Tendsto (fun x ↦ (⌈x⌉₊ : R) / x) at
   simpa using tendsto_nat_ceil_mul_div_atTop (zero_le_one' R)
 #align tendsto_nat_ceil_div_at_top tendsto_nat_ceil_div_atTop
 
-lemma Nat.tendsto_div_const_atTop {n : ℕ} (hn : n ≠ 0) : Tendsto (λ x ↦ x / n) atTop atTop := by
+lemma Nat.tendsto_div_const_atTop {n : ℕ} (hn : n ≠ 0) : Tendsto (· / n) atTop atTop := by
   rw [Tendsto, map_div_atTop_eq_nat n hn.bot_lt]
 
 end

Mathlib/Combinatorics/Additive/Energy.lean

@@ -17,8 +17,8 @@ additive combinatorics.
 ## TODO
 
 It's possibly interesting to have
-`(s ×ˢ s) ×ˢ t ×ˢ t).filter (λ x : (α × α) × α × α, x.1.1 * x.2.1 = x.1.2 * x.2.2)` (whose `card`
-is `multiplicativeEnergy s t`) as a standalone definition.
+`(s ×ˢ s) ×ˢ t ×ˢ t).filter (fun x : (α × α) × α × α ↦ x.1.1 * x.2.1 = x.1.2 * x.2.2)`
+(whose `card` is `multiplicativeEnergy s t`) as a standalone definition.
 -/
 
 

Mathlib/Combinatorics/Quiver/Cast.lean

@@ -32,7 +32,7 @@ namespace Quiver
 
 /-- Change the endpoints of an arrow using equalities. -/
 def Hom.cast {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) : u' ⟶ v' :=
-  Eq.ndrec (motive := λ x => x ⟶ v') (Eq.ndrec e hv) hu
+  Eq.ndrec (motive := (· ⟶ v')) (Eq.ndrec e hv) hu
 #align quiver.hom.cast Quiver.Hom.cast
 
 theorem Hom.cast_eq_cast {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) :
@@ -81,7 +81,7 @@ open Path
 
 /-- Change the endpoints of a path using equalities. -/
 def Path.cast {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Path u v) : Path u' v' :=
-  Eq.ndrec (motive := λ x => Path x v') (Eq.ndrec p hv) hu
+  Eq.ndrec (motive := (Path · v')) (Eq.ndrec p hv) hu
 #align quiver.path.cast Quiver.Path.cast
 
 theorem Path.cast_eq_cast {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Path u v) :

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -63,7 +63,7 @@ structure IsTree : Prop where
 
 variable {G}
 
-@[simp] lemma isAcyclic_bot : IsAcyclic (⊥ : SimpleGraph V) := λ _a _w hw ↦ hw.ne_bot rfl
+@[simp] lemma isAcyclic_bot : IsAcyclic (⊥ : SimpleGraph V) := fun _a _w hw ↦ hw.ne_bot rfl
 
 theorem isAcyclic_iff_forall_adj_isBridge :
     G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w) := by

Mathlib/Combinatorics/SimpleGraph/Girth.lean

@@ -29,11 +29,11 @@ noncomputable def girth (G : SimpleGraph α) : ℕ∞ :=
 protected alias ⟨_, IsAcyclic.girth_eq_top⟩ := girth_eq_top
 
 lemma girth_anti : Antitone (girth : SimpleGraph α → ℕ∞) :=
-λ G H h ↦ iInf_mono λ a ↦ iInf₂_mono' λ w hw ↦ ⟨w.mapLe h, hw.mapLe _, by simp⟩
+fun G H h ↦ iInf_mono fun a ↦ iInf₂_mono' fun w hw ↦ ⟨w.mapLe h, hw.mapLe _, by simp⟩
 
 lemma exists_girth_eq_length :
     (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length) ↔ ¬ G.IsAcyclic := by
-  refine' ⟨_, λ h ↦ _⟩
+  refine' ⟨_, fun h ↦ _⟩
   · rintro ⟨a, w, hw, _⟩ hG
     exact hG _ hw
   · simp_rw [← girth_eq_top, ← Ne.def, girth, iInf_subtype', iInf_sigma', ENat.iInf_coe_ne_top,

Mathlib/Computability/AkraBazzi/AkraBazzi.lean

@@ -263,8 +263,8 @@ lemma eventually_log_b_mul_pos : ∀ᶠ (n:ℕ) in atTop, ∀ i, 0 < log (b i *
   induction n using Nat.strongInductionOn with
   | ind n h_ind =>
     cases lt_or_le n R.n₀ with
-    | inl hn => exact R.T_gt_zero' n hn   -- n < R.n₀
-    | inr hn =>   -- R.n₀ ≤ n
+    | inl hn => exact R.T_gt_zero' n hn -- n < R.n₀
+    | inr hn => -- R.n₀ ≤ n
       rw [R.h_rec n hn]
       have := R.g_nonneg
       refine add_pos_of_pos_of_nonneg (Finset.sum_pos ?sum_elems univ_nonempty) (by aesop)
@@ -609,7 +609,7 @@ lemma eventually_atTop_sumTransform_le :
   have hrpos_i := hrpos i
   have g_nonneg : 0 ≤ g n := R.g_nonneg n (by positivity)
   cases le_or_lt 0 (p a b + 1) with
-  | inl hp =>   -- 0 ≤ p a b + 1
+  | inl hp => -- 0 ≤ p a b + 1
     calc sumTransform (p a b) g (r i n) n
            = n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1)) := by rfl
          _ ≤ n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, c₂ * g n / u ^ ((p a b) + 1)) := by
@@ -641,7 +641,7 @@ lemma eventually_atTop_sumTransform_le :
          _ = c₂ * g n / c₁ ^ ((p a b) + 1) := by rw [div_self (by positivity), mul_one]
          _ = (c₂ / c₁ ^ ((p a b) + 1)) * g n := by ring
          _ ≤ max c₂ (c₂ / c₁ ^ ((p a b) + 1)) * g n := by gcongr; exact le_max_right _ _
-  | inr hp =>   -- p a b + 1 < 0
+  | inr hp => -- p a b + 1 < 0
     calc sumTransform (p a b) g (r i n) n
            = n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1)) := by rfl
          _ ≤ n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, c₂ * g n / u ^ ((p a b) + 1)) := by
@@ -688,7 +688,7 @@ lemma eventually_atTop_sumTransform_ge :
   have hrpos_i := hrpos i
   have g_nonneg : 0 ≤ g n := R.g_nonneg n (by positivity)
   cases le_or_gt 0 (p a b + 1) with
-  | inl hp =>   -- 0 ≤ (p a b) + 1
+  | inl hp => -- 0 ≤ (p a b) + 1
     calc sumTransform (p a b) g (r i n) n
            = n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, g u / u ^ ((p a b) + 1))     := by rfl
          _ ≥ n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, c₂ * g n / u^((p a b) + 1)) := by
@@ -722,7 +722,7 @@ lemma eventually_atTop_sumTransform_ge :
          _ = c₂ * (1 - c₃) * g n := by rw [div_self (by positivity), mul_one]
          _ ≥ min (c₂ * (1 - c₃)) ((1 - c₃) * c₂ / c₁ ^ ((p a b) + 1)) * g n := by
                 gcongr; exact min_le_left _ _
-  | inr hp =>  -- (p a b) + 1 < 0
+  | inr hp => -- (p a b) + 1 < 0
     calc sumTransform (p a b) g (r i n) n
         = n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, g u / u^((p a b) + 1))     := by rfl
       _ ≥ n ^ (p a b) * (∑ u in Finset.Ico (r i n) n, c₂ * g n / u ^ ((p a b) + 1)) := by
@@ -918,7 +918,7 @@ lemma growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) :
       (GrowsPolynomially.pow 2 growsPolynomially_log ?_)
     filter_upwards [eventually_ge_atTop 1] with _ hx
     exact log_nonneg hx
-  | inr hp =>  -- p ≠ 0
+  | inr hp => -- p ≠ 0
     refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p-1))
       (isTheta_deriv_rpow_p_mul_one_sub_smoothingFn hp) ?_
     filter_upwards [eventually_gt_atTop 0] with _ _
@@ -927,7 +927,7 @@ lemma growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) :
 lemma growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) :
     GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖ := by
   cases eq_or_ne p 0 with
-  | inl hp =>   -- p = 0
+  | inl hp => -- p = 0
     have h₁ : (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖)
         =ᶠ[atTop] fun z => z⁻¹ / (log z ^ 2) := by
       filter_upwards [eventually_deriv_one_add_smoothingFn, eventually_gt_atTop 1] with x hx hx_pos
@@ -941,7 +941,7 @@ lemma growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) :
       (GrowsPolynomially.pow 2 growsPolynomially_log ?_)
     filter_upwards [eventually_ge_atTop 1] with x hx
     exact log_nonneg hx
-  | inr hp =>    -- p ≠ 0
+  | inr hp => -- p ≠ 0
     refine GrowsPolynomially.of_isTheta (growsPolynomially_rpow (p-1))
       (isTheta_deriv_rpow_p_mul_one_add_smoothingFn hp) ?_
     filter_upwards [eventually_gt_atTop 0] with _ _