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_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
⊢ 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
have hyp : ∀ (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)) sorry)) ∧
              (basis_hd = basis_hd_1 ∧ basis_tl = basis_tl_1) ∧ ms ≍ mk (Multiseries.cons exp coef x) f
Tactic: rcases h_step _ h_ms with h_step | ⟨exp, coef, tl, h_seq, h_coef, h_maj, h_tl⟩
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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))
⊢ 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
have 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)) sorry)) ∧
  (basis_hd = basis_hd ∧ basis_tl = basis_tl) ∧ ms ≍ mk (Multiseries.cons exp coef tl) ms.toFun
Tactic: refine .inr ⟨basis_hd, ms.toFun, basis_tl, exp, coef, by simpa, ‹_›, tl, ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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 ∨
      ∃ (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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
h : Approximates (basis := basis_hd :: basis_tl) (mk Multiseries.nil f)
⊢ f =ᶠ[atTop] 0
have generalize : ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)) (h_ms : mk Multiseries.nil f = ms) (h : ms.Approximates),
  f =ᶠ[atTop] 0
Tactic: generalize h_ms : (mk .nil f) = ms at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
f basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : mk Multiseries.nil f = ms
h : ms.Approximates
⊢ f =ᶠ[atTop] 0
have 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
Tactic: cases h
Cleared hypotheses: ms, h_ms, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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
⊢ f =ᶠ[atTop] 0
have 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
Tactic: cases h
Cleared hypotheses: ms, h_ms, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
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 =ᶠ[atTop] 0
have h_ms₁ : f = f_1
Tactic: simp at h_ms
Cleared hypotheses: h_ms
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
have 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
Tactic: generalize h_ms : (mk (.cons exp coef tl) f) = ms at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
have 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
Tactic: cases h
Cleared hypotheses: ms, h_ms, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
have 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
Tactic: cases h
Cleared hypotheses: ms, h_ms, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
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
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
have h_ms₁ : (exp = exp_1 ∧ coef = coef_1 ∧ tl = tl_1) ∧ f = f_1
Tactic: simp at h_ms
Cleared hypotheses: h_ms
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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).Approximates
have 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))
Tactic: apply Approximates.coind motive ⟨ms, f, by grind⟩
-- 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 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))
have nil : ∀ (h_approx : g =ᶠ[atTop] 0), f =ᶠ[atTop] 0
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 ⊢
Cleared hypotheses: h_approx
-- 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 g : ℝ → ℝ
h_eq : g =ᶠ[atTop] f
h_approx nil : g =ᶠ[atTop] 0
⊢ f =ᶠ[atTop] 0
have nil₁ : EventuallyEq (α := ℝ) (β := ℝ) atTop 0 0
Tactic: grw [← h_eq, h_approx]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
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
⊢ ((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))
have h_coef : coef.Approximates
Tactic: obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
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
⊢ ((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))
have h_maj : Majorized g basis_hd exp
Tactic: obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
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 (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))
have h_tl : (mk tl (g - basis_hd ^ exp * coef.toFun)).Approximates
Tactic: obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons
-- 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 : (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))
have 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))
Tactic: refine .inr ⟨exp, coef, tl, ?_⟩
-- 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 : (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.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))
have cons : Majorized f basis_hd exp ∧ motive (mk tl (f - basis_hd ^ exp * coef.toFun))
Tactic: simp only [mk_replaceFun, mk_seq, h_coef, mk_toFun, true_and]
-- 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
⊢ Majorized f basis_hd exp ∧ motive (mk tl (f - basis_hd ^ exp * coef.toFun))
have cons : (mk tl (g - basis_hd ^ exp * coef.toFun)).toFun =ᶠ[atTop] 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, ?_⟩