-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms_1 : MultiseriesExpansion (basis_hd :: basis_tl)
f_1 : ℝ → ℝ
h_equiv : ms_1.toFun =ᶠ[atTop] f_1
h_approx_1 : ms_1.Approximates
motive : (ms : MultiseriesExpansion (basis_hd :: basis_tl)) → Prop :=
  fun (ms : MultiseriesExpansion (basis_hd :: basis_tl)) ↦
    ∃ (ms' : MultiseriesExpansion (basis_hd :: basis_tl)) (f' : ℝ → ℝ),
      ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_approx : ms.Approximates
h_eq : ms.toFun =ᶠ[atTop] f
nil :
  ∀ (g : ℝ → ℝ) (h_approx : Approximates (basis := basis_hd :: basis_tl) (mk Multiseries.nil g))
    (h_eq : toFun (basis := basis_hd :: basis_tl) (mk Multiseries.nil g) =ᶠ[atTop] f),
    Eq (α := Multiseries basis_hd basis_tl) (seq (replaceFun (mk Multiseries.nil g) f)) Multiseries.nil ∧
        toFun (basis := basis_hd :: basis_tl) (replaceFun (mk Multiseries.nil g) f) =ᶠ[atTop] 0 ∨
      ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
        seq (replaceFun (mk Multiseries.nil g) f) = Multiseries.cons exp coef tl ∧
          coef.Approximates ∧
            Majorized (toFun (basis := basis_hd :: basis_tl) (replaceFun (mk Multiseries.nil g) f)) basis_hd exp ∧
              motive
                (mk tl
                  (toFun (basis := basis_hd :: basis_tl) (replaceFun (mk Multiseries.nil g) f) -
                    basis_hd ^ exp * coef.toFun))
cons :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl) (g : ℝ → ℝ)
    (h_approx : (mk (Multiseries.cons exp coef tl) g).Approximates)
    (h_eq : (mk (Multiseries.cons exp coef tl) g).toFun =ᶠ[atTop] f),
    ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.nil ∧
        ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun =ᶠ[atTop] 0 ∨
      ∃ (exp_1 : ℝ) (coef_1 : MultiseriesExpansion basis_tl) (tl_1 : Multiseries basis_hd basis_tl),
        ((mk (Multiseries.cons exp coef tl) g).replaceFun f).seq = Multiseries.cons exp_1 coef_1 tl_1 ∧
          coef_1.Approximates ∧
            Majorized ((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun basis_hd exp_1 ∧
              motive
                (mk tl_1 (((mk (Multiseries.cons exp coef tl) g).replaceFun f).toFun - basis_hd ^ exp_1 * coef_1.toFun))
⊢ (ms.replaceFun f).seq = Multiseries.nil ∧ (ms.replaceFun f).toFun =ᶠ[atTop] 0 ∨
    ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
      (ms.replaceFun f).seq = Multiseries.cons exp coef tl ∧
        coef.Approximates ∧
          Majorized (ms.replaceFun f).toFun basis_hd exp ∧
            motive (mk tl ((ms.replaceFun f).toFun - basis_hd ^ exp * coef.toFun))

Tactic:
cases ms with
  | nil g =>
    simp only [nil_iff, mk_toFun, mk_replaceFun, mk_seq, true_and,
      Multiseries.nil_ne_cons, false_and, exists_const, or_false] at h_approx h_eq ⊢
    grw [← h_eq, h_approx]
  | cons exp coef tl g =>
    obtain ⟨h_coef, h_maj, h_tl⟩ := h_approx.elim_cons
    refine .inr ⟨exp, coef, tl, ?_⟩
    simp only [mk_replaceFun, mk_seq, h_coef, mk_toFun, true_and]
    simp only [mk_toFun] at h_eq
    refine ⟨h_maj.of_eventuallyEq h_eq.symm, mk tl (g - basis_hd ^ exp * coef.toFun), _, rfl,
      h_tl, ?_⟩
    grw [mk_toFun, h_eq]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Approximates.cons, ComputeAsymptotics.MultiseriesExpansion.mk_seq, false_and, ComputeAsymptotics.MultiseriesExpansion.Approximates.nil_iff, exists_const, ComputeAsymptotics.MultiseriesExpansion.mk_replaceFun, ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil_ne_cons, ComputeAsymptotics.MultiseriesExpansion.mk_toFun, or_false, ComputeAsymptotics.MultiseriesExpansion.Approximates.nil, true_and