awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
v_a' : (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) < a'
a_a' : a' < a
⊢ 0 < a'

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

Tactic:
have a_a_inv' : a⁻¹ < a'⁻¹ := inv_strictAntiOn (Set.mem_Ioi.2 a_0') (Set.mem_Ioi.2 a_0) a_a'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
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'⁻¹
h₁ :
  ∀ (n : ℕ) (vn_a' : HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal) < a') (n_0 : 0 < n),
    (↑(v n) : EReal) ≤ a' * (↑n : EReal)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑(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

Premises used: Filter.eventually_lt_of_limsup_lt, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
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
h₁ : (↑(v n) : EReal) ≤ (↑n : EReal) * a'
⊢ (↑(v n) : EReal) ≤ a' * (↑n : EReal)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
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) ≤ (↑n : EReal) * a'

Tactic:
(div_le_iff_le_mul (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 vn_a'.le

Premises used: Iff.mpr, LT.lt.le, Iff.mp, EReal.natCast_ne_top, EReal.div_le_iff_le_mul, Nat.cast_pos'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
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) ≤ (↑n : EReal) * a'

Tactic:
exact (div_le_iff_le_mul (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 vn_a'.le

Premises used: Iff.mpr, LT.lt.le, Iff.mp, EReal.natCast_ne_top, EReal.div_le_iff_le_mul, Nat.cast_pos'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
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)

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

Tactic:
rw [← frequently_imp_distrib]

Premises used: Filter.frequently_imp_distrib
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
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,
    (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)
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
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)

Tactic:
frequently_atTop.2 fun M ↦ ?_

Premises used: Iff.mpr, Filter.frequently_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
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)
neg : ∀ (M : ℕ), ∃ b_1 ≥ M, (↑(v b_1) : EReal) ≤ a' * (↑b_1 : EReal) → (u ∘ v) b_1 ≤ a * b * (↑b_1 : EReal)
⊢ ∃ᶠ (x : ℕ) in atTop, (↑(v x) : EReal) ≤ a' * (↑x : EReal) → (u ∘ v) x ≤ a * b * (↑x : EReal)

Tactic:
refine frequently_atTop.2 fun M ↦ ?_

Premises used: Iff.mpr, Filter.frequently_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
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 : ℕ
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)
⊢ ∃ 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

Premises used: EReal.exists_nat_ge_mul
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
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)
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)
⊢ ∃ 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'

Premises used: Filter.frequently_atTop, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
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)

Tactic:
⟨k, ?_, fun vk_ak' ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
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
neg₁ : ∀ (vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)), (u ∘ v) k ≤ a * b * (↑k : EReal)
⊢ ∃ b_1 ≥ M, (↑(v b_1) : EReal) ≤ a' * (↑b_1 : EReal) → (u ∘ v) b_1 ≤ a * b * (↑b_1 : EReal)

Tactic:
refine ⟨k, ?_, fun vk_ak' ↦ ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
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 :
  ∀ (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
⊢ k ≥ M

Tactic:
rw [mul_comm a, ← le_div_iff_mul_le a_0 a_top, EReal.div_eq_inv_mul] at aM_M'

Premises used: EReal.div_eq_inv_mul, mul_comm, EReal.le_div_iff_mul_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
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)
apply : a⁻¹ * (↑M' : EReal) ≤ a⁻¹ * (↑n : EReal)
⊢ k ≥ M

Tactic:
apply Nat.cast_le.1 <| aM_M'.trans <| an_k.trans' _

Premises used: Iff.mp, Nat.cast_le, LE.le.trans, LE.le.trans'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
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)
ha : 0 ≤ a⁻¹
⊢ a⁻¹ * (↑M' : EReal) ≤ a⁻¹ * (↑n : EReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
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)
neg : u (v k) ≤ b * (a * (↑k : EReal))
⊢ (u ∘ v) k ≤ a * b * (↑k : EReal)

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

Premises used: mul_assoc, mul_comm, Function.comp_apply
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
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)
⊢ 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'

Premises used: EReal.div_eq_inv_mul, mul_comm, ne_top_of_lt, EReal.le_div_iff_mul_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
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)
k_an'₁ : a' * (↑k : EReal) ≤ (↑n : EReal)
⊢ (↑(v k) : EReal) ≤ a' * (↑k : 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'

Premises used: EReal.div_eq_inv_mul, mul_comm, ne_top_of_lt, EReal.le_div_iff_mul_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
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)
⊢ (↑n : EReal) ≤ a * (↑k : EReal)

Tactic:
rw [← EReal.div_eq_inv_mul, div_le_iff_le_mul a_0 a_top] at an_k

Premises used: EReal.div_eq_inv_mul, EReal.div_le_iff_le_mul