awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ (n : ℕ), u n ≤ 0
u_0' : linearGrowthInf u = 0
pos : linearGrowthInf (u ∘ v) = 0
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u

Tactic:
rw [u_0', mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ (n : ℕ), u n ≤ 0
u_0' : linearGrowthInf u = 0
apply : linearGrowthInf (u ∘ v) ≤ 0
⊢ linearGrowthInf (u ∘ v) = 0

Tactic:
apply le_antisymm _ (linearGrowthInf_comp_nonneg h u_0 v_top)

Premises used: le_antisymm, LinearGrowth.linearGrowthInf_comp_nonneg
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ (n : ℕ), u n ≤ 0
u_0' : linearGrowthInf u = 0
apply : Eq (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ 0) 0
⊢ linearGrowthInf (u ∘ v) ≤ 0

Tactic:
apply (linearGrowthInf_monotone fun n ↦ h' (v n)).trans_eq

Premises used: LE.le.trans_eq, LinearGrowth.linearGrowthInf_monotone
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ (n : ℕ), u n ≤ 0
u_0' : linearGrowthInf u = 0
⊢ Eq (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ 0) 0

Tactic:
linearGrowthInf_const zero_ne_bot zero_ne_top

Premises used: EReal.zero_ne_bot, LinearGrowth.linearGrowthInf_const, EReal.zero_ne_top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ (n : ℕ), u n ≤ 0
u_0' : linearGrowthInf u = 0
⊢ Eq (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ 0) 0

Tactic:
exact linearGrowthInf_const zero_ne_bot zero_ne_top

Premises used: EReal.zero_ne_bot, LinearGrowth.linearGrowthInf_const, EReal.zero_ne_top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 < u x
⊢ ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x

Tactic:
replace h' := h'.mono fun _ hn ↦ hn.le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x
neg : linearGrowthInf (u ∘ v) ≤ a * linearGrowthInf u
neg₁ : a * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x
neg :
  ∀ (ha : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0)
    (ha' : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊤)
    (hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop))
    (v_top : Tendsto v atTop atTop) (u_0 : ¬u = ⊥) (h' : ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x),
    linearGrowthInf (u ∘ v) ≤
      limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthInf u
⊢ linearGrowthInf (u ∘ v) ≤ a * linearGrowthInf u

Tactic:
rw [← hv.limsup_eq] at ha ha' ⊢

Premises used: Filter.Tendsto.limsup_eq
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0
ha' : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ linearGrowthInf (u ∘ v) ≤
    limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthInf u

Tactic:
h.linearGrowthInf_comp_le ha ha'

Premises used: LinearGrowth.linearGrowthSup, Monotone.linearGrowthInf_comp_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0
ha' : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ linearGrowthInf (u ∘ v) ≤
    limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthInf u

Tactic:
exact h.linearGrowthInf_comp_le ha ha'

Premises used: Monotone.linearGrowthInf_comp_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x
neg :
  liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthInf u ≤
    linearGrowthInf (u ∘ v)
⊢ a * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)

Tactic:
rw [← hv.liminf_eq]

Premises used: Filter.Tendsto.liminf_eq
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthInf u ≤
    linearGrowthInf (u ∘ v)

Tactic:
le_linearGrowthInf_comp h' v_top

Premises used: LinearGrowth.linearGrowthInf, LinearGrowth.le_linearGrowthInf_comp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthInf u ≤
    linearGrowthInf (u ∘ v)

Tactic:
exact le_linearGrowthInf_comp h' v_top

Premises used: LinearGrowth.le_linearGrowthInf_comp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
pos : ∀ (u_0 : u = ⊥), linearGrowthSup (u ∘ v) = a * linearGrowthSup u
neg : ∀ (u_0 : ¬u = ⊥), linearGrowthSup (u ∘ v) = a * linearGrowthSup u
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u

Tactic:
by_cases u_0 : u = ⊥
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : u = ⊥
pos : linearGrowthSup (⊥ ∘ v) = a * linearGrowthSup ⊥
pos₁ : linearGrowthSup ⊥ = a * linearGrowthSup ⊥
pos₂ : ⊥ = a * ⊥
pos₃ : ⊥ = HMul.hMul (α := EReal) (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊥
pos₄ pos₅ : Eq (α := EReal) ⊥ ⊥
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u

Tactic:
rw [u_0, Pi.bot_comp, linearGrowthSup_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]

Premises used: LinearGrowth.linearGrowthSup_bot, Pi.bot_comp, Filter.Tendsto.liminf_eq, EReal.mul_bot_of_pos
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
pos : ∀ (u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0), linearGrowthSup (u ∘ v) = a * linearGrowthSup u
neg : ∀ (u_1 : ∃ᶠ (x : ℕ) in atTop, 0 < u x), linearGrowthSup (u ∘ v) = a * linearGrowthSup u
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u

Tactic:
by_cases! u_1 : ∀ᶠ n : ℕ in atTop, u n ≤ 0

Premises used: Filter.atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0
apply : linearGrowthSup u ≤ 0
⊢ linearGrowthSup u = 0

Tactic:
apply le_antisymm _ (h.linearGrowthSup_nonneg u_0)

Premises used: le_antisymm, Monotone.linearGrowthSup_nonneg
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0
apply : Eq (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ 0) 0
⊢ linearGrowthSup u ≤ 0

Tactic:
apply (linearGrowthSup_eventually_monotone u_1).trans_eq

Premises used: LE.le.trans_eq, LinearGrowth.linearGrowthSup_eventually_monotone
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0
⊢ Eq (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ 0) 0

Tactic:
(linearGrowthSup_const zero_ne_bot zero_ne_top)

Premises used: EReal.zero_ne_bot, EReal.zero_ne_top, LinearGrowth.linearGrowthSup_const
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0
⊢ Eq (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ 0) 0

Tactic:
exact (linearGrowthSup_const zero_ne_bot zero_ne_top)

Premises used: EReal.zero_ne_bot, EReal.zero_ne_top, LinearGrowth.linearGrowthSup_const
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0
⊢ linearGrowthSup u = 0

Tactic:
have u_0' : linearGrowthSup u = 0 := by
      apply le_antisymm _ (h.linearGrowthSup_nonneg u_0)
      apply (linearGrowthSup_eventually_monotone u_1).trans_eq
      exact (linearGrowthSup_const zero_ne_bot zero_ne_top)
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0
u_0' : linearGrowthSup u = 0
pos : linearGrowthSup (u ∘ v) = 0
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u

Tactic:
rw [u_0', mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0
u_0' : linearGrowthSup u = 0
apply : linearGrowthSup (u ∘ v) ≤ 0
⊢ linearGrowthSup (u ∘ v) = 0

Tactic:
apply le_antisymm _ (linearGrowthSup_comp_nonneg h u_0 v_top)

Premises used: LinearGrowth.linearGrowthSup_comp_nonneg, le_antisymm
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0
u_0' : linearGrowthSup u = 0
apply : Eq (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ 0) 0
⊢ linearGrowthSup (u ∘ v) ≤ 0

Tactic:
apply (linearGrowthSup_eventually_monotone (v_top.eventually u_1)).trans_eq

Premises used: LE.le.trans_eq, LinearGrowth.linearGrowthSup_eventually_monotone, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0
u_0' : linearGrowthSup u = 0
⊢ Eq (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ 0) 0

Tactic:
linearGrowthSup_const zero_ne_bot zero_ne_top

Premises used: EReal.zero_ne_bot, EReal.zero_ne_top, LinearGrowth.linearGrowthSup_const
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0
u_0' : linearGrowthSup u = 0
⊢ Eq (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ 0) 0

Tactic:
exact linearGrowthSup_const zero_ne_bot zero_ne_top

Premises used: EReal.zero_ne_bot, EReal.zero_ne_top, LinearGrowth.linearGrowthSup_const
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∃ᶠ (x : ℕ) in atTop, 0 < u x
⊢ ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x

Tactic:
replace u_1 := u_1.mono fun x hx ↦ hx.le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x
neg : linearGrowthSup (u ∘ v) ≤ a * linearGrowthSup u
neg₁ : a * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x
neg :
  ∀ (ha : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0)
    (ha' : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊤)
    (hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop))
    (v_top : Tendsto v atTop atTop) (u_0 : ¬u = ⊥) (u_1 : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x),
    linearGrowthSup (u ∘ v) ≤
      limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthSup u
⊢ linearGrowthSup (u ∘ v) ≤ a * linearGrowthSup u

Tactic:
rw [← hv.limsup_eq] at ha ha' ⊢

Premises used: Filter.Tendsto.limsup_eq
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0
ha' : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ linearGrowthSup (u ∘ v) ≤
    limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthSup u

Tactic:
linearGrowthSup_comp_le u_1 ha ha' v_top

Premises used: LinearGrowth.linearGrowthSup, LinearGrowth.linearGrowthSup_comp_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0
ha' : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ linearGrowthSup (u ∘ v) ≤
    limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthSup u

Tactic:
exact linearGrowthSup_comp_le u_1 ha ha' v_top

Premises used: LinearGrowth.linearGrowthSup_comp_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x
neg :
  liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthSup u ≤
    linearGrowthSup (u ∘ v)
⊢ a * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)

Tactic:
rw [← hv.liminf_eq]

Premises used: Filter.Tendsto.liminf_eq
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthSup u ≤
    linearGrowthSup (u ∘ v)

Tactic:
h.le_linearGrowthSup_comp hv₁.ne.symm

Premises used: Ne.symm, LinearGrowth.linearGrowthInf, Monotone.le_linearGrowthSup_comp, LT.lt.ne
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
u_1 : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthSup u ≤
    linearGrowthSup (u ∘ v)

Tactic:
exact h.le_linearGrowthSup_comp hv₁.ne.symm

Premises used: Ne.symm, Monotone.le_linearGrowthSup_comp, LT.lt.ne
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
⊢ Tendsto (β := EReal) (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(m * n) : EReal) (↑n : EReal)) atTop (𝓝 (↑m : EReal))

Tactic:
tendsto_nhds_of_eventually_eq ((eventually_gt_atTop 0).mono fun x hx ↦ ?_)

Premises used: Filter.Eventually.mono, tendsto_nhds_of_eventually_eq, OfNat.ofNat, Filter.eventually_gt_atTop