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

pp: case x
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.Approximates ∨ ∃ (h_basis : basis_hd :: basis_tl = basis_hd :: basis_tl), motive (h_basis ▸ ms)

Tactic:
·

Goal state after:
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