-- 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
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)) ⋯)) ∧
                (basis_hd = basis_hd_1 ∧ basis_tl = basis_tl_1) ∧ ms ≍ mk (Multiseries.cons exp coef x) f
⊢ 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₁ : ∀ (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)) 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⟩