Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case hyp
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef 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),
    (ms.Approximates ∨ ∃ (h_basis : basis = basis_hd :: basis_tl), motive (h_basis ▸ ms)) →
      basis = [] ∨
        (∃ basis_hd basis_tl f, f =ᶠ[atTop] 0 ∧ basis = basis_hd :: basis_tl ∧ ms ≍ mk Multiseries.nil f) ∨
          ∃ basis_hd_1 f basis_tl_1 exp coef tl,
            (coef.Approximates ∨ ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl), motive (h_basis ▸ coef)) ∧
              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 (h_basis ▸ mk tl (f - basis_hd_1 ^ exp * coef.toFun))) ∧
                  basis = basis_hd_1 :: basis_tl_1 ∧ ms ≍ mk (Multiseries.cons exp coef tl) f

Tactic:
rintro basis ms (h_ms | ⟨rfl, h_ms⟩)

Goal state after:
case hyp.inl
basis_hd : ℝ → ℝ
basis_tl : Basis
ms✝ : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms✝
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef 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
⊢ basis = [] ∨
    (∃ basis_hd basis_tl f, f =ᶠ[atTop] 0 ∧ basis = basis_hd :: basis_tl ∧ ms ≍ mk Multiseries.nil f) ∨
      ∃ basis_hd_1 f basis_tl_1 exp coef tl,
        (coef.Approximates ∨ ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl), motive (h_basis ▸ coef)) ∧
          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 (h_basis ▸ mk tl (f - basis_hd_1 ^ exp * coef.toFun))) ∧
              basis = basis_hd_1 :: basis_tl_1 ∧ ms ≍ mk (Multiseries.cons exp coef tl) f

case hyp.inr
basis_hd : ℝ → ℝ
basis_tl : Basis
ms✝ : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms✝
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef 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)
⊢ basis_hd :: basis_tl = [] ∨
    (∃ basis_hd_1 basis_tl_1 f,
        f =ᶠ[atTop] 0 ∧ basis_hd :: basis_tl = basis_hd_1 :: basis_tl_1 ∧ ms ≍ mk Multiseries.nil f) ∨
      ∃ basis_hd_1 f basis_tl_1 exp coef tl,
        (coef.Approximates ∨ ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl), motive (h_basis ▸ coef)) ∧
          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 (h_basis ▸ mk tl (f - basis_hd_1 ^ exp * coef.toFun))) ∧
              basis_hd :: basis_tl = basis_hd_1 :: basis_tl_1 ∧ ms ≍ mk (Multiseries.cons exp coef tl) f