awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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 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
nil : ∀ (h_approx : g =ᶠ[atTop] 0), f =ᶠ[atTop] 0
⊢ 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:
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 ⊢

Premises used: ComputeAsymptotics.MultiseriesExpansion.mk_seq, false_and, ComputeAsymptotics.MultiseriesExpansion.Approximates.nil_iff, exists_const, ComputeAsymptotics.MultiseriesExpansion.mk_replaceFun, ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil_ne_cons, ComputeAsymptotics.MultiseriesExpansion.mk_toFun, or_false, true_and
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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 g : ℝ → ℝ
h_eq : g =ᶠ[atTop] f
h_approx nil : g =ᶠ[atTop] 0
nil₁ nil₂ : EventuallyEq (α := ℝ) (β := ℝ) atTop 0 0
⊢ f =ᶠ[atTop] 0

Tactic:
grw [← h_eq, h_approx]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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 : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[atTop] f
⊢ coef.Approximates

Tactic:
obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons

Premises used: ComputeAsymptotics.MultiseriesExpansion.Approximates.elim_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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 : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[atTop] f
h_coef : coef.Approximates
⊢ Majorized g basis_hd exp

Tactic:
obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons

Premises used: ComputeAsymptotics.MultiseriesExpansion.Approximates.elim_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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 : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[atTop] f
h_coef : coef.Approximates
h_maj : Majorized g basis_hd exp
⊢ (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons

Premises used: ComputeAsymptotics.MultiseriesExpansion.Approximates.elim_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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 : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[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 (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.nil ∧
      ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun =ᶠ[atTop] 0 ∨
    ∃ (exp_1 : ℝ) (coef_1 : MultiseriesExpansion basis_tl) (tl_1 : Multiseries basis_hd basis_tl),
      ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.cons exp_1 coef_1 tl_1 ∧
        coef_1.Approximates ∧
          Majorized ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun basis_hd exp_1 ∧
            motive
              (mk tl_1 (((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun - basis_hd ^ exp_1 * coef_1.toFun))

Tactic:
.inr ⟨exp, coef, tl, ?_⟩

Premises used: Exists.intro, Or.inr
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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 : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[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 :
  ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.cons exp coef tl ∧
    coef.Approximates ∧
      Majorized ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun basis_hd exp ∧
        motive (mk tl (((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun - basis_hd ^ exp * coef.toFun))
⊢ ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.nil ∧
      ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun =ᶠ[atTop] 0 ∨
    ∃ (exp_1 : ℝ) (coef_1 : MultiseriesExpansion basis_tl) (tl_1 : Multiseries basis_hd basis_tl),
      ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.cons exp_1 coef_1 tl_1 ∧
        coef_1.Approximates ∧
          Majorized ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun basis_hd exp_1 ∧
            motive
              (mk tl_1 (((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun - basis_hd ^ exp_1 * coef_1.toFun))

Tactic:
refine .inr ⟨exp, coef, tl, ?_⟩
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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 : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[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 : Majorized f basis_hd exp ∧ motive (mk tl (f - basis_hd ^ exp * coef.toFun))
⊢ ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.cons exp coef tl ∧
    coef.Approximates ∧
      Majorized ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun basis_hd exp ∧
        motive (mk tl (((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun - basis_hd ^ exp * coef.toFun))

Tactic:
simp only [mk_replaceFun, mk_seq, h_coef, mk_toFun, true_and]

Premises used: ComputeAsymptotics.MultiseriesExpansion.mk_seq, ComputeAsymptotics.MultiseriesExpansion.mk_replaceFun, ComputeAsymptotics.MultiseriesExpansion.mk_toFun, true_and
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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
⊢ Majorized f basis_hd exp ∧ motive (mk tl (f - basis_hd ^ exp * coef.toFun))

Tactic:
⟨h_maj.of_eventuallyEq h_eq.symm, mk tl (g - basis_hd ^ exp * coef.toFun), _, rfl,
      h_tl, ?_⟩

Premises used: Tactic.ComputeAsymptotics.Majorized.of_eventuallyEq, HMul.hMul, ComputeAsymptotics.MultiseriesExpansion.toFun, HSub.hSub, HPow.hPow, And.intro, Exists.intro, ComputeAsymptotics.MultiseriesExpansion.mk, Filter.EventuallyEq.symm, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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 : (mk tl (g - basis_hd ^ exp * coef.toFun)).toFun =ᶠ[atTop] f - basis_hd ^ exp * coef.toFun
⊢ Majorized f basis_hd exp ∧ motive (mk tl (f - basis_hd ^ exp * coef.toFun))

Tactic:
refine ⟨h_maj.of_eventuallyEq h_eq.symm, mk tl (g - basis_hd ^ exp * coef.toFun), _, rfl,
      h_tl, ?_⟩
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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
cons₁ cons₂ : f - 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

Tactic:
grw [mk_toFun, h_eq]

Premises used: ComputeAsymptotics.MultiseriesExpansion.mk_toFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd_1 : ℝ → ℝ
basis_tl_1 : Basis
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ (x : MultiseriesExpansion (basis_hd :: basis_tl)), x.seq = x.seq ∧ x.toFun =ᶠ[atTop] x.toFun

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd_1 : ℝ → ℝ
basis_tl_1 : Basis
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ {x y : MultiseriesExpansion (basis_hd :: basis_tl)},
    x.seq = y.seq ∧ x.toFun =ᶠ[atTop] y.toFun → y.seq = x.seq ∧ y.toFun =ᶠ[atTop] x.toFun

Tactic:
grind [EventuallyEq.symm]

Premises used: Filter.EventuallyEq.symm
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd_1 : ℝ → ℝ
basis_tl_1 : Basis
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ {x y z : MultiseriesExpansion (basis_hd :: basis_tl)},
    x.seq = y.seq ∧ x.toFun =ᶠ[atTop] y.toFun →
      y.seq = z.seq ∧ y.toFun =ᶠ[atTop] z.toFun → x.seq = z.seq ∧ x.toFun =ᶠ[atTop] z.toFun

Tactic:
grind [EventuallyEq.trans]

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
x y : MultiseriesExpansion (basis_hd :: basis_tl)
⊢ x ≈ y ↔ x.seq = y.seq ∧ x.toFun =ᶠ[atTop] y.toFun

Tactic:
rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g b : ℝ → ℝ
exp : ℝ
h_eq : g =ᶠ[atTop] f
h : ∀ exp' > exp, f =o[atTop] (b ^ exp')
exp' : ℝ
h_exp : exp' > exp
⊢ g =o[atTop] (b ^ exp')

Tactic:
EventuallyEq.trans_isLittleO h_eq (h exp' h_exp)

Premises used: Filter.EventuallyEq.trans_isLittleO
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f g b : ℝ → ℝ
exp : ℝ
h_eq : g =ᶠ[atTop] f
h : ∀ exp' > exp, f =o[atTop] (b ^ exp')
exp' : ℝ
h_exp : exp' > exp
⊢ g =o[atTop] (b ^ exp')

Tactic:
exact EventuallyEq.trans_isLittleO h_eq (h exp' h_exp)

Premises used: Filter.EventuallyEq.trans_isLittleO
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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)
apply₁ : ∀ᶠ (x : ℝ) in atTop, (f ^ exp') x = 0 → (f ^ exp) x = 0
⊢ (f ^ exp) =o[atTop] (f ^ exp')

Tactic:
apply (isLittleO_iff_tendsto' _).mpr

Premises used: Iff.mpr, Asymptotics.isLittleO_iff_tendsto'
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f : ℝ → ℝ
exp : ℝ
h_1 : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
x : ℝ
h : 0 < f x
⊢ Eq (α := ℝ) ((fun (t : ℝ) ↦ f t ^ exp / f t ^ exp') x) ((fun (t : ℝ) ↦ f t ^ (exp - exp')) x)

Tactic:
simp [← Real.rpow_sub h]

Premises used: Real.rpow_sub
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ 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])
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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')
apply : Tendsto (β := ℝ) (fun (t : ℝ) ↦ f t ^ (exp - exp')) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (f ^ exp) x / (f ^ exp') x) atTop (𝓝 0)

Tactic:
apply Tendsto.congr' this.symm

Premises used: Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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')
arg : fun (t : ℝ) ↦ f t ^ (exp - exp')
| Tendsto (β := ℝ) (fun (t : ℝ) ↦ f t ^ (exp - exp')) atTop (𝓝 0)

Tactic:
arg 1
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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')
h₁ : ∀ (x : ℝ), f x ^ (exp - exp') = ((fun (t : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f) x
⊢ Eq (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ f t ^ (exp - exp')) ((fun (t : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f)

Tactic:
ext
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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')
x : ℝ
⊢ f x ^ (exp - exp') = ((fun (t : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f) x

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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')
rw : (fun (t : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f
| fun (t : ℝ) ↦ f t ^ (exp - exp')

Tactic:
rw [show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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')
arg : (fun (t : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f
| Tendsto (β := ℝ) (fun (t : ℝ) ↦ f t ^ (exp - exp')) atTop (𝓝 0)

Tactic:
arg 1
      rw [show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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')
conv : Tendsto (β := ℝ) ((fun (t : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ f t ^ (exp - exp')) atTop (𝓝 0)

Tactic:
conv =>
      arg 1
      rw [show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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')
linarith : exp' - exp ≤ 0 → exp - exp' + (exp' - exp - 0) = 0
⊢ 0 < exp' - exp

Tactic:
linarith
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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 : ℝ) ↦ t ^ (-(exp' - exp))) ∘ f) atTop (𝓝 0)

Tactic:
exact (tendsto_rpow_neg_atTop (by linarith)).comp h

Premises used: tendsto_rpow_neg_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
apply : ∀ (x : ℝ), 0 < f x → (f ^ exp') x = 0 → (f ^ exp) x = 0
⊢ ∀ᶠ (x : ℝ) in atTop, (f ^ exp') x = 0 → (f ^ exp) x = 0

Tactic:
apply (Tendsto.eventually_gt_atTop h 0).mono

Premises used: Filter.Eventually.mono, OfNat.ofNat, Filter.Tendsto.eventually_gt_atTop
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
t : ℝ
h1 : 0 < f t
h2 : (f ^ exp') t = 0
⊢ ¬?_mvar.2248

Tactic:
h2
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
t : ℝ
h1 : 0 < f t
h2 : (f ^ exp') t = 0
absurd : ¬(f ^ exp') t = 0
⊢ (f ^ exp) t = 0

Tactic:
absurd h2
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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

Tactic:
(Real.rpow_pos_of_pos h1 _).ne.symm

Premises used: Real.rpow_pos_of_pos, Ne.symm, LT.lt.ne
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
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

Tactic:
exact (Real.rpow_pos_of_pos h1 _).ne.symm

Premises used: Real.rpow_pos_of_pos, Ne.symm, LT.lt.ne
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f b : ℝ → ℝ
exp1 exp2 : ℝ
h_lt : exp1 ≤ exp2
h : ∀ exp' > exp1, f =o[atTop] (b ^ exp')
exp' : ℝ
h_exp : exp' > exp2
linarith : exp' ≤ exp1 → exp1 - exp2 + (exp2 - exp') + (exp' - exp1) = 0
⊢ exp' > exp1

Tactic:
linarith
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f b : ℝ → ℝ
exp1 exp2 : ℝ
h_lt : exp1 ≤ exp2
h : ∀ exp' > exp1, f =o[atTop] (b ^ exp')
⊢ ∀ exp' > exp2, f =o[atTop] (b ^ exp')

Tactic:
exact fun exp' h_exp ↦ h _ (by linarith)
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f b : ℝ → ℝ
exp : ℝ
h_lt : exp < 0
h : Majorized f b exp
linarith : 0 ≤ exp → exp - 0 + (0 - exp) = 0
⊢ 0 > exp

Tactic:
linarith
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
f b : ℝ → ℝ
exp : ℝ
h_lt : exp < 0
h : Majorized f b exp
⊢ Tendsto f atTop (𝓝 0)

Tactic:
simpa [Pi.pow_def, Majorized] using h 0 (by linarith)

Premises used: Tactic.ComputeAsymptotics.Majorized, OfNat.ofNat, Pi.pow_def
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
apply : c = 0 ∨ Tendsto (norm ∘ (b ^ exp)) atTop atTop
⊢ IsLittleO (E := ℝ) atTop (fun (x : ℝ) ↦ c) (b ^ exp)

Tactic:
apply Asymptotics.isLittleO_const_left.mpr

Premises used: Iff.mpr, Asymptotics.isLittleO_const_left
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
h : Tendsto (norm ∘ (b ^ exp)) atTop atTop
⊢ c = 0 ∨ Tendsto (norm ∘ (b ^ exp)) atTop atTop

Tactic:
right
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
h : Tendsto (b ^ exp) atTop atTop
⊢ Tendsto (norm ∘ (b ^ exp)) atTop atTop

Tactic:
apply tendsto_norm_atTop_atTop.comp

Premises used: tendsto_norm_atTop_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
Goal:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
⊢ Tendsto (b ^ exp) atTop atTop

Tactic:
(tendsto_rpow_atTop h_exp).comp h_tendsto

Premises used: tendsto_rpow_atTop, Filter.Tendsto.comp