awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
refine :
  ∀ (a : EReal) (v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) (b : EReal) (u_b : b > linearGrowthSup u),
    ∀ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
⊢ ∀ a' > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal), ∀ b' > linearGrowthSup u, linearGrowthSup (u ∘ v) ≤ a' * b'

Tactic:
refine fun a v_a b u_b ↦ Eventually.linearGrowthSup_le ?_

Premises used: Eventually.linearGrowthSup_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthSup u
rw : (linearGrowthInf fun (x : ℕ) ↦ 0) ≤ b
⊢ 0 ≤ b

Tactic:
rw [← 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 : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthSup u
⊢ (linearGrowthInf fun (x : ℕ) ↦ 0) ≤ b

Tactic:
(linearGrowthInf_le_linearGrowthSup_of_frequently_le hu).trans u_b.le

Premises used: LT.lt.le, LE.le.trans, LinearGrowth.linearGrowthInf_le_linearGrowthSup_of_frequently_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthSup u
⊢ (linearGrowthInf fun (x : ℕ) ↦ 0) ≤ b

Tactic:
exact (linearGrowthInf_le_linearGrowthSup_of_frequently_le hu).trans u_b.le

Premises used: LT.lt.le, LE.le.trans, LinearGrowth.linearGrowthInf_le_linearGrowthSup_of_frequently_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthSup u
⊢ 0 ≤ b

Tactic:
have b_0 : 0 ≤ b := by
    rw [← linearGrowthInf_const zero_ne_bot zero_ne_top]
    exact (linearGrowthInf_le_linearGrowthSup_of_frequently_le hu).trans u_b.le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
⊢ ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * (↑(v n) : EReal)

Tactic:
have uv_b : ∀ᶠ n in atTop, u (v n) ≤ b * v n :=
    eventually_map.1 ((eventually_le_mul u_b).filter_mono hv₂)
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
uv_b : ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * (↑(v n) : EReal)
h :
  ∀ (n : ℕ) (uvn_b : u (v n) ≤ b * (↑(v n) : EReal)) (vn_a : HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal) < a)
    (n_0 : 0 < n), (u ∘ v) n ≤ a * b * (↑n : EReal)
⊢ ∀ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)

Tactic:
filter_upwards [uv_b, eventually_lt_of_limsup_lt v_a, eventually_gt_atTop 0]
    with n uvn_b vn_a n_0

Premises used: Filter.eventually_lt_of_limsup_lt, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
uv_b : ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * (↑(v n) : EReal)
n : ℕ
uvn_b : u (v n) ≤ b * (↑(v n) : EReal)
vn_a : HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal) < a
n_0 : 0 < n
⊢ (↑(v n) : EReal) ≤ a * (↑n : EReal)

Tactic:
replace vn_a := ((div_lt_iff (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 vn_a).le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
uv_b : ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * (↑(v n) : EReal)
n : ℕ
uvn_b : u (v n) ≤ b * (↑(v n) : EReal)
n_0 : 0 < n
vn_a : (↑(v n) : EReal) ≤ a * (↑n : EReal)
h : u (v n) ≤ b * (a * (↑n : EReal))
⊢ (u ∘ v) n ≤ a * b * (↑n : EReal)

Tactic:
rw [comp_apply, mul_comm a b, mul_assoc b a]

Premises used: mul_assoc, mul_comm, Function.comp_apply
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
uv_b : ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * (↑(v n) : EReal)
n : ℕ
uvn_b : u (v n) ≤ b * (↑(v n) : EReal)
n_0 : 0 < n
vn_a : (↑(v n) : EReal) ≤ a * (↑n : EReal)
ha : 0 ≤ b
⊢ b * (↑(v n) : EReal) ≤ b * (a * (↑n : EReal))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
uv_b : ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * (↑(v n) : EReal)
n : ℕ
uvn_b : u (v n) ≤ b * (↑(v n) : EReal)
n_0 : 0 < n
vn_a : (↑(v n) : EReal) ≤ a * (↑n : EReal)
⊢ u (v n) ≤ b * (a * (↑n : EReal))

Tactic:
exact uvn_b.trans <| by gcongr

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
h' : u ≠ ⊥
⊢ ∃ (x : ℕ), ¬u x = ⊥ x

Tactic:
simp only [ne_eq, funext_iff, not_forall] at h'

Premises used: funext_iff, ne_eq, Classical.not_forall
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
h' : ∃ (x : ℕ), ¬u x = ⊥ x
obtain : ∀ (m : ℕ) (hm : ¬u m = ⊥ m), 0 ≤ linearGrowthInf u
⊢ 0 ≤ linearGrowthInf u

Tactic:
obtain ⟨m, hm⟩ := h'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
⊢ ∀ᶠ (n : ℕ) in atTop, u m ≤ u n

Tactic:
have m_n : ∀ᶠ n in atTop, u m ≤ u n := eventually_atTop.2 ⟨m, fun _ hb ↦ h hb⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, u m ≤ u n
inl : ∀ (hm' : u m = ⊤), 0 ≤ linearGrowthInf u
inr : ∀ (hm' : u m ≠ ⊤), 0 ≤ linearGrowthInf u
⊢ 0 ≤ linearGrowthInf u

Tactic:
rcases eq_or_ne (u m) ⊤ with hm' | hm'

Premises used: eq_or_ne, Top.top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, u m ≤ u n
hm' : u m = ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ⊤ ≤ u n

Tactic:
rw [hm'] at m_n
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, u m ≤ u n
hm' : u m = ⊤
m_n₁ : ∀ᶠ (n : ℕ) in atTop, ⊤ ≤ u n
⊢ u m = ⊤

Tactic:
rw [hm'] at m_n
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, ⊤ ≤ u n
hm' : u m = ⊤
⊢ 0 ≤ linearGrowthInf u

Tactic:
le_top.trans (linearGrowthInf_top.symm.trans_le (linearGrowthInf_eventually_monotone m_n))

Premises used: LinearGrowth.linearGrowthInf_top, Eq.trans_le, LinearGrowth.linearGrowthInf_eventually_monotone, le_top, LE.le.trans, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, ⊤ ≤ u n
hm' : u m = ⊤
⊢ 0 ≤ linearGrowthInf u

Tactic:
exact le_top.trans (linearGrowthInf_top.symm.trans_le (linearGrowthInf_eventually_monotone m_n))

Premises used: LinearGrowth.linearGrowthInf_top, Eq.trans_le, LinearGrowth.linearGrowthInf_eventually_monotone, le_top, LE.le.trans, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, u m ≤ u n
hm' : u m ≠ ⊤
inr : (linearGrowthInf fun (x : ℕ) ↦ u m) ≤ linearGrowthInf u
⊢ 0 ≤ linearGrowthInf u

Tactic:
rw [← linearGrowthInf_const hm hm']

Premises used: LinearGrowth.linearGrowthInf_const
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, u m ≤ u n
hm' : u m ≠ ⊤
⊢ (linearGrowthInf fun (x : ℕ) ↦ u m) ≤ linearGrowthInf u

Tactic:
linearGrowthInf_eventually_monotone m_n

Premises used: LinearGrowth.linearGrowthInf_eventually_monotone
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, u m ≤ u n
hm' : u m ≠ ⊤
⊢ (linearGrowthInf fun (x : ℕ) ↦ u m) ≤ linearGrowthInf u

Tactic:
exact linearGrowthInf_eventually_monotone m_n

Premises used: LinearGrowth.linearGrowthInf_eventually_monotone
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : Monotone u
h' : u ≠ ⊥
⊢ 0 ≤ linearGrowthSup u

Tactic:
(h.linearGrowthInf_nonneg h').trans (linearGrowthInf_le_linearGrowthSup)

Premises used: LinearGrowth.linearGrowthInf_le_linearGrowthSup, Monotone.linearGrowthInf_nonneg, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
h' : u ≠ ⊥
hv : Tendsto v atTop atTop
⊢ ∃ (x : ℕ), ¬u x = ⊥ x

Tactic:
simp only [ne_eq, funext_iff, not_forall] at h'

Premises used: funext_iff, ne_eq, Classical.not_forall
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
h' : ∃ (x : ℕ), ¬u x = ⊥ x
obtain : ∀ (m : ℕ) (hum : ¬u m = ⊥ m), 0 ≤ linearGrowthInf (u ∘ v)
⊢ 0 ≤ linearGrowthInf (u ∘ v)

Tactic:
obtain ⟨m, hum⟩ := h'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
⊢ ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n

Tactic:
have um_uvn : ∀ᶠ n in atTop, u m ≤ (u ∘ v) n :=
    (eventually_atTop.2 ⟨m, fun n m_n ↦ h m_n⟩).filter_mono hv
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
apply : LE.le (α := EReal) 0 (linearGrowthInf fun (x : ℕ) ↦ u m)
⊢ 0 ≤ linearGrowthInf (u ∘ v)

Tactic:
apply (linearGrowthInf_eventually_monotone um_uvn).trans'

Premises used: LinearGrowth.linearGrowthInf_eventually_monotone, LE.le.trans'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
inl : ∀ (hum' : u m = ⊤), LE.le (α := EReal) 0 (linearGrowthInf fun (x : ℕ) ↦ u m)
inr : ∀ (hum' : u m ≠ ⊤), LE.le (α := EReal) 0 (linearGrowthInf fun (x : ℕ) ↦ u m)
⊢ LE.le (α := EReal) 0 (linearGrowthInf fun (x : ℕ) ↦ u m)

Tactic:
rcases eq_or_ne (u m) ⊤ with hum' | hum'

Premises used: eq_or_ne, Top.top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
hum' : u m = ⊤
inl : LE.le (α := EReal) 0 ⊤
⊢ LE.le (α := EReal) 0 (linearGrowthInf fun (x : ℕ) ↦ u m)

Tactic:
rw [hum', ← Pi.top_def, linearGrowthInf_top]

Premises used: LinearGrowth.linearGrowthInf_top, Pi.top_def
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
hum' : u m = ⊤
⊢ LE.le (α := EReal) 0 ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
hum' : u m = ⊤
⊢ LE.le (α := EReal) 0 ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
hum' : u m ≠ ⊤
inr inr₁ : LE.le (α := EReal) 0 0
⊢ LE.le (α := EReal) 0 (linearGrowthInf fun (x : ℕ) ↦ u m)

Tactic:
rw [linearGrowthInf_const hum hum']

Premises used: LinearGrowth.linearGrowthInf_const
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
h' : u ≠ ⊥
hv : Tendsto v atTop atTop
⊢ 0 ≤ linearGrowthSup (u ∘ v)

Tactic:
(linearGrowthInf_comp_nonneg h h' hv).trans linearGrowthInf_le_linearGrowthSup

Premises used: LinearGrowth.linearGrowthInf_le_linearGrowthSup, LinearGrowth.linearGrowthInf_comp_nonneg, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
pos : ∀ (u_0 : u = ⊥), linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u
neg : ∀ (u_0 : ¬u = ⊥), linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u

Tactic:
by_cases u_0 : u = ⊥
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : u = ⊥
pos : ⊥ ≤ HMul.hMul (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊥
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u

Tactic:
rw [u_0, Pi.bot_comp, linearGrowthInf_bot]

Premises used: LinearGrowth.linearGrowthInf_bot, Pi.bot_comp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : u = ⊥
⊢ ⊥ ≤ HMul.hMul (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊥

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : u = ⊥
⊢ ⊥ ≤ HMul.hMul (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊥

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
⊢ LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))

Tactic:
have v_0 := hv₀.symm.lt_of_le <| (linearGrowthInf_natCast_nonneg v).trans (liminf_le_limsup)
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u

Tactic:
le_mul_of_forall_lt (.inl v_0) (.inl hv₁) fun a v_a b u_b ↦ ?_

Premises used: EReal.le_mul_of_forall_lt, Or.inl
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
neg :
  ∀ (a : EReal) (v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) (b : EReal) (u_b : b > linearGrowthInf u),
    linearGrowthInf (u ∘ v) ≤ a * b
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u

Tactic:
refine le_mul_of_forall_lt (.inl v_0) (.inl hv₁) fun a v_a b u_b ↦ ?_

Premises used: EReal.le_mul_of_forall_lt, Or.inl
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthInf u
⊢ 0 < a

Tactic:
have a_0 := v_0.trans v_a
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
⊢ 0 < b

Tactic:
have b_0 := (h.linearGrowthInf_nonneg u_0).trans_lt u_b
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
neg :
  ∀ (v_a : GT.gt (α := EReal) ⊤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))) (a_0 : LT.lt (α := EReal) 0 ⊤),
    linearGrowthInf (u ∘ v) ≤ ⊤ * b
neg₁ : ∀ (a_top : a ≠ ⊤), linearGrowthInf (u ∘ v) ≤ a * b
⊢ linearGrowthInf (u ∘ v) ≤ a * b

Tactic:
rcases eq_or_ne a ⊤ with rfl | a_top

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
b : EReal
u_b : b > linearGrowthInf u
b_0 : 0 < b
v_a : GT.gt (α := EReal) ⊤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a_0 : LT.lt (α := EReal) 0 ⊤
neg : linearGrowthInf (u ∘ v) ≤ ⊤
⊢ linearGrowthInf (u ∘ v) ≤ ⊤ * b

Tactic:
rw [top_mul_of_pos b_0]

Premises used: EReal.top_mul_of_pos
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
b : EReal
u_b : b > linearGrowthInf u
b_0 : 0 < b
v_a : GT.gt (α := EReal) ⊤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a_0 : LT.lt (α := EReal) 0 ⊤
⊢ linearGrowthInf (u ∘ v) ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
b : EReal
u_b : b > linearGrowthInf u
b_0 : 0 < b
v_a : GT.gt (α := EReal) ⊤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a_0 : LT.lt (α := EReal) 0 ⊤
⊢ linearGrowthInf (u ∘ v) ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
neg : ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
⊢ linearGrowthInf (u ∘ v) ≤ a * b

Tactic:
apply Frequently.linearGrowthInf_le

Premises used: Frequently.linearGrowthInf_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
neg :
  ∀ (a' : EReal) (v_a' : (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) < a') (a_a' : a' < a),
    ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
⊢ ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)

Tactic:
obtain ⟨a', v_a', a_a'⟩ := exists_between v_a

Premises used: exists_between