awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise_1 :
  Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2)
    (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise :
  Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
x : ℝ × MultiseriesExpansion basis_tl
hx : x ∈ (mk (Multiseries.cons tl_exp tl_coef tl_tl) 0).seq
⊢ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq

Tactic:
simp_all
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise_1 :
  Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2)
    (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise :
  Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
⊢ (Multiseries.cons tl_exp tl_coef tl_tl).Sorted

Tactic:
exact Sorted.seq _ (fun x hx ↦ h_coef _ (by simp_all)) h_Pairwise
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted
h_Pairwise :
  Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk (Multiseries.cons exp coef tl) 0).seq
seq :
  ∀
    (h_coef :
      ∀ (x : ℝ × MultiseriesExpansion basis_tl),
        Membership.mem (γ := Multiseries basis_hd basis_tl)
            (MultiseriesExpansion.seq (mk (Multiseries.cons exp coef Multiseries.nil) 0)) x →
          x.2.Sorted)
    (h_Pairwise :
      Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2)
        (MultiseriesExpansion.seq (mk (Multiseries.cons exp coef Multiseries.nil) 0))),
    leadingExp (basis_hd := basis_hd) (basis_tl := basis_tl) Multiseries.nil < (↑exp : WithBot ℝ) ∧
      Sorted (basis_hd := basis_hd) (basis_tl := basis_tl) Multiseries.nil
seq₁ :
  ∀ (tl_exp : ℝ) (tl_coef : MultiseriesExpansion basis_tl) (tl_tl : Multiseries basis_hd basis_tl)
    (h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted)
    (h_Pairwise :
      Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2)
        (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq),
    (Multiseries.cons tl_exp tl_coef tl_tl).leadingExp < (↑exp : WithBot ℝ) ∧
      (Multiseries.cons tl_exp tl_coef tl_tl).Sorted
⊢ tl.leadingExp < (↑exp : WithBot ℝ) ∧ tl.Sorted

Tactic:
cases tl with
  | nil => simp
  | cons tl_exp tl_coef tl_tl =>
  obtain ⟨h_all, h_Pairwise⟩ := h_Pairwise.cons_elim
  constructor
  · simp only [leadingExp_cons, WithBot.coe_lt_coe]
    exact h_all (tl_exp, tl_coef) (by simp [Multiseries.cons])
  · exact Sorted.seq _ (fun x hx ↦ h_coef _ (by simp_all)) h_Pairwise

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.nil, ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp_cons, ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.cons, WithBot.coe_lt_coe, ComputeAsymptotics.MultiseriesExpansion.Sorted.seq, Stream'.Seq.Pairwise.cons_elim
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : (Multiseries.cons exp coef tl).Sorted
⊢ ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted

Tactic:
cases h with | seq _ h_coef h_Pairwise =>
  constructor
  · simpa using h_coef (exp, coef) (by simp)
  cases tl with
  | nil => simp
  | cons tl_exp tl_coef tl_tl =>
  obtain ⟨h_all, h_Pairwise⟩ := h_Pairwise.cons_elim
  constructor
  · simp only [leadingExp_cons, WithBot.coe_lt_coe]
    exact h_all (tl_exp, tl_coef) (by simp [Multiseries.cons])
  · exact Sorted.seq _ (fun x hx ↦ h_coef _ (by simp_all)) h_Pairwise

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.nil, ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp_cons, ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.cons, WithBot.coe_lt_coe, ComputeAsymptotics.MultiseriesExpansion.seq
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : (Multiseries.cons exp coef tl).Sorted
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted
⊢ Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk (Multiseries.cons exp coef tl) 0).seq

Tactic:
cases h with | seq _ h_coef h_Pairwise =>
  constructor
  · simpa using h_coef (exp, coef) (by simp)
  cases tl with
  | nil => simp
  | cons tl_exp tl_coef tl_tl =>
  obtain ⟨h_all, h_Pairwise⟩ := h_Pairwise.cons_elim
  constructor
  · simp only [leadingExp_cons, WithBot.coe_lt_coe]
    exact h_all (tl_exp, tl_coef) (by simp [Multiseries.cons])
  · exact Sorted.seq _ (fun x hx ↦ h_coef _ (by simp_all)) h_Pairwise

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.nil, ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp_cons, ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.cons, WithBot.coe_lt_coe, ComputeAsymptotics.MultiseriesExpansion.seq
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
h : Sorted (basis_hd := basis_hd) (basis_tl := basis_tl) Multiseries.nil
⊢ Sorted (basis_hd := basis_hd) (basis_tl := basis_tl) (Multiseries.tail Multiseries.nil)

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : (Multiseries.cons exp coef tl).Sorted
⊢ (Multiseries.cons exp coef tl).tail.Sorted

Tactic:
simpa using h.elim_cons.right.right

Premises used: And.right, ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.elim_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
h : ms.Sorted
nil :
  ∀ (h : Sorted (basis_hd := basis_hd) (basis_tl := basis_tl) Multiseries.nil),
    Sorted (basis_hd := basis_hd) (basis_tl := basis_tl) (Multiseries.tail Multiseries.nil)
cons :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl)
    (h : (Multiseries.cons exp coef tl).Sorted), (Multiseries.cons exp coef tl).tail.Sorted
⊢ ms.tail.Sorted

Tactic:
cases ms with
  | nil => simp
  | cons exp coef tl => simpa using h.elim_cons.right.right

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.nil, ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
h_coef : ∀ x ∈ (mk s 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk s 0).seq
⊢ s.Sorted

Tactic:
constructor
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
h_coef : motive (mk s 0).seq
h_coef₁ :
  ∀ (hd : ℝ × MultiseriesExpansion basis_tl) (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive (Seq.cons hd tl) → hd.2.Sorted ∧ motive tl
h_coef₂ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Prop
⊢ ∀ x ∈ (mk s 0).seq, x.2.Sorted

Tactic:
apply Seq.all_coind

Premises used: Stream'.Seq.all_coind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
⊢ motive (mk s 0).seq

Tactic:
h_base

Premises used: ComputeAsymptotics.MultiseriesExpansion.seq
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
⊢ motive (mk s 0).seq

Tactic:
exact h_base
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
⊢ (exp, coef).2.Sorted ∧ motive tl

Tactic:
grind [h_step exp coef tl h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
h_Pairwise : motive (mk s 0).seq
h_Pairwise₁ :
  ∀ (hd : ℝ × MultiseriesExpansion basis_tl) (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive (Seq.cons hd tl) → (∀ x ∈ tl.head, hd > x) ∧ motive tl
h_Pairwise₂ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Prop
⊢ Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk s 0).seq

Tactic:
apply Seq.Pairwise.coind_trans

Premises used: Stream'.Seq.Pairwise.coind_trans
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
h_Pairwise : ∀ x ∈ tl.head, (exp, coef) > x
h_Pairwise₁ : motive tl
⊢ (∀ x ∈ tl.head, (exp, coef) > x) ∧ motive tl

Tactic:
constructor
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
h_Pairwise : tl_exp < exp
⊢ (exp, coef) > (tl_exp, tl_coef)

Tactic:
rw [gt_iff_lt, lt_iff_lt]

Premises used: _private.0.ComputeAsymptotics.MultiseriesExpansion.lt_iff_lt, gt_iff_lt
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
⊢ leadingExp (basis_hd := basis_hd) tl < (↑exp : WithBot ℝ)

Tactic:
replace h_step := (h_step exp coef tl h).right.left
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
h_step : leadingExp (basis_hd := basis_hd) tl < (↑exp : WithBot ℝ)
h_Pairwise :
  ∀ (h : motive (Seq.cons (exp, coef) Seq.nil))
    (h_tl : Membership.mem (γ := Option (ℝ × MultiseriesExpansion basis_tl)) (Seq.head Seq.nil) (tl_exp, tl_coef))
    (h_step : leadingExp (basis_hd := basis_hd) (basis_tl := basis_tl) Seq.nil < (↑exp : WithBot ℝ)), tl_exp < exp
h_Pairwise₁ :
  ∀ (x : ℝ × MultiseriesExpansion basis_tl) (s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl))
    (h : motive (Seq.cons (exp, coef) (Seq.cons x s))) (h_tl : (tl_exp, tl_coef) ∈ (Seq.cons x s).head)
    (h_step : leadingExp (basis_hd := basis_hd) (Seq.cons x s) < (↑exp : WithBot ℝ)), tl_exp < exp
⊢ tl_exp < exp

Tactic:
cases tl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h : motive (Seq.cons (exp, coef) Seq.nil)
h_tl : Membership.mem (γ := Option (ℝ × MultiseriesExpansion basis_tl)) (Seq.head Seq.nil) (tl_exp, tl_coef)
h_step : leadingExp (basis_hd := basis_hd) (basis_tl := basis_tl) Seq.nil < (↑exp : WithBot ℝ)
⊢ tl_exp < exp

Tactic:
simp [leadingExp, head] at h_tl h_step

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp, ComputeAsymptotics.MultiseriesExpansion.Multiseries.head
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
x : ℝ × MultiseriesExpansion basis_tl
s_1 : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) (Seq.cons x s_1))
h_tl : (tl_exp, tl_coef) ∈ (Seq.cons x s_1).head
h_step : leadingExp (basis_hd := basis_hd) (Seq.cons x s_1) < (↑exp : WithBot ℝ)
⊢ x = (tl_exp, tl_coef)

Tactic:
simp [leadingExp, head] at h_tl h_step

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp, ComputeAsymptotics.MultiseriesExpansion.Multiseries.head
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
x : ℝ × MultiseriesExpansion basis_tl
s_1 : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) (Seq.cons x s_1))
h_tl : (tl_exp, tl_coef) ∈ (Seq.cons x s_1).head
h_step : leadingExp (basis_hd := basis_hd) (Seq.cons x s_1) < (↑exp : WithBot ℝ)
h_tl₁ : x = (tl_exp, tl_coef)
⊢ x.1 < exp

Tactic:
simp [leadingExp, head] at h_tl h_step

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp, ComputeAsymptotics.MultiseriesExpansion.Multiseries.head
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
x : ℝ × MultiseriesExpansion basis_tl
s_1 : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) (Seq.cons x s_1))
h_tl : x = (tl_exp, tl_coef)
h_step : x.1 < exp
⊢ tl_exp < exp

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : (ms : Multiseries basis_hd basis_tl) → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
⊢ motive tl

Tactic:
grind [h_step exp coef tl h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
f : ℝ → ℝ
⊢ Sorted (basis := basis_hd :: basis_tl) (mk Multiseries.nil f)

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
f : ℝ → ℝ
h_coef : coef.Sorted
⊢ Sorted (basis := basis_hd :: basis_tl) (mk (Multiseries.cons exp coef Multiseries.nil) f)

Tactic:
simp [Multiseries.Sorted.cons_nil h_coef]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.cons_nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h_coef : coef.Sorted
h_comp : tl.leadingExp < (↑exp : WithBot ℝ)
h_tl : tl.Sorted
⊢ (mk (Multiseries.cons exp coef tl) f).Sorted

Tactic:
simp [Multiseries.Sorted.cons h_coef h_comp h_tl]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (mk (Multiseries.cons exp coef tl) f).Sorted
⊢ (Multiseries.cons exp coef tl).Sorted

Tactic:
simpa using h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (mk (Multiseries.cons exp coef tl) f).Sorted
⊢ coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ tl.Sorted

Tactic:
apply Multiseries.Sorted.elim_cons (by simpa using h)

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.elim_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_sorted : ms.Sorted
⊢ (ms.replaceFun f).Sorted

Tactic:
simpa using h_sorted
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
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 : 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))
hyp :
  ∀ {basis : Basis} (ms : MultiseriesExpansion basis),
    (ms.Approximates ∨
        ∃ (h_basis : basis = basis_hd :: basis_tl),
          motive (Eq.rec (motive := fun (x : Basis) (h : basis = x) ↦ MultiseriesExpansion x) ms h_basis)) →
      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
x :
  ms.Approximates ∨
    ∃ (h_basis : basis_hd :: basis_tl = basis_hd :: basis_tl),
      motive (Eq.rec (motive := fun (x : Basis) (h : basis_hd :: basis_tl = x) ↦ MultiseriesExpansion x) ms h_basis)
⊢ ms.Approximates

Tactic:
apply coinduct fun {basis} ms =>
    ms.Approximates ∨ ∃ (h_basis : basis = basis_hd :: basis_tl), (motive (h_basis ▸ ms))

Premises used: Exists, Eq.rec, ComputeAsymptotics.MultiseriesExpansion.Approximates, ComputeAsymptotics.MultiseriesExpansion.Approximates.coinduct, Or