Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case hyp.inl.const
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 f, f =ᶠ[atTop] 0 ∧ [] = 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_hd_1 :: basis_tl_1 ∧ ms✝ ≍ mk (Multiseries.cons exp coef tl) f

pp: case hyp.inl.nil
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_hd✝ : ℝ → ℝ
basis_tl✝ : Basis
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
⊢ basis_hd✝ :: basis_tl✝ = [] ∨
    (∃ basis_hd basis_tl f,
        f =ᶠ[atTop] 0 ∧ basis_hd✝ :: basis_tl✝ = basis_hd :: basis_tl ∧ mk Multiseries.nil f✝ ≍ 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 ∧
                mk Multiseries.nil f✝ ≍ mk (Multiseries.cons exp coef tl) f

pp: case hyp.inl.cons
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_hd✝ f✝ : ℝ → ℝ
basis_tl✝ : Basis
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl✝
tl✝ : Multiseries basis_hd✝ basis_tl✝
h_coef✝ : coef✝.Approximates
h_maj✝ : Majorized f✝ basis_hd✝ exp✝
h_tl✝ : (mk tl✝ (f✝ - basis_hd✝ ^ exp✝ * coef✝.toFun)).Approximates
⊢ basis_hd✝ :: basis_tl✝ = [] ∨
    (∃ basis_hd basis_tl f,
        f =ᶠ[atTop] 0 ∧
          basis_hd✝ :: basis_tl✝ = basis_hd :: basis_tl ∧
            mk (Multiseries.cons exp✝ coef✝ tl✝) f✝ ≍ 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 ∧
                mk (Multiseries.cons exp✝ coef✝ tl✝) f✝ ≍ mk (Multiseries.cons exp coef tl) f

Tactic:
<;>

Goal state after:
case hyp.inl.const
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 f, f =ᶠ[atTop] 0 ∧ [] = 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_hd_1 :: basis_tl_1 ∧ ms✝ ≍ mk (Multiseries.cons exp coef tl) f

case hyp.inl.nil
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_hd✝ : ℝ → ℝ
basis_tl✝ : Basis
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
⊢ basis_hd✝ :: basis_tl✝ = [] ∨
    (∃ basis_hd basis_tl f,
        f =ᶠ[atTop] 0 ∧ basis_hd✝ :: basis_tl✝ = basis_hd :: basis_tl ∧ mk Multiseries.nil f✝ ≍ 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 ∧
                mk Multiseries.nil f✝ ≍ mk (Multiseries.cons exp coef tl) f

case hyp.inl.cons
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_hd✝ f✝ : ℝ → ℝ
basis_tl✝ : Basis
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl✝
tl✝ : Multiseries basis_hd✝ basis_tl✝
h_coef✝ : coef✝.Approximates
h_maj✝ : Majorized f✝ basis_hd✝ exp✝
h_tl✝ : (mk tl✝ (f✝ - basis_hd✝ ^ exp✝ * coef✝.toFun)).Approximates
⊢ basis_hd✝ :: basis_tl✝ = [] ∨
    (∃ basis_hd basis_tl f,
        f =ᶠ[atTop] 0 ∧
          basis_hd✝ :: basis_tl✝ = basis_hd :: basis_tl ∧
            mk (Multiseries.cons exp✝ coef✝ tl✝) f✝ ≍ 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 ∧
                mk (Multiseries.cons exp✝ coef✝ tl✝) f✝ ≍ mk (Multiseries.cons exp coef tl) f