refactor(Analysis): golf 100 files

Mathlib/Analysis/Analytic/Basic.lean

@@ -237,20 +237,6 @@ theorem HasFPowerSeriesOnBall.mono (hf : HasFPowerSeriesOnBall f p x r) (r'_pos
     (hr : r' ≤ r) : HasFPowerSeriesOnBall f p x r' :=
   ⟨le_trans hr hf.1, r'_pos, fun hy => hf.hasSum (Metric.eball_subset_eball hr hy)⟩
 
-lemma HasFPowerSeriesWithinOnBall.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F}
-    {s : Set E} {x : E} {r : ℝ≥0∞} (h : HasFPowerSeriesWithinOnBall f p s x r)
-    (h' : EqOn g f (s ∩ Metric.eball x r)) (h'' : g x = f x) :
-    HasFPowerSeriesWithinOnBall g p s x r := by
-  refine ⟨h.r_le, h.r_pos, ?_⟩
-  intro y hy h'y
-  convert h.hasSum hy h'y using 1
-  simp only [mem_insert_iff, add_eq_left] at hy
-  rcases hy with rfl | hy
-  · simpa using h''
-  · apply h'
-    refine ⟨hy, ?_⟩
-    simpa [edist_eq_enorm_sub] using h'y
-
 /-- Variant of `HasFPowerSeriesWithinOnBall.congr` in which one requests equality on `insert x s`
 instead of separating `x` and `s`. -/
 lemma HasFPowerSeriesWithinOnBall.congr' {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F}
@@ -261,6 +247,16 @@ lemma HasFPowerSeriesWithinOnBall.congr' {f g : E → F} {p : FormalMultilinearS
   convert h.hasSum hy h'y using 1
   exact h' ⟨hy, by simpa [edist_eq_enorm_sub] using h'y⟩
 
+lemma HasFPowerSeriesWithinOnBall.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F}
+    {s : Set E} {x : E} {r : ℝ≥0∞} (h : HasFPowerSeriesWithinOnBall f p s x r)
+    (h' : EqOn g f (s ∩ Metric.eball x r)) (h'' : g x = f x) :
+    HasFPowerSeriesWithinOnBall g p s x r := by
+  refine h.congr' ?_
+  rintro y ⟨hy, h'y⟩
+  rcases hy with rfl | hy
+  · simpa using h''
+  · exact h' ⟨hy, by simpa [edist_eq_enorm_sub] using h'y⟩
+
 lemma HasFPowerSeriesWithinAt.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E}
     {x : E} (h : HasFPowerSeriesWithinAt f p s x) (h' : g =ᶠ[𝓝[s] x] f) (h'' : g x = f x) :
     HasFPowerSeriesWithinAt g p s x := by

Mathlib/Analysis/Analytic/CPolynomialDef.lean

@@ -233,20 +233,16 @@ the ball. -/
 theorem HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_zero
     (hf : HasFiniteFPowerSeriesOnBall f pf x 0 r) : ∀ y ∈ Metric.eball x r, f y = 0 := by
   intro y hy
-  rw [hf.eq_partialSum' y hy 0 le_rfl, FormalMultilinearSeries.partialSum]
-  simp only [Finset.range_zero, Finset.sum_empty]
+  simpa [FormalMultilinearSeries.partialSum] using hf.eq_partialSum' y hy 0 le_rfl
 
 theorem HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero (hf : ∀ y ∈ Metric.eball x r, f y = 0)
     (r_pos : 0 < r) (hp : ∀ n, p n = 0) : HasFiniteFPowerSeriesOnBall f p x 0 r := by
-  refine ⟨⟨?_, r_pos, ?_⟩, fun n _ ↦ hp n⟩
-  · rw [p.radius_eq_top_of_forall_image_add_eq_zero 0 (fun n ↦ by rw [add_zero]; exact hp n)]
-    exact le_top
-  · intro y hy
-    rw [hf (x + y)]
-    · convert hasSum_zero
-      rw [hp, ContinuousMultilinearMap.zero_apply]
-    · rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
-        ← edist_zero_right, ← Metric.mem_eball]
+  refine HasFiniteFPowerSeriesOnBall.mk' (fun n _ ↦ hp n) r_pos ?_
+  intro y hy
+  rw [hf (x + y)]
+  · simp
+  · rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
+      ← edist_zero_right, ← Metric.mem_eball]
 
 /-- If `f` has a formal power series at `x` bounded by `0`, then `f` is equal to `0` in a
 neighborhood of `x`. -/

Mathlib/Analysis/Analytic/Composition.lean

@@ -916,12 +916,8 @@ theorem HasFiniteFPowerSeriesAt.comp {m n : ℕ} {g : F → G} {f : E → F}
     contrapose! hi
     rw [← c.sum_blocksFun]
     rcases eq_zero_or_pos c.length with h'c | h'c
-    · have : ∑ j : Fin c.length, c.blocksFun j = 0 := by
-        apply Finset.sum_eq_zero (fun j hj ↦ ?_)
-        have := j.2
-        grind
-      rw [this]
-      exact mul_pos (by grind) hn
+    · have hi0 : i = 0 := (Composition.length_eq_zero (c := c)).1 h'c
+      simpa [hi0, h'c] using mul_pos (Nat.zero_lt_of_lt hc) hn
     · calc ∑ j : Fin c.length, c.blocksFun j
       _ < ∑ j : Fin c.length, n := by
         apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)

Mathlib/Analysis/Analytic/Constructions.lean

@@ -927,11 +927,8 @@ lemma AnalyticWithinAt.zpow {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
 @[to_fun]
 lemma AnalyticAt.zpow {f : E → 𝕝} {z : E} {n : ℤ} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
     AnalyticAt 𝕜 (f ^ n) z := by
-  by_cases hn : 0 ≤ n
-  · exact zpow_nonneg h₁f hn
-  · rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]
-    conv => arg 2; intro x; rw [zpow_neg]
-    exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)
+  rw [← analyticWithinAt_univ] at h₁f ⊢
+  exact h₁f.zpow h₂f
 
 /-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/

Mathlib/Analysis/Analytic/ConvergenceRadius.lean

@@ -252,17 +252,9 @@ theorem radius_eq_top_of_summable_norm (p : FormalMultilinearSeries 𝕜 E F)
   ENNReal.eq_top_of_forall_nnreal_le fun r => p.le_radius_of_summable_norm (hs r)
 
 theorem radius_eq_top_iff_summable_norm (p : FormalMultilinearSeries 𝕜 E F) :
-    p.radius = ∞ ↔ ∀ r : ℝ≥0, Summable fun n => ‖p n‖ * (r : ℝ) ^ n := by
-  constructor
-  · intro h r
-    obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius
-      (show (r : ℝ≥0∞) < p.radius from h.symm ▸ ENNReal.coe_lt_top)
-    refine .of_norm_bounded
-      (g := fun n ↦ (C : ℝ) * a ^ n) ((summable_geometric_of_lt_one ha.1.le ha.2).mul_left _)
-      fun n ↦ ?_
-    specialize hp n
-    rwa [Real.norm_of_nonneg (by positivity)]
-  · exact p.radius_eq_top_of_summable_norm
+    p.radius = ∞ ↔ ∀ r : ℝ≥0, Summable fun n => ‖p n‖ * (r : ℝ) ^ n :=
+  ⟨fun h _ ↦ p.summable_norm_mul_pow (h.symm ▸ ENNReal.coe_lt_top),
+    p.radius_eq_top_of_summable_norm⟩
 
 /-- If the radius of `p` is positive, then `‖pₙ‖` grows at most geometrically. -/
 theorem le_mul_pow_of_radius_pos (p : FormalMultilinearSeries 𝕜 E F) (h : 0 < p.radius) :

Mathlib/Analysis/Analytic/IteratedFDeriv.lean

@@ -127,17 +127,9 @@ lemma ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal
   rw [← sum_comp (Equiv.embeddingEquivOfFinite (Fin n))]
   congr with σ
   congr with i
-  have A : ∃ y, σ y = i := by
-    have : Function.Bijective σ := (Fintype.bijective_iff_injective_and_card _).2 ⟨σ.injective, rfl⟩
-    exact this.surjective i
-  rcases A with ⟨y, rfl⟩
-  simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte,
-    Function.Embedding.toEquivRange_symm_apply_self, ContinuousLinearMap.coe_pi',
-    ContinuousLinearMap.coe_id', id_eq, g]
-  congr 1
-  symm
+  obtain ⟨y, rfl⟩ := σ.equivOfFiniteSelfEmbedding.surjective i
   simp [inv_apply, Perm.inv_def,
-    ofBijective_symm_apply_apply, Function.Embedding.equivOfFiniteSelfEmbedding]
+    ofBijective_symm_apply_apply, Function.Embedding.equivOfFiniteSelfEmbedding, g]
 
 private lemma HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
     (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s)

Mathlib/Analysis/Analytic/OfScalars.lean

@@ -64,15 +64,9 @@ theorem ofScalars_series_of_subsingleton [Subsingleton E] : ofScalars E c = 0 :=
 
 variable (𝕜) in
 theorem ofScalars_series_injective [Nontrivial E] : Function.Injective (ofScalars E (𝕜 := 𝕜)) := by
-  intro _ _
-  refine Function.mtr fun h ↦ ?_
-  simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff,
-    ContinuousMultilinearMap.smul_apply]
-  push Not
-  obtain ⟨n, hn⟩ := Function.ne_iff.1 h
-  refine ⟨n, fun _ ↦ 1, ?_⟩
-  simp only [mkPiAlgebraFin_apply, List.ofFn_const, List.prod_replicate, one_pow, ne_eq]
-  exact (smul_left_injective 𝕜 one_ne_zero).ne hn
+  intro c c' h
+  funext n
+  simpa [ofScalars] using congrArg (fun p => p n fun _ ↦ (1 : E)) h
 
 variable (c)
 
@@ -91,19 +85,16 @@ lemma coeff_ofScalars {𝕜 : Type*} [NontriviallyNormedField 𝕜] {p : ℕ →
     (FormalMultilinearSeries.ofScalars 𝕜 p).coeff n = p n := by
   simp [FormalMultilinearSeries.coeff, FormalMultilinearSeries.ofScalars, List.prod_ofFn]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ofScalars_add (c' : ℕ → 𝕜) : ofScalars E (c + c') = ofScalars E c + ofScalars E c' := by
-  unfold ofScalars
-  simp_rw [Pi.add_apply, Pi.add_def _ _]
-  exact funext fun n ↦ Module.add_smul (c n) (c' n) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)
+  ext n x
+  simp [ofScalars, add_smul]
 
 lemma ofScalars_sub (c' : ℕ → 𝕜) : ofScalars E (c - c') = ofScalars E c - ofScalars E c' := by
   ext; simp [ofScalars, sub_smul]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ofScalars_smul (x : 𝕜) : ofScalars E (x • c) = x • ofScalars E c := by
-  unfold ofScalars
-  simp [Pi.smul_def x _, smul_smul]
+  ext n y
+  simp [ofScalars, smul_smul]
 
 theorem ofScalars_comp_neg_id :
     (ofScalars E c).compContinuousLinearMap (-ContinuousLinearMap.id _ _) =

Mathlib/Analysis/Analytic/Order.lean

@@ -611,14 +611,9 @@ codiscrete sets.
 theorem preimage_zero_mem_codiscreteWithin {x : 𝕜} (h₁f : AnalyticOnNhd 𝕜 f U) (h₂f : f x ≠ 0)
     (hx : x ∈ U) (hU : IsConnected U) :
     f ⁻¹' {0}ᶜ ∈ codiscreteWithin U := by
-  filter_upwards [h₁f.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top,
-    self_mem_codiscreteWithin U] with a ha h₂a
-  rw [← (h₁f x hx).analyticOrderAt_eq_zero] at h₂f
-  have {u : U} : analyticOrderAt f u ≠ ⊤ := by
-    apply (h₁f.exists_analyticOrderAt_ne_top_iff_forall hU).1
-    use ⟨x, hx⟩
-    simp_all
-  simp_all [(h₁f a h₂a).analyticOrderAt_eq_zero]
+  rcases h₁f.eqOn_zero_or_eventually_ne_zero_of_preconnected hU.isPreconnected with hzero | hne
+  · exact (h₂f (hzero hx)).elim
+  · simpa [Filter.Eventually, Set.mem_setOf_eq] using hne
 
 /--
 If an analytic function `f` is not constantly zero on `𝕜`, then its set of zeros is codiscrete.

Mathlib/Analysis/Analytic/Within.lean

@@ -118,16 +118,10 @@ lemma hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall [CompleteSpac
   constructor
   · intro h
     refine ⟨fun y ↦ p.sum (y - x), ?_, ?_⟩
-    · intro y ⟨ys,yb⟩
-      simp only [mem_eball, edist_eq_enorm_sub] at yb
-      have e0 := p.hasSum (x := y - x) ?_
-      · have e1 := (h.hasSum (y := y - x) ?_ ?_)
-        · simp only [add_sub_cancel] at e1
-          exact e1.unique e0
-        · simpa only [add_sub_cancel]
-        · simpa only [mem_eball, edist_zero_right]
-      · simp only [mem_eball, edist_zero_right]
-        exact lt_of_lt_of_le yb h.r_le
+    · rintro y ⟨ys, yb⟩
+      have : f (x + (y - x)) = p.sum (y - x) :=
+        h.sum (y := y - x) (by simpa using ys) (by simpa [edist_eq_enorm_sub] using yb)
+      simpa using this
     · refine ⟨h.r_le, h.r_pos, ?_⟩
       intro y lt
       simp only [add_sub_cancel_left]
@@ -181,19 +175,15 @@ lemma analyticWithinAt_iff_exists_analyticAt' [CompleteSpace F] {f : E → F} {s
   refine ⟨?_, ?_⟩
   · rintro ⟨g, hf, hg⟩
     rcases mem_nhdsWithin.1 hf with ⟨u, u_open, xu, hu⟩
-    let g' := Set.piecewise u g f
-    refine ⟨g', ?_, ?_, ?_⟩
-    · have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩
-      simpa [g', xu, this] using hu this
+    refine ⟨u.piecewise g f, ?_, ?_, ?_⟩
+    · simpa [xu] using hu ⟨xu, by simp⟩
     · intro y hy
       by_cases h'y : y ∈ u
-      · have : y ∈ u ∩ insert x s := ⟨h'y, hy⟩
-        simpa [g', h'y, this] using hu this
-      · simp [g', h'y]
-    · apply hg.congr
-      filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]
+      · simpa [h'y] using hu ⟨h'y, hy⟩
+      · simp [h'y]
+    · exact hg.congr <| (Set.piecewise_eqOn u g f).symm.eventuallyEq_of_mem (u_open.mem_nhds xu)
   · rintro ⟨g, -, hf, hg⟩
-    exact ⟨g, by filter_upwards [self_mem_nhdsWithin] using hf, hg⟩
+    exact ⟨g, hf.eventuallyEq_of_mem self_mem_nhdsWithin, hg⟩
 
 alias ⟨AnalyticWithinAt.exists_analyticAt, _⟩ := analyticWithinAt_iff_exists_analyticAt'
 

Mathlib/Analysis/AperiodicOrder/Delone/Basic.lean

@@ -119,14 +119,11 @@ theorem copy_eq (D : DeloneSet X)
 lemma packingRadius_lt_dist_of_mem_ne (D : DeloneSet X) {x y : X}
     (hx : x ∈ D) (hy : y ∈ D) (hne : x ≠ y) :
     D.packingRadius < dist x y := by
-  have hsep : ENNReal.ofReal D.packingRadius < ENNReal.ofReal (dist x y) := by
-    simpa [edist_dist] using D.isSeparated_packingRadius hx hy hne
-  exact (ENNReal.ofReal_lt_ofReal_iff (h := dist_pos.mpr hne)).1 hsep
+  simpa [edist_dist] using D.isSeparated_packingRadius hx hy hne
 
 lemma exists_dist_le_coveringRadius (D : DeloneSet X) (x : X) :
     ∃ y ∈ D, dist x y ≤ D.coveringRadius := by
-  obtain ⟨y, hy, hdist⟩ := D.isCover_coveringRadius (x := x) (by trivial)
-  exact ⟨y, hy, by simpa [edist_dist] using hdist⟩
+  simpa [edist_dist] using D.isCover_coveringRadius (by trivial)
 
 lemma eq_of_mem_ball (D : DeloneSet X) {r : ℝ≥0} (hr : r ≤ D.packingRadius / 2)
     {x y z : X} (hx : x ∈ D) (hy : y ∈ D) (hxz : x ∈ ball z r) (hyz : y ∈ ball z r) :
@@ -170,11 +167,7 @@ lemma mapBilipschitz_trans {Z : Type*} [MetricSpace Z] (D : DeloneSet X)
     D.mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f)
       (mul_pos hf₁_pos hg₁_pos) (mul_pos hg₂_pos hf₂_pos)
       (hg_anti.comp hf_anti) (hg_lip.comp hf_lip) := by
-  ext
-  · simp only [mapBilipschitz_carrier, Equiv.trans_apply, Set.mem_image]
-    exact exists_exists_and_eq_and
-  · simp only [mapBilipschitz_packingRadius, NNReal.coe_div, div_div]
-  · simp only [mapBilipschitz_coveringRadius, NNReal.coe_mul, mul_assoc]
+  (ext <;> simp [mapBilipschitz, Equiv.trans_apply, div_div, mul_assoc]); grind
 
 /-- The image of a Delone set under an isometry. This is a specialization of
 `DeloneSet.mapBilipschitz` where the packing and covering radii are preserved because the

Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

@@ -118,13 +118,9 @@ theorem isEquivalent_zero_iff_isBigO_zero : u ~[l] 0 ↔ u =O[l] (0 : α → β)
 
 theorem isEquivalent_const_iff_tendsto {c : β} (h : c ≠ 0) :
     u ~[l] const _ c ↔ Tendsto u l (𝓝 c) := by
-  simp +unfoldPartialApp only [IsEquivalent, const, isLittleO_const_iff h]
-  constructor <;> intro h
-  · have := h.sub (tendsto_const_nhds (x := -c))
-    simp only [Pi.sub_apply, sub_neg_eq_add, sub_add_cancel, zero_add] at this
-    exact this
-  · have := h.sub (tendsto_const_nhds (x := c))
-    rwa [sub_self] at this
+  rw [IsEquivalent]
+  change (u - const α c) =o[l] (fun _ : α => c) ↔ Tendsto u l (𝓝 c)
+  simpa [isLittleO_const_iff h] using tendsto_sub_const_iff c (c := c)
 
 theorem IsEquivalent.tendsto_const {c : β} (hu : u ~[l] const _ c) : Tendsto u l (𝓝 c) := by
   rcases em <| c = 0 with rfl | h
@@ -207,16 +203,13 @@ theorem isEquivalent_of_tendsto_one (huv : Tendsto (u / v) l (𝓝 1)) :
 
 theorem isEquivalent_iff_tendsto_one (hz : ∀ᶠ x in l, v x ≠ 0) :
     u ~[l] v ↔ Tendsto (u / v) l (𝓝 1) := by
-  constructor
-  · intro hequiv
-    have := hequiv.isLittleO.tendsto_div_nhds_zero
-    simp only [Pi.sub_apply, sub_div] at this
-    have key : Tendsto (fun x ↦ v x / v x) l (𝓝 1) :=
-      (tendsto_congr' <| hz.mono fun x hnz ↦ @div_self _ _ (v x) hnz).mpr tendsto_const_nhds
-    convert this.add key
-    · simp
-    · simp
-  · exact isEquivalent_of_tendsto_one
+  rw [IsEquivalent, isLittleO_iff_tendsto' (hz.mono fun x hx hx0 => (hx hx0).elim)]
+  change Tendsto (fun x ↦ (u x - v x) / v x) l (𝓝 0) ↔ Tendsto (u / v) l (𝓝 1)
+  have : Tendsto (fun x ↦ (u x - v x) / v x) l (𝓝 0) ↔
+      Tendsto (fun x ↦ u x / v x - 1) l (𝓝 0) :=
+    tendsto_congr' <| hz.mono fun x hx => by simp [sub_div, hx]
+  rw [this]
+  exact tendsto_sub_nhds_zero_iff
 
 end NormedField
 

Mathlib/Analysis/Asymptotics/Defs.lean

@@ -897,21 +897,17 @@ section
 
 variable (l' : Filter β)
 
-protected theorem IsBigO.comp_fst : f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst) := by
-  simp only [isBigO_iff, eventually_prod_iff]
-  exact fun ⟨c, hc⟩ ↦ ⟨c, _, hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩
+protected theorem IsBigO.comp_fst : f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst) :=
+  fun h ↦ h.comp_tendsto Filter.tendsto_fst
 
-protected theorem IsBigO.comp_snd : f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd) := by
-  simp only [isBigO_iff, eventually_prod_iff]
-  exact fun ⟨c, hc⟩ ↦ ⟨c, fun _ ↦ True, eventually_true l', _, hc, fun _ ↦ id⟩
+protected theorem IsBigO.comp_snd : f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd) :=
+  fun h ↦ h.comp_tendsto Filter.tendsto_snd
 
-protected theorem IsLittleO.comp_fst : f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst) := by
-  simp only [isLittleO_iff, eventually_prod_iff]
-  exact fun h _ hc ↦ ⟨_, h hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩
+protected theorem IsLittleO.comp_fst : f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst) :=
+  fun h ↦ h.comp_tendsto Filter.tendsto_fst
 
-protected theorem IsLittleO.comp_snd : f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd) := by
-  simp only [isLittleO_iff, eventually_prod_iff]
-  exact fun h _ hc ↦ ⟨fun _ ↦ True, eventually_true l', _, h hc, fun _ ↦ id⟩
+protected theorem IsLittleO.comp_snd : f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd) :=
+  fun h ↦ h.comp_tendsto Filter.tendsto_snd
 
 end
 

Mathlib/Analysis/Asymptotics/ExpGrowth.lean

@@ -250,25 +250,17 @@ lemma expGrowthSup_inv : expGrowthSup u⁻¹ = - expGrowthInf u := by
 -- `IsBigO` property is spelt out.
 lemma expGrowthInf_le_of_eventually_le (hb : b ≠ ∞) (h : ∀ᶠ n in atTop, u n ≤ b * v n) :
     expGrowthInf u ≤ expGrowthInf v := by
-  apply (expGrowthInf_eventually_monotone h).trans
-  rcases eq_zero_or_pos b with rfl | b_pos
-  · simp only [zero_mul, ← Pi.zero_def, expGrowthInf_zero, bot_le]
-  · apply (expGrowthInf_mul_le _ _).trans_eq <;> rw [expGrowthSup_const b_pos.ne' hb]
-    · exact zero_add (expGrowthInf v)
-    · exact .inl zero_ne_bot
-    · exact .inl zero_ne_top
+  rw [expGrowthInf_def, expGrowthInf_def]
+  exact linearGrowthInf_le_of_eventually_le (u := log ∘ u) (v := log ∘ v) (b := log b) (by simpa) <|
+    h.mono fun n hn ↦ by simpa [Pi.mul_apply, log_mul_add, add_comm] using log_monotone hn
 
 -- Bound on `expGrowthSup` under a `IsBigO` hypothesis. However, `ℝ≥0∞` is not normed, so the
 -- `IsBigO` property is spelt out.
 lemma expGrowthSup_le_of_eventually_le (hb : b ≠ ∞) (h : ∀ᶠ n in atTop, u n ≤ b * v n) :
     expGrowthSup u ≤ expGrowthSup v := by
-  apply (expGrowthSup_eventually_monotone h).trans
-  rcases eq_zero_or_pos b with rfl | b_pos
-  · simp only [zero_mul, ← Pi.zero_def, expGrowthSup_zero, bot_le]
-  · apply (expGrowthSup_mul_le _ _).trans_eq <;> rw [expGrowthSup_const b_pos.ne' hb]
-    · exact zero_add (expGrowthSup v)
-    · exact .inl zero_ne_bot
-    · exact .inl zero_ne_top
+  rw [expGrowthSup_def, expGrowthSup_def]
+  exact linearGrowthSup_le_of_eventually_le (u := log ∘ u) (v := log ∘ v) (b := log b) (by simpa) <|
+    h.mono fun n hn ↦ by simpa [Pi.mul_apply, log_mul_add, add_comm] using log_monotone hn
 
 lemma expGrowthInf_of_eventually_ge (hb : b ≠ 0) (h : ∀ᶠ n in atTop, b * u n ≤ v n) :
     expGrowthInf u ≤ expGrowthInf v := by

Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

@@ -44,18 +44,9 @@ open Bornology
 
 theorem Asymptotics.isLittleO_pow_pow_cobounded_of_lt (hpq : p < q) :
     (· ^ p) =o[cobounded R] (· ^ q) := by
-  nontriviality R
-  have noc : NormOneClass R := NormMulClass.toNormOneClass
-  refine IsLittleO.of_bound fun c cpos ↦ ?_
-  rw [← Nat.sub_add_cancel hpq.le]
-  simp_rw [pow_add, norm_mul, norm_pow, eventually_iff_exists_mem]
-  refine ⟨{y | c⁻¹ ≤ ‖y‖ ^ (q - p)}, ?_, fun y my ↦ ?_⟩
-  · have key : Tendsto (‖·‖ ^ (q - p)) (cobounded R) atTop :=
-      (tendsto_pow_atTop (Nat.sub_ne_zero_iff_lt.mpr hpq)).comp tendsto_norm_cobounded_atTop
-    rw [tendsto_atTop] at key
-    exact mem_map.mp (key c⁻¹)
-  · rw [← inv_mul_le_iff₀ cpos]
-    gcongr; exact my
+  rw [← Nat.add_sub_of_le hpq.le]
+  simpa [pow_add] using (isBigO_refl (fun x ↦ x ^ p) (cobounded R)).mul_isLittleO
+    ((isLittleO_const_id_cobounded (1 : R)).pow (Nat.sub_pos_of_lt hpq))
 
 theorem Asymptotics.isBigO_pow_pow_cobounded_of_le (hpq : p ≤ q) :
     (· ^ p) =O[cobounded R] (· ^ q) := by