-- 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 (Eq.rec (motive := fun (x : Basis) (h : basis_hd :: basis_tl = x) ↦ MultiseriesExpansion x) ms ⋯)
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)) ⋯)) ∧
              (basis_hd = basis_hd_1 ∧ basis_tl = basis_tl_1) ∧ ms ≍ mk (Multiseries.cons exp coef x) f
⊢ 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

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 ⊢

Premises used: reduceCtorEq, and_true, heq_eq_eq, exists_and_left, ExistsAndEq.existsAndEq, false_or, ComputeAsymptotics.MultiseriesExpansion.ms_eq_mk_iff, List.cons.injEq, exists_eq_right_right', true_and