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 : Multiseries basis_hd basis_tl
h : ms.Sorted
nil :
  ∀ (h : Sorted (basis_hd := basis_hd) (basis_tl := basis_tl) Multiseries.nil),
    Sorted (basis_hd := basis_hd) (basis_tl := basis_tl) (Multiseries.tail Multiseries.nil)
⊢ ms.tail.Sorted
have cons : ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl)
  (h : (Multiseries.cons exp coef tl).Sorted), (Multiseries.cons exp coef tl).tail.Sorted
Tactic: cases ms with
  | nil => simp
  | cons exp coef tl => simpa using h.elim_cons.right.right
Cleared hypotheses: ms, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
⊢ s.Sorted
have h_coef : ∀ x ∈ (mk s 0).seq, x.2.Sorted
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
h_coef : ∀ x ∈ (mk s 0).seq, x.2.Sorted
⊢ s.Sorted
have h_Pairwise : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk s 0).seq
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
⊢ ∀ x ∈ (mk s 0).seq, x.2.Sorted
have h_coef : motive (mk s 0).seq
Tactic: apply Seq.all_coind
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
h_coef : motive (mk s 0).seq
⊢ ∀ x ∈ (mk s 0).seq, x.2.Sorted
have h_coef₁ : ∀ (hd : ℝ × MultiseriesExpansion basis_tl) (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
  motive (Seq.cons hd tl) → hd.2.Sorted ∧ motive tl
Tactic: apply Seq.all_coind
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
h_coef : motive (mk s 0).seq
h_coef₁ :
  ∀ (hd : ℝ × MultiseriesExpansion basis_tl) (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive (Seq.cons hd tl) → hd.2.Sorted ∧ motive tl
⊢ ∀ x ∈ (mk s 0).seq, x.2.Sorted
have h_coef₂ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Prop
Tactic: apply Seq.all_coind
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
⊢ Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk s 0).seq
have h_Pairwise : motive (mk s 0).seq
Tactic: apply Seq.Pairwise.coind_trans
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
h_Pairwise : motive (mk s 0).seq
⊢ Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk s 0).seq
have h_Pairwise₁ : ∀ (hd : ℝ × MultiseriesExpansion basis_tl) (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
  motive (Seq.cons hd tl) → (∀ x ∈ tl.head, hd > x) ∧ motive tl
Tactic: apply Seq.Pairwise.coind_trans
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
h_Pairwise : motive (mk s 0).seq
h_Pairwise₁ :
  ∀ (hd : ℝ × MultiseriesExpansion basis_tl) (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive (Seq.cons hd tl) → (∀ x ∈ tl.head, hd > x) ∧ motive tl
⊢ Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk s 0).seq
have h_Pairwise₂ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Prop
Tactic: apply Seq.Pairwise.coind_trans
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
⊢ (∀ x ∈ tl.head, (exp, coef) > x) ∧ motive tl
have h_Pairwise : ∀ x ∈ tl.head, (exp, coef) > x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
h_Pairwise : ∀ x ∈ tl.head, (exp, coef) > x
⊢ (∀ x ∈ tl.head, (exp, coef) > x) ∧ motive tl
have h_Pairwise₁ : motive tl
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
⊢ (exp, coef) > (tl_exp, tl_coef)
have h_Pairwise : tl_exp < exp
Tactic: rw [gt_iff_lt, lt_iff_lt]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
⊢ tl_exp < exp
have h_step₁ : leadingExp (basis_hd := basis_hd) tl < (↑exp : WithBot ℝ)
Tactic: replace h_step := (h_step exp coef tl h).right.left
Cleared hypotheses: h_step
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
h_step : leadingExp (basis_hd := basis_hd) tl < (↑exp : WithBot ℝ)
⊢ tl_exp < exp
have h_Pairwise : ∀ (h : motive (Seq.cons (exp, coef) Seq.nil))
  (h_tl : Membership.mem (γ := Option (ℝ × MultiseriesExpansion basis_tl)) (Seq.head Seq.nil) (tl_exp, tl_coef))
  (h_step : leadingExp (basis_hd := basis_hd) (basis_tl := basis_tl) Seq.nil < (↑exp : WithBot ℝ)), tl_exp < exp
Tactic: cases tl
Cleared hypotheses: tl, h, h_tl, h_step
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
h_step : leadingExp (basis_hd := basis_hd) tl < (↑exp : WithBot ℝ)
h_Pairwise :
  ∀ (h : motive (Seq.cons (exp, coef) Seq.nil))
    (h_tl : Membership.mem (γ := Option (ℝ × MultiseriesExpansion basis_tl)) (Seq.head Seq.nil) (tl_exp, tl_coef))
    (h_step : leadingExp (basis_hd := basis_hd) (basis_tl := basis_tl) Seq.nil < (↑exp : WithBot ℝ)), tl_exp < exp
⊢ tl_exp < exp
have h_Pairwise₁ : ∀ (x : ℝ × MultiseriesExpansion basis_tl) (s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl))
  (h : motive (Seq.cons (exp, coef) (Seq.cons x s))) (h_tl : (tl_exp, tl_coef) ∈ (Seq.cons x s).head)
  (h_step : leadingExp (basis_hd := basis_hd) (Seq.cons x s) < (↑exp : WithBot ℝ)), tl_exp < exp
Tactic: cases tl
Cleared hypotheses: tl, h, h_tl, h_step
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
x : ℝ × MultiseriesExpansion basis_tl
s_1 : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) (Seq.cons x s_1))
h_tl : (tl_exp, tl_coef) ∈ (Seq.cons x s_1).head
h_step : leadingExp (basis_hd := basis_hd) (Seq.cons x s_1) < (↑exp : WithBot ℝ)
⊢ tl_exp < exp
have h_tl₁ : x = (tl_exp, tl_coef)
Tactic: simp [leadingExp, head] at h_tl h_step
Cleared hypotheses: h_tl, h_step
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
x : ℝ × MultiseriesExpansion basis_tl
s_1 : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) (Seq.cons x s_1))
h_tl : (tl_exp, tl_coef) ∈ (Seq.cons x s_1).head
h_step : leadingExp (basis_hd := basis_hd) (Seq.cons x s_1) < (↑exp : WithBot ℝ)
h_tl₁ : x = (tl_exp, tl_coef)
⊢ tl_exp < exp
have h_step₁ : x.1 < exp
Tactic: simp [leadingExp, head] at h_tl h_step
Cleared hypotheses: h_tl, h_step
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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
have hyp : ∀ {basis : Basis} (ms : MultiseriesExpansion basis),
  (ms.Approximates ∨
      ∃ (h_basis : basis = basis_hd :: basis_tl),
        motive (Eq.rec (motive := fun (x : Basis) (h : basis = x) ↦ MultiseriesExpansion x) ms h_basis)) →
    basis = [] ∨
      (∃ (basis_hd : ℝ → ℝ) (basis_tl : Basis) (f : ℝ → ℝ),
          f =ᶠ[atTop] 0 ∧
            basis = basis_hd :: basis_tl ∧
              HEq ms (β := 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 = basis_hd_1 :: basis_tl_1 ∧ ms ≍ mk (Multiseries.cons exp coef tl) f
Tactic: apply coinduct fun {basis} ms =>
    ms.Approximates ∨ ∃ (h_basis : basis = basis_hd :: basis_tl), (motive (h_basis ▸ ms))
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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))
hyp :
  ∀ {basis : Basis} (ms : MultiseriesExpansion basis),
    (ms.Approximates ∨
        ∃ (h_basis : basis = basis_hd :: basis_tl),
          motive (Eq.rec (motive := fun (x : Basis) (h : basis = x) ↦ MultiseriesExpansion x) ms h_basis)) →
      basis = [] ∨
        (∃ (basis_hd : ℝ → ℝ) (basis_tl : Basis) (f : ℝ → ℝ),
            f =ᶠ[atTop] 0 ∧
              basis = basis_hd :: basis_tl ∧
                HEq ms (β := 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 = basis_hd_1 :: basis_tl_1 ∧ ms ≍ mk (Multiseries.cons exp coef tl) f
⊢ ms.Approximates
have x : 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: apply coinduct fun {basis} ms =>
    ms.Approximates ∨ ∃ (h_basis : basis = basis_hd :: basis_tl), (motive (h_basis ▸ ms))
-- 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))
basis : Basis
ms : MultiseriesExpansion basis
h_ms : ms.Approximates
⊢ basis = [] ∨
    (∃ (basis_hd : ℝ → ℝ) (basis_tl : Basis) (f : ℝ → ℝ),
        f =ᶠ[atTop] 0 ∧
          basis = basis_hd :: basis_tl ∧
            HEq ms (β := 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 = basis_hd_1 :: basis_tl_1 ∧ ms ≍ mk (Multiseries.cons exp coef tl) f
have hyp : ∀ (ms : MultiseriesExpansion []),
  Eq (α := Basis) [] [] ∨
    (∃ (basis_hd : ℝ → ℝ) (basis_tl : Basis) (f : ℝ → ℝ),
        f =ᶠ[atTop] 0 ∧
          [] = basis_hd :: basis_tl ∧
            HEq ms (β := 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 ≍ mk (Multiseries.cons exp coef tl) f
Tactic: cases h_ms
Cleared hypotheses: basis, ms, h_ms
-- 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 (Eq.rec (motive := fun (x : Basis) (h : basis_hd :: basis_tl = x) ↦ MultiseriesExpansion x) ms ⋯)
⊢ basis_hd :: basis_tl = [] ∨
    (∃ (basis_hd_1 : ℝ → ℝ) (basis_tl_1 : Basis) (f : ℝ → ℝ),
        f =ᶠ[atTop] 0 ∧
          basis_hd :: basis_tl = basis_hd_1 :: basis_tl_1 ∧
            HEq ms (β := MultiseriesExpansion (basis_hd_1 :: basis_tl_1)) (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 :: basis_tl = basis_hd_1 :: basis_tl_1 ∧ ms ≍ mk (Multiseries.cons exp coef tl) f
have hyp : 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: simp only [reduceCtorEq, List.cons.injEq, ↓existsAndEq, and_true, heq_eq_eq, ms_eq_mk_iff,
      true_and, exists_eq_right_right', exists_and_left, false_or] at h_ms ⊢