awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
⊢ ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
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) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
⊢ ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
have h₁ : ∀ (n : ℕ) (a_vn' : a' < HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) (n_0 : 0 < n),
  a' * (↑n : EReal) ≤ (↑(v n) : EReal)
Tactic: filter_upwards [eventually_lt_of_lt_liminf a_v', eventually_gt_atTop 0] with n a_vn' n_0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
⊢ ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
have a_v'₁ : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
Tactic: replace a_v' : ∀ᶠ n : ℕ in atTop, a' * n ≤ v n := by
    filter_upwards [eventually_lt_of_lt_liminf a_v', eventually_gt_atTop 0] with n a_vn' n_0
    exact (le_div_iff_mul_le (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 a_vn'.le
Cleared hypotheses: a_v'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
⊢ ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
have neg : (∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)) → ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
Tactic: suffices h : (∀ᶠ n : ℕ in atTop, a' * n ≤ v n) → ∃ᶠ n : ℕ in atTop, a * b * n ≤ (u ∘ v) n
    from h a_v'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
⊢ (∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)) → ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
have neg : ∃ᶠ (x : ℕ) in atTop, a' * (↑x : EReal) ≤ (↑(v x) : EReal) → a * b * (↑x : EReal) ≤ (u ∘ v) x
Tactic: rw [← frequently_imp_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
⊢ ∃ᶠ (x : ℕ) in atTop, a' * (↑x : EReal) ≤ (↑(v x) : EReal) → a * b * (↑x : EReal) ≤ (u ∘ v) x
have b_u₁ : ∃ᶠ (x : ℕ) in atTop,
  (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
Tactic: replace b_u := ((frequently_mul_le b_u).and_eventually (eventually_gt_atTop 0)).and_eventually
    <| EReal.eventually_atTop_exists_nat_between a_a_inv' (inv_nonneg_of_nonneg a_0.le)
Cleared hypotheses: b_u
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
⊢ ∃ᶠ (x : ℕ) in atTop, a' * (↑x : EReal) ≤ (↑(v x) : EReal) → a * b * (↑x : EReal) ≤ (u ∘ v) x
have neg : ∀ (M : ℕ), ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1
Tactic: refine frequently_atTop.2 fun M ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M : ℕ
⊢ ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1
have neg : ∀ (M' : ℕ) (aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)),
  ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1
Tactic: obtain ⟨M', aM_M'⟩ := exists_nat_ge_mul a_top' M
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)
⊢ ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1
have neg : ∀ (n : ℕ) (n_M' : n ≥ M') (bn_un : b * (↑n : EReal) ≤ u n),
  0 < n →
    ∀ (k : ℕ) (an_k' : a'⁻¹ * (↑n : EReal) ≤ (↑k : EReal)) (k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)),
      ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1
Tactic: obtain ⟨n, n_M', ⟨bn_un, _⟩, k, an_k', k_an⟩ := frequently_atTop.1 b_u M'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
bn_un : b * (↑n : EReal) ≤ u n
right : 0 < n
k : ℕ
an_k' : a'⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
⊢ ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1
have neg : k ≥ M
Tactic: refine ⟨k, ?_, fun ak_vk' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
bn_un : b * (↑n : EReal) ≤ u n
right : 0 < n
k : ℕ
an_k' : a'⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
neg : k ≥ M
⊢ ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1
have neg₁ : ∀ (ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)), a * b * (↑k : EReal) ≤ (u ∘ v) k
Tactic: refine ⟨k, ?_, fun ak_vk' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
bn_un : b * (↑n : EReal) ≤ u n
right : 0 < n
k : ℕ
an_k' : a'⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
⊢ k ≥ M
have neg : ∀ (aM_M' : (↑M : EReal) ≤ a'⁻¹ * (↑M' : EReal)) (n : ℕ) (n_M' : n ≥ M') (bn_un : b * (↑n : EReal) ≤ u n),
  0 < n → ∀ (k : ℕ) (an_k' : a'⁻¹ * (↑n : EReal) ≤ (↑k : EReal)) (k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)), k ≥ M
Tactic: rw [mul_comm a', ← le_div_iff_mul_le a_0' a_top', EReal.div_eq_inv_mul] at aM_M'
Cleared hypotheses: aM_M', n, n_M', bn_un, right, k, an_k', k_an
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : (↑M : EReal) ≤ a'⁻¹ * (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
bn_un : b * (↑n : EReal) ≤ u n
right : 0 < n
k : ℕ
an_k' : a'⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
⊢ k ≥ M
have apply : a'⁻¹ * (↑M' : EReal) ≤ a'⁻¹ * (↑n : EReal)
Tactic: apply Nat.cast_le.1 <| aM_M'.trans <| an_k'.trans' _
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : (↑M : EReal) ≤ a'⁻¹ * (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
bn_un : b * (↑n : EReal) ≤ u n
right : 0 < n
k : ℕ
an_k' : a'⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
⊢ a'⁻¹ * (↑M' : EReal) ≤ a'⁻¹ * (↑n : EReal)
have ha : 0 ≤ a'⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
bn_un : b * (↑n : EReal) ≤ u n
right : 0 < n
k : ℕ
an_k' : a'⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
⊢ a * b * (↑k : EReal) ≤ (u ∘ v) k
have neg : b * (a * (↑k : EReal)) ≤ u (v k)
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
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
bn_un : b * (↑n : EReal) ≤ u n
right : 0 < n
k : ℕ
an_k' : a'⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
⊢ b * (a * (↑k : EReal)) ≤ u (v k)
have an_k'₁ : (↑n : EReal) ≤ a' * (↑k : EReal)
Tactic: rw [← EReal.div_eq_inv_mul, div_le_iff_le_mul a_0' a_top'] at an_k'
Cleared hypotheses: an_k', k_an, ak_vk'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
bn_un : b * (↑n : EReal) ≤ u n
right : 0 < n
k : ℕ
an_k' : (↑n : EReal) ≤ a' * (↑k : EReal)
k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
⊢ b * (a * (↑k : EReal)) ≤ u (v k)
have k_an₁ : a * (↑k : EReal) ≤ (↑n : EReal)
Tactic: rw [← EReal.div_eq_inv_mul, le_div_iff_mul_le a_0 (ne_top_of_lt a_a'), mul_comm] at k_an
Cleared hypotheses: k_an, ak_vk'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
bn_un : b * (↑n : EReal) ≤ u n
right : 0 < n
k : ℕ
an_k' : (↑n : EReal) ≤ a' * (↑k : EReal)
k_an : a * (↑k : EReal) ≤ (↑n : EReal)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
⊢ b * (a * (↑k : EReal)) ≤ u (v k)
have n_vk : n ≤ v k
Tactic: have n_vk := Nat.cast_le.1 (an_k'.trans ak_vk')
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
bn_un : b * (↑n : EReal) ≤ u n
right : 0 < n
k : ℕ
an_k' : (↑n : EReal) ≤ a' * (↑k : EReal)
k_an : a * (↑k : EReal) ≤ (↑n : EReal)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
n_vk : n ≤ v k
⊢ b * (a * (↑k : EReal)) ≤ b * (↑n : EReal)
have ha : 0 ≤ b
Tactic: gcongr
-- 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 ≠ ⊤
⊢ LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
have ha₁ : Ne (α := EReal) (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0
Tactic: rw [← hv.liminf_eq] at ha
Cleared hypotheses: ha, ha'
-- 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 ≠ ⊤
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf 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)
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf 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
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have pos : ∀ (u_0 : u = ⊥), linearGrowthInf (u ∘ v) = a * linearGrowthInf 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 = ⊥), linearGrowthInf (u ∘ v) = a * linearGrowthInf u
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have neg : ∀ (u_0 : ¬u = ⊥), linearGrowthInf (u ∘ v) = a * linearGrowthInf 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 = ⊥
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have pos : linearGrowthInf (⊥ ∘ v) = a * linearGrowthInf ⊥
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 ⊥
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have pos₁ : linearGrowthInf ⊥ = a * linearGrowthInf ⊥
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 ⊥
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
have pos₂ : ⊥ = a * ⊥
Tactic: rw [u_0, Pi.bot_comp, linearGrowthInf_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]