awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a b : EReal
h : b > a
n : ℕ
h_1 : n ≥ 1
rw : u n ≤ (↑n : EReal) * b ↔ u n ≤ b * (↑n : EReal)
⊢ u n / (↑n : EReal) ≤ b ↔ u n ≤ b * (↑n : EReal)
have rw₁ : u n ≤ b * (↑n : EReal) ↔ u n ≤ b * (↑n : EReal)
Tactic: rw [div_le_iff_le_mul (by norm_cast) (natCast_ne_top n), mul_comm _ b]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
⊢ a ≤ linearGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n
have rw : (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ u a / (↑a : EReal)) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n
Tactic: rw [linearGrowthInf, le_liminf_iff']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ u a / (↑a : EReal)) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n
have refine : ∀ b < a, ∀ n ≥ 1, b ≤ u n / (↑n : EReal) ↔ b * (↑n : EReal) ≤ u n
Tactic: refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a b : EReal
h : b < a
n : ℕ
h_1 : n ≥ 1
⊢ GT.gt (α := EReal) (↑n : EReal) 0
have norm_cast : 0 < n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a b : EReal
h : b < a
n : ℕ
h_1 : n ≥ 1
⊢ b ≤ u n / (↑n : EReal) ↔ b * (↑n : EReal) ≤ u n
have nth_rw : b * (↑n : EReal) ≤ u n ↔ b * (↑n : EReal) ≤ u n
Tactic: nth_rw 1 [le_div_iff_mul_le (by norm_cast) (natCast_ne_top n)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
⊢ linearGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)
have rw : (∀ y > a, ∀ᶠ (a : ℕ) in atTop, u a / (↑a : EReal) ≤ y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)
Tactic: rw [linearGrowthSup, limsup_le_iff']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, u a / (↑a : EReal) ≤ y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)
have refine : ∀ b > a, ∀ n ≥ 1, u n / (↑n : EReal) ≤ b ↔ u n ≤ b * (↑n : EReal)
Tactic: refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
⊢ a ≤ linearGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n
have rw : (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ u a / (↑a : EReal)) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n
Tactic: rw [linearGrowthSup, le_limsup_iff']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ u a / (↑a : EReal)) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n
have refine : ∀ b < a, ∀ n ≥ 1, b ≤ u n / (↑n : EReal) ↔ b * (↑n : EReal) ≤ u n
Tactic: refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ a * (↑n : EReal)
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ a * (↑n : EReal)
⊢ a * (↑n : EReal) ≤ c * (↑n : EReal)
have ha : LE.le (α := EReal) 0 (↑n : EReal)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, a * (↑n : EReal) ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : a * (↑n : EReal) ≤ u n
⊢ c * (↑n : EReal) ≤ a * (↑n : EReal)
have ha : LE.le (α := EReal) 0 (↑n : EReal)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ a * (↑n : EReal)
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ a * (↑n : EReal)
⊢ a * (↑n : EReal) ≤ c * (↑n : EReal)
have ha : LE.le (α := EReal) 0 (↑n : EReal)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, a * (↑n : EReal) ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : a * (↑n : EReal) ≤ u n
⊢ c * (↑n : EReal) ≤ a * (↑n : EReal)
have ha : LE.le (α := EReal) 0 (↑n : EReal)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
⊢ Eq (α := EReal) (linearGrowthSup ⊥) ⊥
have nth_rw : Eq (α := EReal) (linearGrowthSup ⊥) (limsup (fun (x : ℕ) ↦ ⊥) atTop)
Tactic: nth_rw 2 [← limsup_const (f := atTop (α := ℕ)) ⊥]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
⊢ Eq (α := EReal) (linearGrowthSup ⊥) (limsup (fun (x : ℕ) ↦ ⊥) atTop)
have refine : ∀ (n : ℕ) (n_pos : 0 < n), HDiv.hDiv (α := EReal) (⊥ n) (↑n : EReal) = ⊥
Tactic: refine limsup_congr <| (eventually_gt_atTop 0).mono fun n n_pos ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
⊢ Eq (α := EReal) (linearGrowthInf ⊥) ⊥
have apply : LE.le (α := EReal) (linearGrowthInf ⊥) ⊥
Tactic: apply le_bot_iff.1
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
⊢ LE.le (α := EReal) (linearGrowthInf ⊥) ⊥
have rw : LE.le (α := EReal) (linearGrowthInf ⊥) (linearGrowthSup ⊥)
Tactic: rw [← linearGrowthSup_bot]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
⊢ Eq (α := EReal) (linearGrowthInf ⊤) ⊤
have nth_rw : Eq (α := EReal) (linearGrowthInf ⊤) (liminf (fun (x : ℕ) ↦ ⊤) atTop)
Tactic: nth_rw 2 [← liminf_const (f := atTop (α := ℕ)) ⊤]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
⊢ Eq (α := EReal) (linearGrowthInf ⊤) (liminf (fun (x : ℕ) ↦ ⊤) atTop)
have refine : ∃ (a : ℕ), ∀ b ≥ a, HDiv.hDiv (α := EReal) (⊤ b) (↑b : EReal) = ⊤
Tactic: refine liminf_congr (eventually_atTop.2 ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
⊢ Eq (α := EReal) (linearGrowthSup ⊤) ⊤
have apply : LE.le (α := EReal) ⊤ (linearGrowthSup ⊤)
Tactic: apply top_le_iff.1
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
⊢ LE.le (α := EReal) ⊤ (linearGrowthSup ⊤)
have rw : LE.le (α := EReal) (linearGrowthInf ⊤) (linearGrowthSup ⊤)
Tactic: rw [← linearGrowthInf_top]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
⊢ Tendsto u atTop (𝓝 ⊤)
have obtain : ∀ (a : EReal) (a_0 : 0 < a) (a_v : a < linearGrowthInf u), Tendsto u atTop (𝓝 ⊤)
Tactic: obtain ⟨a, a_0, a_v⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf u
⊢ Tendsto u atTop (𝓝 ⊤)
have apply : Tendsto (β := EReal) (fun (x : ℕ) ↦ a * (↑x : EReal)) atTop (𝓝 ⊤)
Tactic: apply tendsto_nhds_top_mono _ ((le_linearGrowthInf_iff (u := u)).1 (le_refl _) a a_v)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf u
⊢ Tendsto (β := EReal) (fun (x : ℕ) ↦ a * (↑x : EReal)) atTop (𝓝 ⊤)
have refine : ∀ (M : ℝ), ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < a * (↑b : EReal)
Tactic: refine tendsto_nhds_top_iff_real.2 fun M ↦ eventually_atTop.2 ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf u
M : ℝ
⊢ ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < a * (↑b : EReal)
have lift : ∀ (a : ℝ) (a_0 : 0 < (↑a : EReal)) (a_v : (↑a : EReal) < linearGrowthInf u),
  ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < (↑a : EReal) * (↑b : EReal)
Tactic: lift a to ℝ using ⟨ne_top_of_lt a_v, ne_bot_of_gt a_0⟩
Cleared hypotheses: a, a_0, a_v
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < (↑a : EReal)
a_v : (↑a : EReal) < linearGrowthInf u
⊢ ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < (↑a : EReal) * (↑b : EReal)
have a_0₁ : 0 < a
Tactic: rw [EReal.coe_pos] at a_0
Cleared hypotheses: a_0, a_v
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : (↑a : EReal) < linearGrowthInf u
⊢ ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < (↑a : EReal) * (↑b : EReal)
have obtain : ∀ (n : ℕ) (hn : M / a ≤ (↑n : ℝ)), ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < (↑a : EReal) * (↑b : EReal)
Tactic: obtain ⟨n, hn⟩ := exists_nat_ge (M / a)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : (↑a : EReal) < linearGrowthInf u
n : ℕ
hn : M / a ≤ (↑n : ℝ)
⊢ ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < (↑a : EReal) * (↑b : EReal)
have refine : ∀ (k : ℕ) (k_n : k ≥ n + 1), (↑M : EReal) < (↑a : EReal) * (↑k : EReal)
Tactic: refine ⟨n + 1, fun k k_n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : (↑a : EReal) < linearGrowthInf u
n : ℕ
hn : M / a ≤ (↑n : ℝ)
k : ℕ
k_n : k ≥ n + 1
⊢ (↑M : EReal) < (↑a : EReal) * (↑k : EReal)
have rw : M < (↑k : ℝ) * a
Tactic: rw [← coe_coe_eq_natCast, ← coe_mul, EReal.coe_lt_coe_iff, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
⊢ linearGrowthInf u + linearGrowthInf v ≤ linearGrowthInf (u + v)
have refine : ∀ (n : ℕ),
  HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
Tactic: refine le_liminf_add.trans_eq (liminf_congr (Eventually.of_forall fun n ↦ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
n : ℕ
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, ← add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
n : ℕ
rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw₁ : u n / (↑n : EReal) + v n / (↑n : EReal) = (u n + v n) / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, ← add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
n : ℕ
rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
rw₁ : u n / (↑n : EReal) + v n / (↑n : EReal) = (u n + v n) / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw₂ : (u n + v n) / (↑n : EReal) = (u n + v n) / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, ← add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf v ≠ ⊥
⊢ linearGrowthInf (u + v) ≤ linearGrowthSup u + linearGrowthInf v
have refine : ∀ (n : ℕ),
  HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
Tactic: refine (liminf_add_le h h').trans_eq' (liminf_congr (Eventually.of_forall fun n ↦ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf v ≠ ⊥
n : ℕ
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, ← add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf v ≠ ⊥
n : ℕ
rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw₁ : u n / (↑n : EReal) + v n / (↑n : EReal) = (u n + v n) / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, ← add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf v ≠ ⊥
n : ℕ
rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
rw₁ : u n / (↑n : EReal) + v n / (↑n : EReal) = (u n + v n) / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw₂ : (u n + v n) / (↑n : EReal) = (u n + v n) / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, ← add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthInf (u + v) ≤ linearGrowthInf u + linearGrowthSup v
have rw : linearGrowthInf (v + u) ≤ linearGrowthSup v + linearGrowthInf u
Tactic: rw [add_comm u v, add_comm (linearGrowthInf u) (linearGrowthSup v)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
⊢ linearGrowthSup u + linearGrowthInf v ≤ linearGrowthSup (u + v)
have refine : ∀ (n : ℕ),
  HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
Tactic: refine le_limsup_add.trans_eq (limsup_congr (Eventually.of_forall fun n ↦ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
n : ℕ
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
n : ℕ
rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw₁ : u n / (↑n : EReal) + v n / (↑n : EReal) = (u n + v n) / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
n : ℕ
rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
rw₁ : u n / (↑n : EReal) + v n / (↑n : EReal) = (u n + v n) / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw₂ : u n / (↑n : EReal) + v n / (↑n : EReal) = u n / (↑n : EReal) + v n / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
⊢ linearGrowthInf u + linearGrowthSup v ≤ linearGrowthSup (u + v)
have rw : linearGrowthSup v + linearGrowthInf u ≤ linearGrowthSup (v + u)
Tactic: rw [add_comm u v, add_comm (linearGrowthInf u) (linearGrowthSup v)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthSup (u + v) ≤ linearGrowthSup u + linearGrowthSup v
have refine : ∀ (n : ℕ),
  HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
Tactic: refine (limsup_add_le h h').trans_eq' (limsup_congr (Eventually.of_forall fun n ↦ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
n : ℕ
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
n : ℕ
rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw₁ : u n / (↑n : EReal) + v n / (↑n : EReal) = (u n + v n) / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
n : ℕ
rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
rw₁ : u n / (↑n : EReal) + v n / (↑n : EReal) = (u n + v n) / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)
have rw₂ : u n / (↑n : EReal) + v n / (↑n : EReal) = u n / (↑n : EReal) + v n / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.add_apply, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
⊢ linearGrowthInf (-u) = -linearGrowthSup u
have rw : linearGrowthInf (-u) = liminf (β := ℕ) (-fun (n : ℕ) ↦ u n / (↑n : EReal)) atTop
Tactic: rw [linearGrowthSup, ← liminf_neg]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
⊢ linearGrowthInf (-u) = liminf (β := ℕ) (-fun (n : ℕ) ↦ u n / (↑n : EReal)) atTop
have refine : ∀ (n : ℕ), (-u) n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
Tactic: refine liminf_congr (Eventually.of_forall fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
n : ℕ
⊢ (-u) n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
have rw : -u n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
Tactic: rw [Pi.neg_apply, Pi.neg_apply, div_eq_mul_inv, div_eq_mul_inv, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
n : ℕ
rw : -u n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
⊢ (-u) n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
have rw₁ : -u n / (↑n : EReal) = -(u n / (↑n : EReal))
Tactic: rw [Pi.neg_apply, Pi.neg_apply, div_eq_mul_inv, div_eq_mul_inv, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
n : ℕ
rw : -u n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
rw₁ : -u n / (↑n : EReal) = -(u n / (↑n : EReal))
⊢ (-u) n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
have rw₂ : -u n * (↑n : EReal)⁻¹ = -(u n / (↑n : EReal))
Tactic: rw [Pi.neg_apply, Pi.neg_apply, div_eq_mul_inv, div_eq_mul_inv, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
n : ℕ
rw : -u n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
rw₁ : -u n / (↑n : EReal) = -(u n / (↑n : EReal))
rw₂ : -u n * (↑n : EReal)⁻¹ = -(u n / (↑n : EReal))
⊢ (-u) n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
have rw₃ : -u n * (↑n : EReal)⁻¹ = -(u n * (↑n : EReal)⁻¹)
Tactic: rw [Pi.neg_apply, Pi.neg_apply, div_eq_mul_inv, div_eq_mul_inv, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
n : ℕ
rw : -u n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
rw₁ : -u n / (↑n : EReal) = -(u n / (↑n : EReal))
rw₂ : -u n * (↑n : EReal)⁻¹ = -(u n / (↑n : EReal))
rw₃ : -u n * (↑n : EReal)⁻¹ = -(u n * (↑n : EReal)⁻¹)
⊢ (-u) n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
have rw₄ : -u n * (↑n : EReal)⁻¹ = -u n * (↑n : EReal)⁻¹
Tactic: rw [Pi.neg_apply, Pi.neg_apply, div_eq_mul_inv, div_eq_mul_inv, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
⊢ linearGrowthSup (-u) = -linearGrowthInf u
have rw : linearGrowthSup (-u) = limsup (β := ℕ) (-fun (n : ℕ) ↦ u n / (↑n : EReal)) atTop
Tactic: rw [linearGrowthInf, ← limsup_neg]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
⊢ linearGrowthSup (-u) = limsup (β := ℕ) (-fun (n : ℕ) ↦ u n / (↑n : EReal)) atTop
have refine : ∀ (n : ℕ), (-u) n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
Tactic: refine limsup_congr (Eventually.of_forall fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
⊢ linearGrowthInf u ≤ linearGrowthInf v
have apply : (linearGrowthInf fun (x : ℕ) ↦ v x + b) ≤ linearGrowthInf v
Tactic: apply (linearGrowthInf_eventually_monotone h).trans
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
⊢ (linearGrowthInf fun (x : ℕ) ↦ v x + b) ≤ linearGrowthInf v
have inl : ∀ (hb : Ne (α := EReal) ⊥ ⊤) (h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + ⊥),
  (linearGrowthInf fun (x : ℕ) ↦ v x + ⊥) ≤ linearGrowthInf v
Tactic: rcases eq_bot_or_bot_lt b with rfl | b_bot
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
inl :
  ∀ (hb : Ne (α := EReal) ⊥ ⊤) (h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + ⊥),
    (linearGrowthInf fun (x : ℕ) ↦ v x + ⊥) ≤ linearGrowthInf v
⊢ (linearGrowthInf fun (x : ℕ) ↦ v x + b) ≤ linearGrowthInf v
have inr : ∀ (b_bot : ⊥ < b), (linearGrowthInf fun (x : ℕ) ↦ v x + b) ≤ linearGrowthInf v
Tactic: rcases eq_bot_or_bot_lt b with rfl | b_bot
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthInf fun (x : ℕ) ↦ v x + b) ≤ linearGrowthInf v
have inr : (linearGrowthInf v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthInf v
Tactic: apply (linearGrowthInf_add_le' _ _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
inr : (linearGrowthInf v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthInf v
⊢ (linearGrowthInf fun (x : ℕ) ↦ v x + b) ≤ linearGrowthInf v
have apply : linearGrowthInf v ≠ ⊥ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊤
Tactic: apply (linearGrowthInf_add_le' _ _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
inr : (linearGrowthInf v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthInf v
apply : linearGrowthInf v ≠ ⊥ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊤
⊢ (linearGrowthInf fun (x : ℕ) ↦ v x + b) ≤ linearGrowthInf v
have apply₁ : linearGrowthInf v ≠ ⊤ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊥
Tactic: apply (linearGrowthInf_add_le' _ _).trans_eq