awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : Function.uncurry A =O[SProd.sprod (α := Filter ι) ⊤ l] Function.uncurry B
obtain :
  ∀ (C : ℝ) (hC : IsBigOWith C (SProd.sprod (α := Filter ι) ⊤ l) (Function.uncurry A) (Function.uncurry B)),
    ∃ (c : ℝ),
      IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖
⊢ ∃ (c : ℝ),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
obtain ⟨C, hC⟩ := hAB.isBigOWith

Premises used: Asymptotics.IsBigO.isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : Function.uncurry A =O[SProd.sprod (α := Filter ι) ⊤ l] Function.uncurry B
C : ℝ
hC : IsBigOWith C (SProd.sprod (α := Filter ι) ⊤ l) (Function.uncurry A) (Function.uncurry B)
⊢ ∃ (c : ℝ),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
⟨C, hC.sum_congr'⟩

Premises used: Asymptotics.IsBigOWith.sum_congr', Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : Function.uncurry A =O[SProd.sprod (α := Filter ι) ⊤ l] Function.uncurry B
C : ℝ
hC : IsBigOWith C (SProd.sprod (α := Filter ι) ⊤ l) (Function.uncurry A) (Function.uncurry B)
⊢ ∃ (c : ℝ),
    IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
exact ⟨C, hC.sum_congr'⟩
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : Function.uncurry A =o[SProd.sprod (α := Filter ι) ⊤ l] Function.uncurry B
rw :
  ∀ (hAB : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (SProd.sprod (α := Filter ι) ⊤ l) (Function.uncurry A) (Function.uncurry B))
    ⦃c : ℝ⦄,
    0 < c →
      IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖
⊢ IsLittleO.{u_1, u_6, 0} (E := E') (F := ℝ) l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
rw [isLittleO_iff_forall_isBigOWith] at *

Premises used: Asymptotics.isLittleO_iff_forall_isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (SProd.sprod (α := Filter ι) ⊤ l) (Function.uncurry A) (Function.uncurry B)
c : ℝ
hc : 0 < c
⊢ IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
(hAB hc).sum_congr'

Premises used: Asymptotics.IsBigOWith.sum_congr'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (SProd.sprod (α := Filter ι) ⊤ l) (Function.uncurry A) (Function.uncurry B)
c : ℝ
hc : 0 < c
⊢ IsBigOWith.{u_1, u_6, 0} (E := E') (F := ℝ) c l (fun (H : α) ↦ ∑ j ∈ i H, A j H) fun (H : α) ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
exact (hAB hc).sum_congr'

Premises used: Asymptotics.IsBigOWith.sum_congr'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
h : IsBigOWith c l u v
y : α
hy : ‖u y‖ ≤ c * ‖v y‖
hv : v y = 0
⊢ u y = 0

Tactic:
simpa [hv] using hy
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
⊢ u / v * v =ᶠ[l] u

Tactic:
let ⟨_c, hc⟩ := h.isBigOWith
  hc.eventually_mul_div_cancel

Premises used: HMul.hMul, Filter.EventuallyEq, HDiv.hDiv, Asymptotics.IsBigOWith.eventually_mul_div_cancel, _private.0.Asymptotics.IsBigO.eventually_mul_div_cancel.match_1, Asymptotics.IsBigO.isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =o[l] v
⊢ u / v * v =ᶠ[l] u

Tactic:
(h.forall_isBigOWith zero_lt_one).eventually_mul_div_cancel

Premises used: Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsBigOWith.eventually_mul_div_cancel, zero_lt_one
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
⊢ expGrowthInf u = linearGrowthInf (log ∘ u)

Tactic:
rfl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
⊢ expGrowthSup u = linearGrowthSup (log ∘ u)

Tactic:
rfl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : u =ᶠ[atTop] v
⊢ expGrowthInf u = expGrowthInf v

Tactic:
liminf_congr (h.mono fun _ uv ↦ uv ▸ rfl)

Premises used: ExpGrowth.expGrowthInf, Eq.rec, Filter.liminf_congr, Filter.Eventually.mono, rfl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : u =ᶠ[atTop] v
⊢ expGrowthSup u = expGrowthSup v

Tactic:
limsup_congr (h.mono fun _ uv ↦ uv ▸ rfl)

Premises used: Eq.rec, Filter.Eventually.mono, Filter.limsup_congr, ExpGrowth.expGrowthSup, rfl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : u ≤ᶠ[atTop] v
⊢ expGrowthInf u ≤ expGrowthInf v

Tactic:
liminf_le_liminf (h.mono fun n uv ↦ monotone_div_right_of_nonneg n.cast_nonneg' (log_monotone uv))

Premises used: ExpGrowth.expGrowthInf, ENNReal.log_monotone, Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg, Filter.Eventually.mono, Filter.liminf_le_liminf
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
⊢ Monotone expGrowthInf

Tactic:
fun _ _ uv ↦ expGrowthInf_eventually_monotone (Eventually.of_forall uv)

Premises used: ExpGrowth.expGrowthInf_eventually_monotone, Monotone, Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : u ≤ᶠ[atTop] v
⊢ expGrowthSup u ≤ expGrowthSup v

Tactic:
limsup_le_limsup (h.mono fun n uv ↦ monotone_div_right_of_nonneg n.cast_nonneg' (log_monotone uv))

Premises used: ENNReal.log_monotone, Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg, Filter.Eventually.mono, Filter.limsup_le_limsup, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
⊢ Monotone expGrowthSup

Tactic:
fun _ _ uv ↦ expGrowthSup_eventually_monotone (Eventually.of_forall uv)

Premises used: Monotone, Filter.Eventually.of_forall, ExpGrowth.expGrowthSup_eventually_monotone
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
⊢ expGrowthInf u ≤ expGrowthSup u

Tactic:
liminf_le_limsup

Premises used: ExpGrowth.expGrowthInf, Filter.liminf_le_limsup, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ v n
n : ℕ
u_v : u n ≤ v n
h₁ : LE.le (α := EReal) 0 (↑n : EReal)
⊢ (u n).log / (↑n : EReal) ≤ (v n).log / (↑n : EReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
rw :
  (∀ y > a, ∃ᶠ (a : ℕ) in atTop, (u a).log / (↑a : EReal) ≤ y) ↔
    ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp
⊢ expGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp

Tactic:
rw [expGrowthInf, liminf_le_iff']

Premises used: ExpGrowth.expGrowthInf, Filter.liminf_le_iff'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, (u a).log / (↑a : EReal) ≤ y) ↔
    ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp

Tactic:
forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.frequently_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
refine : ∀ b > a, ∀ n ≥ 1, (u n).log / (↑n : EReal) ≤ b ↔ u n ≤ (b * (↑n : EReal)).exp
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, (u a).log / (↑a : EReal) ≤ y) ↔
    ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp

Tactic:
refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.frequently_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b > a
n : ℕ
h_1 : n ≥ 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < n
⊢ LT.lt (α := EReal) 0 (↑n : EReal)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b > a
n : ℕ
h_1 : n ≥ 1
rw : (u n).log ≤ (b * (↑n : EReal)).exp.log ↔ u n ≤ (b * (↑n : EReal)).exp
⊢ (u n).log / (↑n : EReal) ≤ b ↔ u n ≤ (b * (↑n : EReal)).exp

Tactic:
rw [div_le_iff_le_mul (by norm_cast) (natCast_ne_top n), ← log_exp (n * b), mul_comm _ b]

Premises used: HMul.hMul, Nat.cast, mul_comm, EReal.natCast_ne_top, EReal.div_le_iff_le_mul, EReal.log_exp
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b > a
n : ℕ
h_1 : n ≥ 1
⊢ (u n).log ≤ (b * (↑n : EReal)).exp.log ↔ u n ≤ (b * (↑n : EReal)).exp

Tactic:
logOrderIso.le_iff_le

Premises used: ENNReal.log, OrderIso.le_iff_le, ENNReal.logOrderIso, ite
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b > a
n : ℕ
h_1 : n ≥ 1
⊢ (u n).log ≤ (b * (↑n : EReal)).exp.log ↔ u n ≤ (b * (↑n : EReal)).exp

Tactic:
exact logOrderIso.le_iff_le

Premises used: OrderIso.le_iff_le, ENNReal.logOrderIso
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
rw :
  (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ (u a).log / (↑a : EReal)) ↔
    ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n
⊢ a ≤ expGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n

Tactic:
rw [expGrowthInf, le_liminf_iff']

Premises used: ExpGrowth.expGrowthInf, Filter.le_liminf_iff'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ (u a).log / (↑a : EReal)) ↔
    ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n

Tactic:
forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.eventually_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
refine : ∀ b < a, ∀ n ≥ 1, b ≤ (u n).log / (↑n : EReal) ↔ (b * (↑n : EReal)).exp ≤ u n
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ (u a).log / (↑a : EReal)) ↔
    ∀ b < a, ∀ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n

Tactic:
refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.eventually_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b < a
n : ℕ
h_1 : n ≥ 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < n
⊢ GT.gt (α := EReal) (↑n : EReal) 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b < a
n : ℕ
h_1 : n ≥ 1
nth_rw : (b * (↑n : EReal)).exp.log ≤ (u n).log ↔ (b * (↑n : EReal)).exp ≤ u n
⊢ b ≤ (u n).log / (↑n : EReal) ↔ (b * (↑n : EReal)).exp ≤ u n

Tactic:
nth_rw 1 [le_div_iff_mul_le (by norm_cast) (natCast_ne_top n), ← log_exp (b * n)]

Premises used: HMul.hMul, Nat.cast, EReal.natCast_ne_top, EReal.le_div_iff_mul_le, EReal.log_exp
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b < a
n : ℕ
h_1 : n ≥ 1
⊢ (b * (↑n : EReal)).exp.log ≤ (u n).log ↔ (b * (↑n : EReal)).exp ≤ u n

Tactic:
logOrderIso.le_iff_le

Premises used: ENNReal.log, OrderIso.le_iff_le, ENNReal.logOrderIso, ite
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a b : EReal
h : b < a
n : ℕ
h_1 : n ≥ 1
⊢ (b * (↑n : EReal)).exp.log ≤ (u n).log ↔ (b * (↑n : EReal)).exp ≤ u n

Tactic:
exact logOrderIso.le_iff_le

Premises used: OrderIso.le_iff_le, ENNReal.logOrderIso
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
rw :
  (∀ y > a, ∀ᶠ (a : ℕ) in atTop, (u a).log / (↑a : EReal) ≤ y) ↔
    ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp
⊢ expGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp

Tactic:
rw [expGrowthSup, limsup_le_iff']

Premises used: Filter.limsup_le_iff', ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, (u a).log / (↑a : EReal) ≤ y) ↔
    ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp

Tactic:
forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.eventually_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
refine : ∀ b > a, ∀ n ≥ 1, (u n).log / (↑n : EReal) ≤ b ↔ u n ≤ (b * (↑n : EReal)).exp
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, (u a).log / (↑a : EReal) ≤ y) ↔
    ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ (b * (↑n : EReal)).exp

Tactic:
refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.eventually_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
rw :
  (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ (u a).log / (↑a : EReal)) ↔
    ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n
⊢ a ≤ expGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n

Tactic:
rw [expGrowthSup, le_limsup_iff']

Premises used: Filter.le_limsup_iff', ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ (u a).log / (↑a : EReal)) ↔
    ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n

Tactic:
forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.frequently_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
refine : ∀ b < a, ∀ n ≥ 1, b ≤ (u n).log / (↑n : EReal) ↔ (b * (↑n : EReal)).exp ≤ u n
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ (u a).log / (↑a : EReal)) ↔
    ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * (↑n : EReal)).exp ≤ u n

Tactic:
refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.frequently_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : expGrowthInf u < a
⊢ ∃ᶠ (n : ℕ) in atTop, u n ≤ (a * (↑n : EReal)).exp

Tactic:
expGrowthInf_le_iff.1 (le_refl (expGrowthInf u)) a h

Premises used: le_refl, ExpGrowth.expGrowthInf, ExpGrowth.expGrowthInf_le_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : a < expGrowthInf u
⊢ ∀ᶠ (n : ℕ) in atTop, (a * (↑n : EReal)).exp ≤ u n

Tactic:
le_expGrowthInf_iff.1 (le_refl (expGrowthInf u)) a h

Premises used: le_refl, ExpGrowth.expGrowthInf, ExpGrowth.le_expGrowthInf_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : expGrowthSup u < a
⊢ ∀ᶠ (n : ℕ) in atTop, u n ≤ (a * (↑n : EReal)).exp

Tactic:
expGrowthSup_le_iff.1 (le_refl (expGrowthSup u)) a h

Premises used: le_refl, Iff.mp, ExpGrowth.expGrowthSup_le_iff, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : a < expGrowthSup u
⊢ ∃ᶠ (n : ℕ) in atTop, (a * (↑n : EReal)).exp ≤ u n

Tactic:
le_expGrowthSup_iff.1 (le_refl (expGrowthSup u)) a h

Premises used: le_refl, Iff.mp, ExpGrowth.expGrowthSup, ExpGrowth.le_expGrowthSup_iff
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ (a * (↑n : EReal)).exp
apply :
  ∀ (c : EReal) (c_u : c > a) (n : ℕ) (hn : u n ≤ (a * (↑n : EReal)).exp),
    (a * (↑n : EReal)).exp ≤ (c * (↑n : EReal)).exp
⊢ expGrowthInf u ≤ a

Tactic:
apply expGrowthInf_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans ?_

Premises used: Iff.mpr, ExpGrowth.expGrowthInf_le_iff, Filter.Frequently.mono, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ (a * (↑n : EReal)).exp
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ (a * (↑n : EReal)).exp
a₁ : LE.le (α := EReal) 0 (↑n : EReal)
⊢ (a * (↑n : EReal)).exp ≤ (c * (↑n : EReal)).exp

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, (a * (↑n : EReal)).exp ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : (a * (↑n : EReal)).exp ≤ u n
a₁ : LE.le (α := EReal) 0 (↑n : EReal)
⊢ (c * (↑n : EReal)).exp ≤ (a * (↑n : EReal)).exp

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ (a * (↑n : EReal)).exp
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ (a * (↑n : EReal)).exp
a₁ : LE.le (α := EReal) 0 (↑n : EReal)
⊢ (a * (↑n : EReal)).exp ≤ (c * (↑n : EReal)).exp

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, (a * (↑n : EReal)).exp ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : (a * (↑n : EReal)).exp ≤ u n
a₁ : LE.le (α := EReal) 0 (↑n : EReal)
⊢ (c * (↑n : EReal)).exp ≤ (a * (↑n : EReal)).exp

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
rw : linearGrowthSup (log ∘ 0) = linearGrowthSup ⊥
⊢ expGrowthSup 0 = ⊥

Tactic:
rw [← linearGrowthSup_bot, expGrowthSup_def]

Premises used: LinearGrowth.linearGrowthSup_bot, ExpGrowth.expGrowthSup_def
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
e_u : Eq (α := ℕ → EReal) (log ∘ 0) ⊥
⊢ linearGrowthSup (log ∘ 0) = linearGrowthSup ⊥

Tactic:
congr 1
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
e_u : ∀ (x : ℕ), (log ∘ 0) x = ⊥ x
⊢ Eq (α := ℕ → EReal) (log ∘ 0) ⊥

Tactic:
ext _
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
x : ℕ
e_u : log (0 x) = ⊥ x
e_u₁ : log 0 = ⊥ x
e_u₂ : log 0 = ⊥
e_u₃ e_u₄ : Eq (α := EReal) ⊥ ⊥
⊢ (log ∘ 0) x = ⊥ x

Tactic:
rw [comp_apply, Pi.zero_apply, Pi.bot_apply, log_zero]

Premises used: Pi.zero_apply, Pi.bot_apply, ENNReal.log_zero, Function.comp_apply
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
apply : expGrowthInf 0 ≤ ⊥
⊢ expGrowthInf 0 = ⊥

Tactic:
apply le_bot_iff.1

Premises used: le_bot_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
rw : expGrowthInf 0 ≤ expGrowthSup 0
⊢ expGrowthInf 0 ≤ ⊥

Tactic:
rw [← expGrowthSup_zero]

Premises used: ExpGrowth.expGrowthSup_zero
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
⊢ expGrowthInf 0 ≤ expGrowthSup 0

Tactic:
expGrowthInf_le_expGrowthSup

Premises used: ExpGrowth.expGrowthInf_le_expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
⊢ expGrowthInf 0 ≤ expGrowthSup 0

Tactic:
exact expGrowthInf_le_expGrowthSup

Premises used: ExpGrowth.expGrowthInf_le_expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
rw : linearGrowthInf (log ∘ ⊤) = linearGrowthInf ⊤
⊢ expGrowthInf ⊤ = ⊤

Tactic:
rw [← linearGrowthInf_top, expGrowthInf_def]

Premises used: LinearGrowth.linearGrowthInf_top, ExpGrowth.expGrowthInf_def
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
⊢ linearGrowthInf (log ∘ ⊤) = linearGrowthInf ⊤

Tactic:
rfl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
apply : ⊤ ≤ expGrowthSup ⊤
⊢ expGrowthSup ⊤ = ⊤

Tactic:
apply top_le_iff.1

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
rw : expGrowthInf ⊤ ≤ expGrowthSup ⊤
⊢ ⊤ ≤ expGrowthSup ⊤

Tactic:
rw [← expGrowthInf_top]

Premises used: ExpGrowth.expGrowthInf_top
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
⊢ expGrowthInf ⊤ ≤ expGrowthSup ⊤

Tactic:
expGrowthInf_le_expGrowthSup

Premises used: ExpGrowth.expGrowthInf_le_expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
⊢ expGrowthInf ⊤ ≤ expGrowthSup ⊤

Tactic:
exact expGrowthInf_le_expGrowthSup

Premises used: ExpGrowth.expGrowthInf_le_expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
b : ℝ≥0∞
h : b ≠ 0
h' : b ≠ ∞
⊢ (expGrowthInf fun (x : ℕ) ↦ b) = 0

Tactic:
(tendsto_const_div_atTop_nhds_zero_nat (fun k ↦ h (log_eq_bot_iff.1 k))
    (fun k ↦ h' (log_eq_top_iff.1 k))).liminf_eq

Premises used: ENNReal.log_eq_bot_iff, ExpGrowth.expGrowthInf, EReal.tendsto_const_div_atTop_nhds_zero_nat, Filter.Tendsto.liminf_eq, ENNReal.log_eq_top_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
b : ℝ≥0∞
h : b ≠ 0
h' : b ≠ ∞
⊢ (expGrowthSup fun (x : ℕ) ↦ b) = 0

Tactic:
(tendsto_const_div_atTop_nhds_zero_nat (fun k ↦ h (log_eq_bot_iff.1 k))
    (fun k ↦ h' (log_eq_top_iff.1 k))).limsup_eq

Premises used: Filter.Tendsto.limsup_eq, ENNReal.log_eq_bot_iff, EReal.tendsto_const_div_atTop_nhds_zero_nat, ENNReal.log_eq_top_iff, Iff.mp, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
b : ℝ≥0∞
rw : Eq (α := EReal) (liminf (fun (n : ℕ) ↦ (b ^ n).log / (↑n : EReal)) atTop) (liminf (fun (x : ℕ) ↦ b.log) atTop)
⊢ (expGrowthInf fun (n : ℕ) ↦ b ^ n) = b.log

Tactic:
rw [expGrowthInf, ← liminf_const (f := atTop (α := ℕ)) (log b)]

Premises used: ExpGrowth.expGrowthInf, ENNReal.log, Filter.liminf_const
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
b : ℝ≥0∞
⊢ Eq (α := EReal) (liminf (fun (n : ℕ) ↦ (b ^ n).log / (↑n : EReal)) atTop) (liminf (fun (x : ℕ) ↦ b.log) atTop)

Tactic:
liminf_congr (eventually_atTop.2 ⟨1, fun n n_1 ↦ ?_⟩)

Premises used: Iff.mpr, Filter.liminf_congr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
b : ℝ≥0∞
refine : ∀ (n : ℕ) (n_1 : n ≥ 1), (b ^ n).log / (↑n : EReal) = b.log
⊢ Eq (α := EReal) (liminf (fun (n : ℕ) ↦ (b ^ n).log / (↑n : EReal)) atTop) (liminf (fun (x : ℕ) ↦ b.log) atTop)

Tactic:
refine liminf_congr (eventually_atTop.2 ⟨1, fun n n_1 ↦ ?_⟩)

Premises used: Iff.mpr, Filter.liminf_congr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
b : ℝ≥0∞
n : ℕ
n_1 : n ≥ 1
rw : (b ^ n).log = b.log * (↑n : EReal)
rw₁ : (↑n : EReal) * b.log = b.log * (↑n : EReal)
rw₂ rw₃ : b.log * (↑n : EReal) = b.log * (↑n : EReal)
⊢ (b ^ n).log / (↑n : EReal) = b.log

Tactic:
rw [EReal.div_eq_iff (natCast_ne_bot n) (natCast_ne_top n)
    (zero_lt_one.trans_le (Nat.one_le_cast.2 n_1)).ne.symm, log_pow, mul_comm]

Premises used: Iff.mpr, Nat.one_le_cast, Ne.symm, ENNReal.log_pow, zero_lt_one, LT.lt.trans_le, mul_comm, EReal.natCast_ne_top, EReal.div_eq_iff, EReal.natCast_ne_bot, LT.lt.ne
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
b : ℝ≥0∞
rw : Eq (α := EReal) (limsup (fun (n : ℕ) ↦ (b ^ n).log / (↑n : EReal)) atTop) (limsup (fun (x : ℕ) ↦ b.log) atTop)
⊢ (expGrowthSup fun (n : ℕ) ↦ b ^ n) = b.log

Tactic:
rw [expGrowthSup, ← limsup_const (f := atTop (α := ℕ)) (log b)]

Premises used: Filter.limsup_const, ENNReal.log, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
b : ℝ≥0∞
⊢ Eq (α := EReal) (limsup (fun (n : ℕ) ↦ (b ^ n).log / (↑n : EReal)) atTop) (limsup (fun (x : ℕ) ↦ b.log) atTop)

Tactic:
limsup_congr (eventually_atTop.2 ⟨1, fun n n_1 ↦ ?_⟩)

Premises used: Iff.mpr, Exists.intro, Filter.limsup_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
b : ℝ≥0∞
refine : ∀ (n : ℕ) (n_1 : n ≥ 1), (b ^ n).log / (↑n : EReal) = b.log
⊢ Eq (α := EReal) (limsup (fun (n : ℕ) ↦ (b ^ n).log / (↑n : EReal)) atTop) (limsup (fun (x : ℕ) ↦ b.log) atTop)

Tactic:
refine limsup_congr (eventually_atTop.2 ⟨1, fun n n_1 ↦ ?_⟩)

Premises used: Iff.mpr, Exists.intro, Filter.limsup_congr, Filter.eventually_atTop, OfNat.ofNat