-- 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))
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
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)
hyp₂ :
  ∀ {basis_hd_1 f : ℝ → ℝ} {basis_tl_1 : Basis} {exp : ℝ} {coef : MultiseriesExpansion basis_tl_1}
    {tl : Multiseries basis_hd_1 basis_tl_1},
    coef.Approximates →
      Majorized f basis_hd_1 exp →
        (mk tl (f - basis_hd_1 ^ exp * coef.toFun)).Approximates →
          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 (mk (Multiseries.cons exp coef tl) f) (β := MultiseriesExpansion (basis_hd :: basis_tl))
                      (mk Multiseries.nil f_1)) ∨
              ∃ (basis_hd_2 : ℝ → ℝ) (f_1 : ℝ → ℝ) (basis_tl_2 : Basis) (exp_1 : ℝ) (coef_1 :
                MultiseriesExpansion basis_tl_2) (tl_1 : Multiseries basis_hd_2 basis_tl_2),
                (coef_1.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_1
                          h_basis)) ∧
                  Majorized f_1 basis_hd_2 exp_1 ∧
                    ((mk tl_1 (f_1 - basis_hd_2 ^ exp_1 * coef_1.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_1 (f_1 - basis_hd_2 ^ exp_1 * coef_1.toFun)) h_basis)) ∧
                      basis_hd_1 :: basis_tl_1 = basis_hd_2 :: basis_tl_2 ∧
                        mk (Multiseries.cons exp coef tl) f ≍ mk (Multiseries.cons exp_1 coef_1 tl_1) f_1
⊢ 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:
cases h_ms