-- 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
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
⊢ 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₁ : ∀ {basis_hd_1 : ℝ → ℝ} {basis_tl_1 : Basis} {f : ℝ → ℝ},
  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: cases h_ms
Cleared hypotheses: basis, ms, h_ms