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)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms_1 : MultiseriesExpansion []
⊢ Eq (α := Basis) [] [] ∨
    (∃ (basis_hd : ℝ → ℝ) (basis_tl : Basis) (f : ℝ → ℝ),
        f =ᶠ[atTop] 0 ∧
          [] = basis_hd :: basis_tl ∧
            HEq ms_1 (β := MultiseriesExpansion (basis_hd :: basis_tl)) (mk Multiseries.nil f)) ∨
      ∃ (basis_hd_1 : ℝ → ℝ) (f : ℝ → ℝ) (basis_tl_1 : Basis) (exp : ℝ) (coef : MultiseriesExpansion basis_tl_1) (tl :
        Multiseries basis_hd_1 basis_tl_1),
        (coef.Approximates ∨
            ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl),
              motive (Eq.rec (motive := fun (x : Basis) (h : basis_tl_1 = x) ↦ MultiseriesExpansion x) coef h_basis)) ∧
          Majorized f basis_hd_1 exp ∧
            ((mk tl (f - basis_hd_1 ^ exp * coef.toFun)).Approximates ∨
                ∃ (h_basis : basis_hd_1 :: basis_tl_1 = basis_hd :: basis_tl),
                  motive
                    (Eq.rec (motive := fun (x : Basis) (h : basis_hd_1 :: basis_tl_1 = x) ↦ MultiseriesExpansion x)
                      (mk tl (f - basis_hd_1 ^ exp * coef.toFun)) h_basis)) ∧
              [] = basis_hd_1 :: basis_tl_1 ∧ ms_1 ≍ mk (Multiseries.cons exp coef tl) f

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
basis_hd_1 : ℝ → ℝ
basis_tl_1 : Basis
f : ℝ → ℝ
hf : f =ᶠ[atTop] 0
⊢ basis_hd_1 :: basis_tl_1 = [] ∨
    (∃ (basis_hd : ℝ → ℝ) (basis_tl : Basis) (f_1 : ℝ → ℝ),
        f_1 =ᶠ[atTop] 0 ∧
          basis_hd_1 :: basis_tl_1 = basis_hd :: basis_tl ∧
            HEq (α := MultiseriesExpansion (basis_hd_1 :: basis_tl_1)) (mk Multiseries.nil f) (β :=
              MultiseriesExpansion (basis_hd :: basis_tl)) (mk Multiseries.nil f_1)) ∨
      ∃ (basis_hd_2 : ℝ → ℝ) (f_1 : ℝ → ℝ) (basis_tl_2 : Basis) (exp : ℝ) (coef : MultiseriesExpansion basis_tl_2) (tl :
        Multiseries basis_hd_2 basis_tl_2),
        (coef.Approximates ∨
            ∃ (h_basis : basis_tl_2 = basis_hd :: basis_tl),
              motive (Eq.rec (motive := fun (x : Basis) (h : basis_tl_2 = x) ↦ MultiseriesExpansion x) coef h_basis)) ∧
          Majorized f_1 basis_hd_2 exp ∧
            ((mk tl (f_1 - basis_hd_2 ^ exp * coef.toFun)).Approximates ∨
                ∃ (h_basis : basis_hd_2 :: basis_tl_2 = basis_hd :: basis_tl),
                  motive
                    (Eq.rec (motive := fun (x : Basis) (h : basis_hd_2 :: basis_tl_2 = x) ↦ MultiseriesExpansion x)
                      (mk tl (f_1 - basis_hd_2 ^ exp * coef.toFun)) h_basis)) ∧
              basis_hd_1 :: basis_tl_1 = basis_hd_2 :: basis_tl_2 ∧
                HEq (α := MultiseriesExpansion (basis_hd_1 :: basis_tl_1)) (mk Multiseries.nil f)
                  (mk (Multiseries.cons exp coef tl) f_1)

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
basis_hd_1 f : ℝ → ℝ
basis_tl_1 : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl_1
tl : Multiseries basis_hd_1 basis_tl_1
h_coef : coef.Approximates
h_maj : Majorized f basis_hd_1 exp
h_tl : (mk tl (f - basis_hd_1 ^ exp * coef.toFun)).Approximates
⊢ basis_hd_1 :: basis_tl_1 = [] ∨
    (∃ (basis_hd : ℝ → ℝ) (basis_tl : Basis) (f_1 : ℝ → ℝ),
        f_1 =ᶠ[atTop] 0 ∧
          basis_hd_1 :: basis_tl_1 = basis_hd :: basis_tl ∧
            HEq (mk (Multiseries.cons exp coef tl) f) (β := MultiseriesExpansion (basis_hd :: basis_tl))
              (mk Multiseries.nil f_1)) ∨
      ∃ (basis_hd_2 : ℝ → ℝ) (f_1 : ℝ → ℝ) (basis_tl_2 : Basis) (exp_1 : ℝ) (coef_1 : MultiseriesExpansion basis_tl_2)
        (tl_1 : Multiseries basis_hd_2 basis_tl_2),
        (coef_1.Approximates ∨
            ∃ (h_basis : basis_tl_2 = basis_hd :: basis_tl),
              motive
                (Eq.rec (motive := fun (x : Basis) (h : basis_tl_2 = x) ↦ MultiseriesExpansion x) coef_1 h_basis)) ∧
          Majorized f_1 basis_hd_2 exp_1 ∧
            ((mk tl_1 (f_1 - basis_hd_2 ^ exp_1 * coef_1.toFun)).Approximates ∨
                ∃ (h_basis : basis_hd_2 :: basis_tl_2 = basis_hd :: basis_tl),
                  motive
                    (Eq.rec (motive := fun (x : Basis) (h : basis_hd_2 :: basis_tl_2 = x) ↦ MultiseriesExpansion x)
                      (mk tl_1 (f_1 - basis_hd_2 ^ exp_1 * coef_1.toFun)) h_basis)) ∧
              basis_hd_1 :: basis_tl_1 = basis_hd_2 :: basis_tl_2 ∧
                mk (Multiseries.cons exp coef tl) f ≍ mk (Multiseries.cons exp_1 coef_1 tl_1) f_1

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms_1 : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms_1
h_step_1 :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
h_step : ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0
⊢ ms.toFun =ᶠ[atTop] 0 ∧ ms.seq = Multiseries.nil ∨
    ∃ (basis_hd_1 : ℝ → ℝ) (f : ℝ → ℝ) (basis_tl_1 : Basis) (exp : ℝ) (coef : MultiseriesExpansion basis_tl_1),
      (coef.Approximates ∨
          ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl),
            motive (Eq.rec (motive := fun (x : Basis) (h : basis_tl_1 = x) ↦ MultiseriesExpansion x) coef h_basis)) ∧
        Majorized f basis_hd_1 exp ∧
          ∃ (x : Multiseries basis_hd_1 basis_tl_1),
            ((mk x (f - basis_hd_1 ^ exp * coef.toFun)).Approximates ∨
                ∃ (h : basis_hd_1 = basis_hd ∧ basis_tl_1 = basis_tl),
                  motive
                    (Eq.rec (motive := fun (x : Basis) (h : basis_hd_1 :: basis_tl_1 = x) ↦ MultiseriesExpansion x)
                      (mk x (f - basis_hd_1 ^ exp * coef.toFun)) ⋯)) ∧
              (basis_hd = basis_hd_1 ∧ basis_tl = basis_tl_1) ∧ ms ≍ mk (Multiseries.cons exp coef x) f

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms_1 : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms_1
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_seq : ms.seq = Multiseries.cons exp coef tl
h_coef : coef.Approximates
h_maj : Majorized ms.toFun basis_hd exp
h_tl : motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ coef.Approximates ∨
    ∃ (h_basis : basis_tl = basis_hd :: basis_tl),
      motive (Eq.rec (motive := fun (x : Basis) (h : basis_tl = x) ↦ MultiseriesExpansion x) coef h_basis)

Tactic:
simpa
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms_1 : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms_1
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_seq : ms.seq = Multiseries.cons exp coef tl
h_coef : coef.Approximates
h_maj : Majorized ms.toFun basis_hd exp
h_tl : motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
hyp :
  ((mk tl (ms.toFun - basis_hd ^ exp * coef.toFun)).Approximates ∨
      ∃ (h : basis_hd = basis_hd ∧ basis_tl = basis_tl),
        motive
          (Eq.rec (motive := fun (x : Basis) (h : basis_hd :: basis_tl = x) ↦ MultiseriesExpansion x)
            (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun)) ⋯)) ∧
    (basis_hd = basis_hd ∧ basis_tl = basis_tl) ∧ ms ≍ mk (Multiseries.cons exp coef tl) ms.toFun
⊢ ms.toFun =ᶠ[atTop] 0 ∧ ms.seq = Multiseries.nil ∨
    ∃ (basis_hd_1 : ℝ → ℝ) (f : ℝ → ℝ) (basis_tl_1 : Basis) (exp : ℝ) (coef : MultiseriesExpansion basis_tl_1),
      (coef.Approximates ∨
          ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl),
            motive (Eq.rec (motive := fun (x : Basis) (h : basis_tl_1 = x) ↦ MultiseriesExpansion x) coef h_basis)) ∧
        Majorized f basis_hd_1 exp ∧
          ∃ (x : Multiseries basis_hd_1 basis_tl_1),
            ((mk x (f - basis_hd_1 ^ exp * coef.toFun)).Approximates ∨
                ∃ (h : basis_hd_1 = basis_hd ∧ basis_tl_1 = basis_tl),
                  motive
                    (Eq.rec (motive := fun (x : Basis) (h : basis_hd_1 :: basis_tl_1 = x) ↦ MultiseriesExpansion x)
                      (mk x (f - basis_hd_1 ^ exp * coef.toFun)) ⋯)) ∧
              (basis_hd = basis_hd_1 ∧ basis_tl = basis_tl_1) ∧ ms ≍ mk (Multiseries.cons exp coef x) f

Tactic:
refine .inr ⟨basis_hd, ms.toFun, basis_tl, exp, coef, by simpa, ‹_›, tl, ?_⟩
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms_1 : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms_1
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_seq : ms.seq = Multiseries.cons exp coef tl
h_coef : coef.Approximates
h_maj : Majorized ms.toFun basis_hd exp
h_tl : motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
hyp :
  ((mk tl (ms.toFun - basis_hd ^ exp * coef.toFun)).Approximates ∨
      motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))) ∧
    ms.seq = Multiseries.cons exp coef tl
⊢ ((mk tl (ms.toFun - basis_hd ^ exp * coef.toFun)).Approximates ∨
      ∃ (h : basis_hd = basis_hd ∧ basis_tl = basis_tl),
        motive
          (Eq.rec (motive := fun (x : Basis) (h : basis_hd :: basis_tl = x) ↦ MultiseriesExpansion x)
            (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun)) ⋯)) ∧
    (basis_hd = basis_hd ∧ basis_tl = basis_tl) ∧ ms ≍ mk (Multiseries.cons exp coef tl) ms.toFun

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms_1 : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms_1
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_seq : ms.seq = Multiseries.cons exp coef tl
h_coef : coef.Approximates
h_maj : Majorized ms.toFun basis_hd exp
h_tl : motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ((mk tl (ms.toFun - basis_hd ^ exp * coef.toFun)).Approximates ∨
      motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))) ∧
    ms.seq = Multiseries.cons exp coef tl

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ms.Approximates ∨
    ∃ (h_basis : basis_hd :: basis_tl = basis_hd :: basis_tl),
      motive (Eq.rec (motive := fun (x : Basis) (h : basis_hd :: basis_tl = x) ↦ MultiseriesExpansion x) ms h_basis)

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
h : Approximates (basis := basis_hd :: basis_tl) (mk Multiseries.nil f)
generalize :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)) (h_ms : mk Multiseries.nil f = ms) (h : ms.Approximates),
    f =ᶠ[atTop] 0
⊢ f =ᶠ[atTop] 0

Tactic:
generalize h_ms : (mk .nil f) = ms at h

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil, ComputeAsymptotics.MultiseriesExpansion.mk
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : mk Multiseries.nil f = ms
h : ms.Approximates
nil :
  ∀ {f_1 : ℝ → ℝ},
    f_1 =ᶠ[atTop] 0 →
      ∀ (h_ms : Eq (α := MultiseriesExpansion (basis_hd :: basis_tl)) (mk Multiseries.nil f) (mk Multiseries.nil f_1)),
        f =ᶠ[atTop] 0
cons :
  ∀ {f_1 : ℝ → ℝ} {exp : ℝ},
    Majorized f_1 basis_hd exp →
      ∀ {coef : MultiseriesExpansion basis_tl},
        coef.Approximates →
          ∀ {tl : Multiseries basis_hd basis_tl},
            (mk tl (f_1 - basis_hd ^ exp * coef.toFun)).Approximates →
              ∀ (h_ms : mk Multiseries.nil f = mk (Multiseries.cons exp coef tl) f_1), f =ᶠ[atTop] 0
⊢ f =ᶠ[atTop] 0

Tactic:
cases h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
f_1 : ℝ → ℝ
hf : f_1 =ᶠ[atTop] 0
h_ms : Eq (α := MultiseriesExpansion (basis_hd :: basis_tl)) (mk Multiseries.nil f) (mk Multiseries.nil f_1)
⊢ f = f_1

Tactic:
simp at h_ms
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
f_1 : ℝ → ℝ
exp : ℝ
h_maj : Majorized f_1 basis_hd exp
coef : MultiseriesExpansion basis_tl
h_coef : coef.Approximates
tl : Multiseries basis_hd basis_tl
h_tl : (mk tl (f_1 - basis_hd ^ exp * coef.toFun)).Approximates
h_ms : mk Multiseries.nil f = mk (Multiseries.cons exp coef tl) f_1
⊢ f =ᶠ[atTop] 0

Tactic:
simp at h_ms
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
f_1 : ℝ → ℝ
hf : f_1 =ᶠ[atTop] 0
h_ms : f = f_1
⊢ f =ᶠ[atTop] 0

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
f : ℝ → ℝ
⊢ Approximates (basis := basis_hd :: basis_tl) (mk Multiseries.nil f) ↔ f =ᶠ[atTop] 0

Tactic:
⟨elim_nil, nil⟩

Premises used: ComputeAsymptotics.MultiseriesExpansion.Approximates.elim_nil, Iff.intro, ComputeAsymptotics.MultiseriesExpansion.Approximates.nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : (mk (Multiseries.cons exp coef tl) f).Approximates
generalize :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)) (h_ms : mk (Multiseries.cons exp coef tl) f = ms)
    (h : ms.Approximates),
    coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
generalize h_ms : (mk (.cons exp coef tl) f) = ms at h

Premises used: ComputeAsymptotics.MultiseriesExpansion.mk, ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : mk (Multiseries.cons exp coef tl) f = ms
h : ms.Approximates
nil :
  ∀ {f_1 : ℝ → ℝ},
    f_1 =ᶠ[atTop] 0 →
      ∀ (h_ms : mk (Multiseries.cons exp coef tl) f = mk Multiseries.nil f_1),
        coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
cons :
  ∀ {f_1 : ℝ → ℝ} {exp_1 : ℝ},
    Majorized f_1 basis_hd exp_1 →
      ∀ {coef_1 : MultiseriesExpansion basis_tl},
        coef_1.Approximates →
          ∀ {tl_1 : Multiseries basis_hd basis_tl},
            (mk tl_1 (f_1 - basis_hd ^ exp_1 * coef_1.toFun)).Approximates →
              ∀ (h_ms : mk (Multiseries.cons exp coef tl) f = mk (Multiseries.cons exp_1 coef_1 tl_1) f_1),
                coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
cases h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f_1 : ℝ → ℝ
hf : f_1 =ᶠ[atTop] 0
h_ms : mk (Multiseries.cons exp coef tl) f = mk Multiseries.nil f_1
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
simp at h_ms
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f_1 : ℝ → ℝ
exp_1 : ℝ
h_maj : Majorized f_1 basis_hd exp_1
coef_1 : MultiseriesExpansion basis_tl
h_coef : coef_1.Approximates
tl_1 : Multiseries basis_hd basis_tl
h_tl : (mk tl_1 (f_1 - basis_hd ^ exp_1 * coef_1.toFun)).Approximates
h_ms : mk (Multiseries.cons exp coef tl) f = mk (Multiseries.cons exp_1 coef_1 tl_1) f_1
⊢ (exp = exp_1 ∧ coef = coef_1 ∧ tl = tl_1) ∧ f = f_1

Tactic:
simp at h_ms
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f_1 : ℝ → ℝ
exp_1 : ℝ
h_maj : Majorized f_1 basis_hd exp_1
coef_1 : MultiseriesExpansion basis_tl
h_coef : coef_1.Approximates
tl_1 : Multiseries basis_hd basis_tl
h_tl : (mk tl_1 (f_1 - basis_hd ^ exp_1 * coef_1.toFun)).Approximates
h_ms : (exp = exp_1 ∧ coef = coef_1 ∧ tl = tl_1) ∧ f = f_1
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f
h_approx : 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'
⊢ ms.replaceFun f = ms.replaceFun f ∧ ms.Approximates ∧ ms.toFun =ᶠ[atTop] f

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f
h_approx : 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'
apply :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ (ms.replaceFun f).Approximates

Tactic:
apply Approximates.coind motive ⟨ms, f, by grind⟩

Premises used: ComputeAsymptotics.MultiseriesExpansion.Approximates.coind, Exists.intro