awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f_1 : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f_1
h_approx_1 : ms.Approximates
motive : (ms : MultiseriesExpansion (basis_hd :: basis_tl)) → Prop :=
  fun (ms : MultiseriesExpansion (basis_hd :: basis_tl)) ↦
    ∃ (ms' : MultiseriesExpansion (basis_hd :: basis_tl)) (f' : ℝ → ℝ),
      ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : g =ᶠ[atTop] f
h_coef : coef.Approximates
h_maj : Majorized g basis_hd exp
h_tl : (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates
⊢ (mk tl (g - basis_hd ^ exp * coef.toFun)).toFun =ᶠ[atTop] f - basis_hd ^ exp * coef.toFun
have cons : g - basis_hd ^ exp * coef.toFun =ᶠ[atTop] f - basis_hd ^ exp * coef.toFun
Tactic: grw [mk_toFun, h_eq]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f_1 : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f_1
h_approx_1 : ms.Approximates
motive : (ms : MultiseriesExpansion (basis_hd :: basis_tl)) → Prop :=
  fun (ms : MultiseriesExpansion (basis_hd :: basis_tl)) ↦
    ∃ (ms' : MultiseriesExpansion (basis_hd :: basis_tl)) (f' : ℝ → ℝ),
      ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f : ℝ → ℝ
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
g : ℝ → ℝ
h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates
h_eq : g =ᶠ[atTop] f
h_coef : coef.Approximates
h_maj : Majorized g basis_hd exp
h_tl : (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates
cons : g - basis_hd ^ exp * coef.toFun =ᶠ[atTop] f - basis_hd ^ exp * coef.toFun
⊢ (mk tl (g - basis_hd ^ exp * coef.toFun)).toFun =ᶠ[atTop] f - basis_hd ^ exp * coef.toFun
have cons₁ : f - basis_hd ^ exp * coef.toFun =ᶠ[atTop] f - basis_hd ^ exp * coef.toFun
Tactic: grw [mk_toFun, h_eq]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms_1 : MultiseriesExpansion (basis_hd :: basis_tl)
f_1 : ℝ → ℝ
h_equiv : ms_1.toFun =ᶠ[atTop] f_1
h_approx_1 : ms_1.Approximates
motive : (ms : MultiseriesExpansion (basis_hd :: basis_tl)) → Prop :=
  fun (ms : MultiseriesExpansion (basis_hd :: basis_tl)) ↦
    ∃ (ms' : MultiseriesExpansion (basis_hd :: basis_tl)) (f' : ℝ → ℝ),
      ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_approx : ms.Approximates
h_eq : ms.toFun =ᶠ[atTop] f
⊢ (ms.replaceFun f).seq = Multiseries.nil ∧ (ms.replaceFun f).toFun =ᶠ[atTop] 0 ∨
    ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
      (ms.replaceFun f).seq = Multiseries.cons exp coef tl ∧
        coef.Approximates ∧
          Majorized (ms.replaceFun f).toFun basis_hd exp ∧
            motive (mk tl ((ms.replaceFun f).toFun - basis_hd ^ exp * coef.toFun))
have nil : ∀ (g : ℝ → ℝ) (h_approx : Approximates (basis := basis_hd :: basis_tl) (mk Multiseries.nil g))
  (h_eq : toFun (basis := basis_hd :: basis_tl) (mk Multiseries.nil g) =ᶠ[atTop] f),
  Eq (α := Multiseries basis_hd basis_tl) (seq (replaceFun (mk Multiseries.nil g) f)) Multiseries.nil ∧
      toFun (basis := basis_hd :: basis_tl) (replaceFun (mk Multiseries.nil g) f) =ᶠ[atTop] 0 ∨
    ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
      seq (replaceFun (mk Multiseries.nil g) f) = Multiseries.cons exp coef tl ∧
        coef.Approximates ∧
          Majorized (toFun (basis := basis_hd :: basis_tl) (replaceFun (mk Multiseries.nil g) f)) basis_hd exp ∧
            motive
              (mk tl
                (toFun (basis := basis_hd :: basis_tl) (replaceFun (mk Multiseries.nil g) f) -
                  basis_hd ^ exp * coef.toFun))
Tactic: cases ms with
  | nil g =>
    simp only [nil_iff, mk_toFun, mk_replaceFun, mk_seq, true_and,
      Multiseries.nil_ne_cons, false_and, exists_const, or_false] at h_approx h_eq ⊢
    grw [← h_eq, h_approx]
  | cons exp coef tl g =>
    obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons
    refine .inr ⟨exp, coef, tl, ?_⟩
    simp only [mk_replaceFun, mk_seq, h_coef, mk_toFun, true_and]
    simp only [mk_toFun] at h_eq
    refine ⟨h_maj.of_eventuallyEq h_eq.symm, mk tl (g - basis_hd ^ exp * coef.toFun), _, rfl,
      h_tl, ?_⟩
    grw [mk_toFun, h_eq]
Cleared hypotheses: ms, h_approx, h_eq
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ (f ^ exp) =o[atTop] (f ^ exp')
have apply : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (f ^ exp) x / (f ^ exp') x) atTop (𝓝 0)
Tactic: apply (isLittleO_iff_tendsto' _).mpr
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
apply : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (f ^ exp) x / (f ^ exp') x) atTop (𝓝 0)
⊢ (f ^ exp) =o[atTop] (f ^ exp')
have apply₁ : ∀ᶠ (x : ℝ) in atTop, (f ^ exp') x = 0 → (f ^ exp) x = 0
Tactic: apply (isLittleO_iff_tendsto' _).mpr
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (hypothesis)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (f ^ exp) x / (f ^ exp') x) atTop (𝓝 0)
have this : EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ f t ^ exp / f t ^ exp') fun (t : ℝ) ↦ f t ^ (exp - exp')
Tactic: have : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ (f t) ^ (exp - exp') :=
      (h.eventually_gt_atTop 0).mono (fun _ h ↦ by simp [← Real.rpow_sub h])
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ f t ^ exp / f t ^ exp') fun (t : ℝ) ↦ f t ^ (exp - exp')
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (f ^ exp) x / (f ^ exp') x) atTop (𝓝 0)
have apply : Tendsto (β := ℝ) (fun (t : ℝ) ↦ f t ^ (exp - exp')) atTop (𝓝 0)
Tactic: apply Tendsto.congr' this.symm
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ f t ^ exp / f t ^ exp') fun (t : ℝ) ↦ f t ^ (exp - exp')
| Tendsto (β := ℝ) (fun (t : ℝ) ↦ f t ^ (exp - exp')) atTop (𝓝 0)
have arg : fun (t : ℝ) ↦ f t ^ (exp - exp')
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ f t ^ exp / f t ^ exp') fun (t : ℝ) ↦ f t ^ (exp - exp')
⊢ Eq (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ f t ^ (exp - exp')) ((fun (t : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f)
have h₁ : ∀ (x : ℝ), f x ^ (exp - exp') = ((fun (t : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ f t ^ exp / f t ^ exp') fun (t : ℝ) ↦ f t ^ (exp - exp')
| fun (t : ℝ) ↦ f t ^ (exp - exp')
have rw : (fun (t : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f
Tactic: rw [show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ f t ^ exp / f t ^ exp') fun (t : ℝ) ↦ f t ^ (exp - exp')
| Tendsto (β := ℝ) (fun (t : ℝ) ↦ f t ^ (exp - exp')) atTop (𝓝 0)
have arg : (fun (t : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f
Tactic: arg 1
      rw [show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ f t ^ exp / f t ^ exp') fun (t : ℝ) ↦ f t ^ (exp - exp')
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ f t ^ (exp - exp')) atTop (𝓝 0)
have conv : Tendsto (β := ℝ) ((fun (t : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f) atTop (𝓝 0)
Tactic: conv =>
      arg 1
      rw [show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ f t ^ exp / f t ^ exp') fun (t : ℝ) ↦ f t ^ (exp - exp')
⊢ 0 < exp' - exp
have linarith : exp' - exp ≤ 0 → exp - exp' + (exp' - exp - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ ∀ᶠ (x : ℝ) in atTop, (f ^ exp') x = 0 → (f ^ exp) x = 0
have apply : ∀ (x : ℝ), 0 < f x → (f ^ exp') x = 0 → (f ^ exp) x = 0
Tactic: apply (Tendsto.eventually_gt_atTop h 0).mono
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
t : ℝ
h1 : 0 < f t
h2 : (f ^ exp') t = 0
⊢ (f ^ exp) t = 0
have absurd : ¬(f ^ exp') t = 0
Tactic: absurd h2
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f b : ℝ → ℝ
exp1 exp2 : ℝ
h_lt : exp1 ≤ exp2
h : ∀ exp' > exp1, f =o[atTop] (b ^ exp')
exp' : ℝ
h_exp : exp' > exp2
⊢ exp' > exp1
have linarith : exp' ≤ exp1 → exp1 - exp2 + (exp2 - exp') + (exp' - exp1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f b : ℝ → ℝ
exp : ℝ
h_lt : exp < 0
h : Majorized f b exp
⊢ 0 > exp
have linarith : 0 ≤ exp → exp - 0 + (0 - exp) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
⊢ IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ c) (b ^ exp)
have apply : c = 0 ∨ Tendsto (norm ∘ (b ^ exp)) atTop atTop
Tactic: apply Asymptotics.isLittleO_const_left.mpr
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
⊢ c = 0 ∨ Tendsto (norm ∘ (b ^ exp)) atTop atTop
have h : Tendsto (norm ∘ (b ^ exp)) atTop atTop
Tactic: right
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
⊢ Tendsto (norm ∘ (b ^ exp)) atTop atTop
have h : Tendsto (b ^ exp) atTop atTop
Tactic: apply tendsto_norm_atTop_atTop.comp
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
exp' : ℝ
h_exp' : exp' > exp
⊢ exp' > f_exp
have order : ¬exp' > f_exp → False
Tactic: order
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
exp' : ℝ
h_exp' : exp' > exp
order order₁ order₂ order₃ : ¬exp' > f_exp → False
⊢ exp' > f_exp
have order₄ : exp' ≤ f_exp → False
Tactic: order
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
exp' : ℝ
h_exp' : exp' > exp
⊢ exp' > g_exp
have order : ¬exp' > g_exp → False
Tactic: order
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
exp' : ℝ
h_exp' : exp' > exp
order order₁ order₂ order₃ : ¬exp' > g_exp → False
⊢ exp' > g_exp
have order₄ : exp' ≤ g_exp → False
Tactic: order
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
⊢ f_exp + (exp - f_exp - g_exp) / 2 > f_exp
have linarith : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
linarith : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → 2 / 2 = 1
⊢ f_exp + (exp - f_exp - g_exp) / 2 > f_exp
have linarith₁ : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
linarith : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → 2 / 2 = 1
linarith₁ : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → HMul.hMul (α := ℝ) 1 2 = 2
⊢ f_exp + (exp - f_exp - g_exp) / 2 > f_exp
have linarith₂ : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
linarith : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → 2 / 2 = 1
linarith₁ : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp → GT.gt (α := ℝ) 2 0
⊢ f_exp + (exp - f_exp - g_exp) / 2 > f_exp
have linarith₃ : f_exp + (exp - f_exp - g_exp) / 2 ≤ f_exp →
  f_exp + g_exp - exp + (2 * f_exp + (1 * exp - 1 * f_exp - 1 * g_exp) - 2 * f_exp) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (hypothesis)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
⊢ (f * g) =o[atTop] (b ^ exp)
have hf₁ : f =o[atTop] (b ^ (f_exp + ε))
Tactic: specialize hf (f_exp + ε) (by dsimp [ε]; linarith)
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
⊢ g_exp + (exp - f_exp - g_exp) / 2 > g_exp
have linarith : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
linarith : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → 2 / 2 = 1
⊢ g_exp + (exp - f_exp - g_exp) / 2 > g_exp
have linarith₁ : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
linarith : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → 2 / 2 = 1
linarith₁ : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → HMul.hMul (α := ℝ) 1 2 = 2
⊢ g_exp + (exp - f_exp - g_exp) / 2 > g_exp
have linarith₂ : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
linarith : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → 2 / 2 = 1
linarith₁ : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp → GT.gt (α := ℝ) 2 0
⊢ g_exp + (exp - f_exp - g_exp) / 2 > g_exp
have linarith₃ : g_exp + (exp - f_exp - g_exp) / 2 ≤ g_exp →
  f_exp + g_exp - exp + (2 * g_exp + (1 * exp - 1 * f_exp - 1 * g_exp) - 2 * g_exp) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (hypothesis)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
⊢ (f * g) =o[atTop] (b ^ exp)
have hg₁ : g =o[atTop] (b ^ (g_exp + ε))
Tactic: specialize hg (g_exp + ε) (by dsimp [ε]; linarith)
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
hg : g =o[atTop] (b ^ (g_exp + ε))
⊢ (f * g) =o[atTop] (b ^ exp)
have apply : (fun (t : ℝ) ↦ b t ^ (f_exp + ε) * b t ^ (g_exp + ε)) =ᶠ[atTop] b ^ exp
Tactic: apply (hf.mul hg).trans_eventuallyEq (g₁ := fun t ↦ b t ^ (f_exp + ε) * b t ^ (g_exp + ε))
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
hg : g =o[atTop] (b ^ (g_exp + ε))
⊢ (fun (t : ℝ) ↦ b t ^ (f_exp + ε) * b t ^ (g_exp + ε)) =ᶠ[atTop] b ^ exp
have apply : ∀ (x : ℝ), 0 < b x → (fun (t : ℝ) ↦ b t ^ (f_exp + ε) * b t ^ (g_exp + ε)) x = (b ^ exp) x
Tactic: apply h_pos.mono
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
hg : g =o[atTop] (b ^ (g_exp + ε))
t : ℝ
hx : 0 < b t
| b t ^ exp
have rw : b t ^ (f_exp + ε) * b t ^ (g_exp + ε)
Tactic: rw [show exp = (f_exp + ε) + (g_exp + ε) by dsimp [ε]; ring_nf, Real.rpow_add hx]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
hg : g =o[atTop] (b ^ (g_exp + ε))
t : ℝ
hx : 0 < b t
⊢ b t ^ (f_exp + ε) * b t ^ (g_exp + ε) = b t ^ exp
have conv_rhs : b t ^ (f_exp + ε) * b t ^ (g_exp + ε) = b t ^ exp
Tactic: conv_rhs => rw [show exp = (f_exp + ε) + (g_exp + ε) by dsimp [ε]; ring_nf, Real.rpow_add hx]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
hg : g =o[atTop] (b ^ (g_exp + ε))
t : ℝ
hx : 0 < b t
conv_rhs : b t ^ (f_exp + ε) * b t ^ (g_exp + ε) = b t ^ exp
⊢ b t ^ (f_exp + ε) * b t ^ (g_exp + ε) = b t ^ exp
have conv_rhs₁ : b t ^ (f_exp + ε) * b t ^ (g_exp + ε) = b t ^ (f_exp + ε) * b t ^ (g_exp + ε)
Tactic: conv_rhs => rw [show exp = (f_exp + ε) + (g_exp + ε) by dsimp [ε]; ring_nf, Real.rpow_add hx]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g basis_hd : ℝ → ℝ
exp_1 : ℝ
hf : Majorized f basis_hd exp_1
hg : IsBigO (F := ℝ) atTop g fun (x : ℝ) ↦ 1
exp : ℝ
h_exp : exp > exp_1
⊢ (f * g) =o[atTop] (basis_hd ^ exp)
have h : basis_hd ^ exp = fun (x : ℝ) ↦ (basis_hd ^ exp) x * 1
Tactic: convert! IsLittleO.mul_isBigO (hf _ h_exp) hg using 1
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (goal)
Goal:
f g basis_hd : ℝ → ℝ
exp_1 : ℝ
hf : Majorized f basis_hd exp_1
hg : IsBigO (F := ℝ) atTop g fun (x : ℝ) ↦ 1
exp : ℝ
h_exp : exp > exp_1
⊢ basis_hd ^ exp = fun (x : ℝ) ↦ (basis_hd ^ exp) x * 1
have h : basis_hd ^ exp = fun (x : ℝ) ↦ basis_hd x ^ exp
Tactic: simp
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
basis : Basis
⊢ toFun [] basis = 1
have h : ∀ (x : ℝ), toFun [] basis x = 1 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
m : UnitMonomial
⊢ m.toFun [] = 1
have h : ∀ (x : ℝ), m.toFun [] x = 1 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
exp : ℝ
tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ toFun (exp :: tl) (basis_hd :: basis_tl) = basis_hd ^ exp * tl.toFun basis_tl
have h : ∀ (x : ℝ), toFun (exp :: tl) (basis_hd :: basis_tl) x = (basis_hd ^ exp * tl.toFun basis_tl) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
basis : Basis
⊢ toLogFun [] basis = 0
have h : ∀ (x : ℝ), toLogFun [] basis x = 0 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
m : UnitMonomial
⊢ m.toLogFun [] = 0
have h : ∀ (x : ℝ), m.toLogFun [] x = 0 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
exp : ℝ
tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ toLogFun (exp :: tl) (basis_hd :: basis_tl) = exp • log ∘ basis_hd + tl.toLogFun basis_tl
have h : ∀ (x : ℝ), toLogFun (exp :: tl) (basis_hd :: basis_tl) x = (exp • log ∘ basis_hd + tl.toLogFun basis_tl) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (goal)
Goal:
m1 m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m1 = List.length m2
⊢ (m1.mul m2).toFun basis =ᶠ[atTop] m1.toFun basis * m2.toFun basis
have apply : ∀ (x : ℝ), (∀ f ∈ basis, 0 < f x) → (m1.mul m2).toFun basis x = (m1.toFun basis * m2.toFun basis) x
Tactic: apply h_basis.eventually_pos.mono
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (hypothesis)
Goal:
x : ℝ
m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length (α := ℝ) [] = List.length m2
h_pos : ∀ f ∈ basis, 0 < f x
⊢ List.prod
      (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) (List.zipWith (fun (x1 x2 : ℝ) ↦ x1 + x2) [] m2) basis) =
    HMul.hMul (α := ℝ) (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) [] basis))
      (List.prod (List.zipWith (fun (exp : ℝ) (b : ℝ → ℝ) ↦ b x ^ exp) m2 basis))
have h_length₁ : List.length m2 = List.length (α := ℝ) []
Tactic: symm at h_length
Cleared hypotheses: h_length, h_pos