awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
⊢ ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
have neg : (∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)) → ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
Tactic: suffices h : (∀ᶠ n : ℕ in atTop, v n ≤ a' * n) → ∃ᶠ n : ℕ in atTop, (u ∘ v) n ≤ a * b * n
    from h v_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
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
⊢ (∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)) → ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * (↑n : EReal)
have neg : ∃ᶠ (x : ℕ) in atTop, (↑(v x) : EReal) ≤ a' * (↑x : EReal) → (u ∘ v) x ≤ a * b * (↑x : EReal)
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) (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
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
⊢ ∃ᶠ (x : ℕ) in atTop, (↑(v x) : EReal) ≤ a' * (↑x : EReal) → (u ∘ v) x ≤ a * b * (↑x : EReal)
have u_b₁ : ∃ᶠ (x : ℕ) in atTop,
  (u x ≤ b * (↑x : EReal) ∧ 0 < x) ∧ ∃ (m : ℕ), a⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a'⁻¹ * (↑x : EReal)
Tactic: replace u_b := ((frequently_le_mul u_b).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: 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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 0 < x) ∧ ∃ (m : ℕ), a⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a'⁻¹ * (↑x : EReal)
⊢ ∃ᶠ (x : ℕ) in atTop, (↑(v x) : EReal) ≤ a' * (↑x : EReal) → (u ∘ v) x ≤ a * b * (↑x : EReal)
have neg : ∀ (M : ℕ), ∃ b_1 ≥ M, (↑(v b_1) : EReal) ≤ a' * (↑b_1 : EReal) → (u ∘ v) b_1 ≤ a * b * (↑b_1 : EReal)
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) (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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 0 < x) ∧ ∃ (m : ℕ), a⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a'⁻¹ * (↑x : EReal)
M : ℕ
⊢ ∃ b_1 ≥ M, (↑(v b_1) : EReal) ≤ a' * (↑b_1 : EReal) → (u ∘ v) b_1 ≤ a * b * (↑b_1 : EReal)
have neg : ∀ (M' : ℕ) (aM_M' : a * (↑M : EReal) ≤ (↑M' : EReal)),
  ∃ b_1 ≥ M, (↑(v b_1) : EReal) ≤ a' * (↑b_1 : EReal) → (u ∘ v) b_1 ≤ a * b * (↑b_1 : EReal)
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) (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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 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, (↑(v b_1) : EReal) ≤ a' * (↑b_1 : EReal) → (u ∘ v) b_1 ≤ a * b * (↑b_1 : EReal)
have neg : ∀ (n : ℕ) (n_M' : n ≥ M') (un_bn : u n ≤ b * (↑n : EReal)),
  0 < n →
    ∀ (k : ℕ) (an_k : a⁻¹ * (↑n : EReal) ≤ (↑k : EReal)) (k_an' : (↑k : EReal) ≤ a'⁻¹ * (↑n : EReal)),
      ∃ b_1 ≥ M, (↑(v b_1) : EReal) ≤ a' * (↑b_1 : EReal) → (u ∘ v) b_1 ≤ a * b * (↑b_1 : EReal)
Tactic: obtain ⟨n, n_M', ⟨un_bn, _⟩, k, an_k, k_an'⟩ := frequently_atTop.1 u_b M'
-- 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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 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'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : a⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an' : (↑k : EReal) ≤ a'⁻¹ * (↑n : EReal)
⊢ ∃ b_1 ≥ M, (↑(v b_1) : EReal) ≤ a' * (↑b_1 : EReal) → (u ∘ v) b_1 ≤ a * b * (↑b_1 : EReal)
have neg : k ≥ M
Tactic: refine ⟨k, ?_, fun vk_ak' ↦ ?_⟩
-- 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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 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'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : a⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an' : (↑k : EReal) ≤ a'⁻¹ * (↑n : EReal)
neg : k ≥ M
⊢ ∃ b_1 ≥ M, (↑(v b_1) : EReal) ≤ a' * (↑b_1 : EReal) → (u ∘ v) b_1 ≤ a * b * (↑b_1 : EReal)
have neg₁ : ∀ (vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)), (u ∘ v) k ≤ a * b * (↑k : EReal)
Tactic: refine ⟨k, ?_, fun vk_ak' ↦ ?_⟩
-- 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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 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'
un_bn : u n ≤ b * (↑n : EReal)
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') (un_bn : u n ≤ b * (↑n : EReal)),
  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', un_bn, 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) (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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 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'
un_bn : u n ≤ b * (↑n : EReal)
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) (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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 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'
un_bn : u n ≤ b * (↑n : EReal)
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) (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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 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'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : a⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an' : (↑k : EReal) ≤ a'⁻¹ * (↑n : EReal)
vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)
⊢ (u ∘ v) k ≤ a * b * (↑k : EReal)
have neg : u (v k) ≤ b * (a * (↑k : 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
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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 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'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : a⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an' : (↑k : EReal) ≤ a'⁻¹ * (↑n : EReal)
vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)
⊢ u (v k) ≤ b * (a * (↑k : EReal))
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', vk_ak'
-- 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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 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'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : a⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an' : a' * (↑k : EReal) ≤ (↑n : EReal)
vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)
⊢ u (v k) ≤ b * (a * (↑k : EReal))
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', vk_ak'
-- 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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 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'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : (↑n : EReal) ≤ a * (↑k : EReal)
k_an' : a' * (↑k : EReal) ≤ (↑n : EReal)
vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)
⊢ u (v k) ≤ b * (a * (↑k : EReal))
have vk_n : v k ≤ n
Tactic: have vk_n := Nat.cast_le.1 (vk_ak'.trans k_an')
-- 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
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 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'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : (↑n : EReal) ≤ a * (↑k : EReal)
k_an' : a' * (↑k : EReal) ≤ (↑n : EReal)
vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)
vk_n : v k ≤ n
⊢ b * (↑n : EReal) ≤ b * (a * (↑k : EReal))
have ha : 0 ≤ b
Tactic: gcongr
-- 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
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
have v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
Tactic: have v_0 := hv.symm.lt_of_le (linearGrowthInf_natCast_nonneg 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))
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
have pos : ∀ (u_0 : u = ⊥), (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
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) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
pos : ∀ (u_0 : u = ⊥), (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
have neg : ∀ (u_0 : ¬u = ⊥), (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
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) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : u = ⊥
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
have pos : LE.le (α := EReal) ⊥ (linearGrowthSup (⊥ ∘ v))
Tactic: rw [u_0, linearGrowthSup_bot, mul_bot_of_pos v_0]
-- 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 = ⊥
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
have neg : ∀ (a' : EReal),
  Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a' →
    ∀ b' ∈ Set.Ioo 0 (linearGrowthSup u), a' * b' ≤ linearGrowthSup (u ∘ v)
Tactic: apply EReal.mul_le_of_forall_lt_of_nonneg v_0.le
    (linearGrowthSup_comp_nonneg h u_0 (tendsto_atTop_of_linearGrowthInf_natCast_pos hv))
-- 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
⊢ Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a →
    ∀ b' ∈ Set.Ioo 0 (linearGrowthSup u), a * b' ≤ linearGrowthSup (u ∘ v)
have neg : ∀ (a_0 : 0 < a) (a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)),
  ∀ b' ∈ Set.Ioo 0 (linearGrowthSup u), a * b' ≤ linearGrowthSup (u ∘ v)
Tactic: ⟨a_0, 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 ∈ Set.Ioo 0 (linearGrowthSup u) → a * b ≤ linearGrowthSup (u ∘ v)
have neg : ∀ (b_0 : 0 < b) (b_u : b < linearGrowthSup u), a * b ≤ linearGrowthSup (u ∘ v)
Tactic: ⟨b_0, 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
b_u : b < linearGrowthSup u
⊢ a * b ≤ linearGrowthSup (u ∘ v)
have neg : ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
Tactic: apply Frequently.le_linearGrowthSup
-- 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
⊢ ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
have neg : ∀ (a' : EReal) (a_a' : a < a') (a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)),
  ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
Tactic: obtain ⟨a', a_a', a_v'⟩ := exists_between a_v
-- 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)
⊢ ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
have a_top' : a' ≠ ⊤
Tactic: have a_top' := ne_top_of_lt a_v'
-- 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' ≠ ⊤
⊢ ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
have a_0' : 0 < a'
Tactic: have a_0' := a_0.trans a_a'