awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
h : Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a
b : EReal
h_1 : b ∈ Set.Ioo 0 (linearGrowthInf u)
left : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * (↑(v a) : EReal) ≤ u (v a)
n : ℕ
b_uvn : b * (↑(v n) : EReal) ≤ u (v n)
n_0 : 0 < n
a_vn : a * (↑n : EReal) ≤ (↑(v n) : EReal)
⊢ b * (a * (↑n : EReal)) ≤ b * (↑(v n) : EReal)
have ha : 0 ≤ b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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
⊢ linearGrowthSup (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u
have v_0 : 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)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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))
⊢ linearGrowthSup (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u
have refine : ∀ a' > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal), ∀ b' > linearGrowthSup u, linearGrowthSup (u ∘ v) ≤ a' * b'
Tactic: refine le_mul_of_forall_lt (.inl v_0) (.inl hv₁) ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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' > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal), ∀ b' > linearGrowthSup u, linearGrowthSup (u ∘ v) ≤ a' * b'
have 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)
Tactic: refine fun a v_a b u_b ↦ Eventually.linearGrowthSup_le ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
have rw : (linearGrowthInf fun (x : ℕ) ↦ 0) ≤ b
Tactic: rw [← linearGrowthInf_const zero_ne_bot zero_ne_top]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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
⊢ ∀ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
have b_0 : 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
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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 ≤ a * b * (↑n : EReal)
have uv_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₂)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
have 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)
Tactic: filter_upwards [uv_b, eventually_lt_of_limsup_lt v_a, eventually_gt_atTop 0]
    with n uvn_b vn_a n_0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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
⊢ (u ∘ v) n ≤ a * b * (↑n : EReal)
have vn_a₁ : (↑(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
Cleared hypotheses: vn_a
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 ≤ a * b * (↑n : EReal)
have h : u (v n) ≤ b * (a * (↑n : EReal))
Tactic: rw [comp_apply, mul_comm a b, mul_assoc b a]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
h : Monotone u
h' : u ≠ ⊥
⊢ 0 ≤ linearGrowthInf u
have h'₁ : ∃ (x : ℕ), ¬u x = ⊥ x
Tactic: simp only [ne_eq, funext_iff, not_forall] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
h : Monotone u
h' : ∃ (x : ℕ), ¬u x = ⊥ x
⊢ 0 ≤ linearGrowthInf u
have obtain : ∀ (m : ℕ) (hm : ¬u m = ⊥ m), 0 ≤ linearGrowthInf u
Tactic: obtain ⟨m, hm⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
⊢ 0 ≤ linearGrowthInf u
have m_n : ∀ᶠ (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⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, u m ≤ u n
⊢ 0 ≤ linearGrowthInf u
have inl : ∀ (hm' : u m = ⊤), 0 ≤ linearGrowthInf u
Tactic: rcases eq_or_ne (u m) ⊤ with hm' | hm'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ 0 ≤ linearGrowthInf u
have inr : ∀ (hm' : u m ≠ ⊤), 0 ≤ linearGrowthInf u
Tactic: rcases eq_or_ne (u m) ⊤ with hm' | hm'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, u m ≤ u n
hm' : u m = ⊤
⊢ 0 ≤ linearGrowthInf u
have m_n₁ : ∀ᶠ (n : ℕ) in atTop, ⊤ ≤ u n
Tactic: rw [hm'] at m_n
Cleared hypotheses: m_n, hm'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
h : Monotone u
m : ℕ
hm : ¬u m = ⊥ m
m_n : ∀ᶠ (n : ℕ) in atTop, u m ≤ u n
hm' : u m ≠ ⊤
⊢ 0 ≤ linearGrowthInf u
have inr : (linearGrowthInf fun (x : ℕ) ↦ u m) ≤ linearGrowthInf u
Tactic: rw [← linearGrowthInf_const hm hm']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
h' : u ≠ ⊥
hv : Tendsto v atTop atTop
⊢ 0 ≤ linearGrowthInf (u ∘ v)
have h'₁ : ∃ (x : ℕ), ¬u x = ⊥ x
Tactic: simp only [ne_eq, funext_iff, not_forall] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
h' : ∃ (x : ℕ), ¬u x = ⊥ x
⊢ 0 ≤ linearGrowthInf (u ∘ v)
have obtain : ∀ (m : ℕ) (hum : ¬u m = ⊥ m), 0 ≤ linearGrowthInf (u ∘ v)
Tactic: obtain ⟨m, hum⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
⊢ 0 ≤ linearGrowthInf (u ∘ v)
have um_uvn : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ 0 ≤ linearGrowthInf (u ∘ v)
have apply : LE.le (α := EReal) 0 (linearGrowthInf fun (x : ℕ) ↦ u m)
Tactic: apply (linearGrowthInf_eventually_monotone um_uvn).trans'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ LE.le (α := EReal) 0 (linearGrowthInf fun (x : ℕ) ↦ u m)
have inl : ∀ (hum' : u m = ⊤), LE.le (α := EReal) 0 (linearGrowthInf fun (x : ℕ) ↦ u m)
Tactic: rcases eq_or_ne (u m) ⊤ with hum' | hum'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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)
⊢ LE.le (α := EReal) 0 (linearGrowthInf fun (x : ℕ) ↦ u m)
have inr : ∀ (hum' : u m ≠ ⊤), LE.le (α := EReal) 0 (linearGrowthInf fun (x : ℕ) ↦ u m)
Tactic: rcases eq_or_ne (u m) ⊤ with hum' | hum'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 (linearGrowthInf fun (x : ℕ) ↦ u m)
have inl : LE.le (α := EReal) 0 ⊤
Tactic: rw [hum', ← Pi.top_def, linearGrowthInf_top]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 (linearGrowthInf fun (x : ℕ) ↦ u m)
have inr : LE.le (α := EReal) 0 0
Tactic: rw [linearGrowthInf_const hum hum']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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)) ⊤
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u
have pos : ∀ (u_0 : u = ⊥), linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u
Tactic: by_cases u_0 : u = ⊥
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u
have neg : ∀ (u_0 : ¬u = ⊥), linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u
Tactic: by_cases u_0 : u = ⊥
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 = ⊥
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u
have pos : ⊥ ≤ HMul.hMul (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊥
Tactic: rw [u_0, Pi.bot_comp, linearGrowthInf_bot]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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 = ⊥
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u
have v_0 : 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)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
have neg : ∀ (a : EReal) (v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) (b : EReal) (u_b : b > linearGrowthInf u),
  linearGrowthInf (u ∘ v) ≤ a * b
Tactic: refine le_mul_of_forall_lt (.inl v_0) (.inl hv₁) fun a v_a b u_b ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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
⊢ linearGrowthInf (u ∘ v) ≤ a * b
have a_0 : 0 < a
Tactic: have a_0 := v_0.trans v_a
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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
⊢ linearGrowthInf (u ∘ v) ≤ a * b
have b_0 : 0 < b
Tactic: have b_0 := (h.linearGrowthInf_nonneg u_0).trans_lt u_b
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthInf (u ∘ v) ≤ a * b
have neg : ∀ (v_a : GT.gt (α := EReal) ⊤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))) (a_0 : LT.lt (α := EReal) 0 ⊤),
  linearGrowthInf (u ∘ v) ≤ ⊤ * b
Tactic: rcases eq_or_ne a ⊤ with rfl | a_top
Cleared hypotheses: a, v_a, a_0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ linearGrowthInf (u ∘ v) ≤ a * b
have neg₁ : ∀ (a_top : a ≠ ⊤), linearGrowthInf (u ∘ v) ≤ a * b
Tactic: rcases eq_or_ne a ⊤ with rfl | a_top
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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) ≤ ⊤ * b
have neg : linearGrowthInf (u ∘ v) ≤ ⊤
Tactic: rw [top_mul_of_pos b_0]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 ≠ ⊤
⊢ linearGrowthInf (u ∘ v) ≤ a * b
have neg : ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
Tactic: apply Frequently.linearGrowthInf_le
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 ≠ ⊤
⊢ ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
have 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)
Tactic: obtain ⟨a', v_a', a_a'⟩ := exists_between v_a
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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 ≠ ⊤
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)
have a_0' : 0 < a'
Tactic: have a_0' := v_0.trans v_a'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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 ≠ ⊤
a' : EReal
v_a' : (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) < a'
a_a' : a' < a
a_0' : 0 < a'
⊢ ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
have a_a_inv' : a⁻¹ < a'⁻¹
Tactic: have a_a_inv' : a⁻¹ < a'⁻¹ := inv_strictAntiOn (Set.mem_Ioi.2 a_0') (Set.mem_Ioi.2 a_0) a_a'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 ≠ ⊤
a' : EReal
v_a' : (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) < a'
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
⊢ ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
have h₁ : ∀ (n : ℕ) (vn_a' : HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal) < a') (n_0 : 0 < n),
  (↑(v n) : EReal) ≤ a' * (↑n : EReal)
Tactic: filter_upwards [eventually_lt_of_limsup_lt v_a', eventually_gt_atTop 0] with n vn_a' n_0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 ≠ ⊤
a' : EReal
v_a' : (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) < a'
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
n : ℕ
vn_a' : HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal) < a'
n_0 : 0 < n
⊢ (↑(v n) : EReal) ≤ a' * (↑n : EReal)
have h₁ : (↑(v n) : EReal) ≤ (↑n : EReal) * a'
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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 ≠ ⊤
a' : EReal
v_a' : (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) < a'
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
⊢ ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
have v_a'₁ : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
Tactic: replace v_a' : ∀ᶠ n : ℕ in atTop, v n ≤ a' * n := by
    filter_upwards [eventually_lt_of_limsup_lt v_a', eventually_gt_atTop 0] with n vn_a' n_0
    rw [mul_comm]
    exact (div_le_iff_le_mul (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 vn_a'.le
Cleared hypotheses: v_a'