awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 : linearGrowthInf (⊥ ∘ v) = a * linearGrowthInf ⊥
pos₁ : linearGrowthInf ⊥ = a * linearGrowthInf ⊥
pos₂ : ⊥ = a * ⊥
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have pos₃ : ⊥ = HMul.hMul (α := EReal) (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊥
Tactic: rw [u_0, Pi.bot_comp, linearGrowthInf_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 : linearGrowthInf (⊥ ∘ v) = a * linearGrowthInf ⊥
pos₁ : linearGrowthInf ⊥ = a * linearGrowthInf ⊥
pos₂ : ⊥ = a * ⊥
pos₃ : ⊥ = HMul.hMul (α := EReal) (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊥
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have pos₄ : Eq (α := EReal) ⊥ ⊥
Tactic: rw [u_0, Pi.bot_comp, linearGrowthInf_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 = ⊥
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have pos : ∀ (h' : ∃ᶠ (n : ℕ) in atTop, u n ≤ 0), linearGrowthInf (u ∘ v) = a * linearGrowthInf u
Tactic: by_cases! h' : ∃ᶠ n : ℕ in atTop, u n ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 : ∀ (h' : ∃ᶠ (n : ℕ) in atTop, u n ≤ 0), linearGrowthInf (u ∘ v) = a * linearGrowthInf u
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have neg : ∀ (h' : ∀ᶠ (x : ℕ) in atTop, 0 < u x), linearGrowthInf (u ∘ v) = a * linearGrowthInf u
Tactic: by_cases! h' : ∃ᶠ n : ℕ in atTop, u n ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 : ℕ) in atTop, u n ≤ 0
n : ℕ
⊢ u n ≤ 0
have obtain : ∀ (m : ℕ) (n_m : m ≥ n) (um_1 : u m ≤ 0), u n ≤ 0
Tactic: obtain ⟨m, n_m, um_1⟩ := (frequently_atTop.1 h') n
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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 : ℕ) in atTop, u n ≤ 0
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have h'₁ : ∀ (n : ℕ), u n ≤ 0
Tactic: replace h' (n : ℕ) : u n ≤ 0 := by
      obtain ⟨m, n_m, um_1⟩ := (frequently_atTop.1 h') n
      exact (h n_m).trans um_1
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthInf u = 0
have apply : linearGrowthInf u ≤ 0
Tactic: apply le_antisymm _ (h.linearGrowthInf_nonneg u_0)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have u_0' : linearGrowthInf u = 0
Tactic: have u_0' : linearGrowthInf u = 0 := by
      apply le_antisymm _ (h.linearGrowthInf_nonneg u_0)
      exact (linearGrowthInf_monotone h').trans_eq (linearGrowthInf_const zero_ne_bot zero_ne_top)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have pos : linearGrowthInf (u ∘ v) = 0
Tactic: rw [u_0', mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthInf (u ∘ v) = 0
have apply : linearGrowthInf (u ∘ v) ≤ 0
Tactic: apply le_antisymm _ (linearGrowthInf_comp_nonneg h u_0 v_top)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthInf (u ∘ v) ≤ 0
have apply : Eq (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ 0) 0
Tactic: apply (linearGrowthInf_monotone fun n ↦ h' (v n)).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have h'₁ : ∀ᶠ (x : ℕ) in atTop, 0 ≤ u x
Tactic: replace h' := h'.mono fun _ hn ↦ hn.le
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have neg : linearGrowthInf (u ∘ v) ≤ a * linearGrowthInf u
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have neg₁ : a * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthInf (u ∘ v) ≤ a * linearGrowthInf u
have 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
Tactic: rw [← hv.limsup_eq] at ha ha' ⊢
Cleared hypotheses: ha, ha', hv₁, v_top, u_0, h'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ a * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)
have neg : liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthInf u ≤
  linearGrowthInf (u ∘ v)
Tactic: rw [← hv.liminf_eq]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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 ≠ ⊤
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
Tactic: have hv₁ : 0 < liminf (fun n ↦ (v n : EReal) / n) atTop := by
    rw [← hv.liminf_eq] at ha
    exact ha.symm.lt_of_le (linearGrowthInf_natCast_nonneg v)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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)
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have v_top : Tendsto v atTop atTop
Tactic: have v_top := tendsto_atTop_of_linearGrowthInf_natCast_pos hv₁.ne.symm
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have pos : ∀ (u_0 : u = ⊥), linearGrowthSup (u ∘ v) = a * linearGrowthSup u
Tactic: by_cases u_0 : u = ⊥
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have neg : ∀ (u_0 : ¬u = ⊥), linearGrowthSup (u ∘ v) = a * linearGrowthSup u
Tactic: by_cases u_0 : u = ⊥
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 = ⊥
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have pos : linearGrowthSup (⊥ ∘ v) = a * linearGrowthSup ⊥
Tactic: rw [u_0, Pi.bot_comp, linearGrowthSup_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 ⊥
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have pos₁ : linearGrowthSup ⊥ = a * linearGrowthSup ⊥
Tactic: rw [u_0, Pi.bot_comp, linearGrowthSup_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 ⊥
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have pos₂ : ⊥ = a * ⊥
Tactic: rw [u_0, Pi.bot_comp, linearGrowthSup_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 * ⊥
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have pos₃ : ⊥ = HMul.hMul (α := EReal) (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊥
Tactic: rw [u_0, Pi.bot_comp, linearGrowthSup_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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) ⊥
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have pos₄ : Eq (α := EReal) ⊥ ⊥
Tactic: rw [u_0, Pi.bot_comp, linearGrowthSup_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 = ⊥
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have pos : ∀ (u_1 : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0), linearGrowthSup (u ∘ v) = a * linearGrowthSup u
Tactic: by_cases! u_1 : ∀ᶠ n : ℕ in atTop, u n ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have neg : ∀ (u_1 : ∃ᶠ (x : ℕ) in atTop, 0 < u x), linearGrowthSup (u ∘ v) = a * linearGrowthSup u
Tactic: by_cases! u_1 : ∀ᶠ n : ℕ in atTop, u n ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
have apply : linearGrowthSup u ≤ 0
Tactic: apply le_antisymm _ (h.linearGrowthSup_nonneg u_0)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
have apply : Eq (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ 0) 0
Tactic: apply (linearGrowthSup_eventually_monotone u_1).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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 ∘ v) = a * linearGrowthSup u
have u_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)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have pos : linearGrowthSup (u ∘ v) = 0
Tactic: rw [u_0', mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthSup (u ∘ v) = 0
have apply : linearGrowthSup (u ∘ v) ≤ 0
Tactic: apply le_antisymm _ (linearGrowthSup_comp_nonneg h u_0 v_top)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthSup (u ∘ v) ≤ 0
have apply : Eq (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ 0) 0
Tactic: apply (linearGrowthSup_eventually_monotone (v_top.eventually u_1)).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have u_1₁ : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x
Tactic: replace u_1 := u_1.mono fun x hx ↦ hx.le
Cleared hypotheses: u_1
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have neg : linearGrowthSup (u ∘ v) ≤ a * linearGrowthSup u
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
have neg₁ : a * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
Tactic: apply le_antisymm