awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
⊢ s.leadingExp = ⊥ ↔ s = nil
have nil : leadingExp (basis_hd := basis_hd) (basis_tl := basis_tl) nil = ⊥ ↔ Eq (α := Multiseries basis_hd basis_tl) nil nil
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
nil :
  leadingExp (basis_hd := basis_hd) (basis_tl := basis_tl) Multiseries.nil = ⊥ ↔
    Eq (α := Multiseries basis_hd basis_tl) Multiseries.nil Multiseries.nil
⊢ s.leadingExp = ⊥ ↔ s = Multiseries.nil
have cons : ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
  (cons exp coef tl).leadingExp = ⊥ ↔ cons exp coef tl = Multiseries.nil
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ ms.seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) ms.seq
⊢ ms.seq.Sorted
have seq : ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ ms.seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) ms.seq
seq : ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted
⊢ ms.seq.Sorted
have seq₁ : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk ms.seq 0).seq
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.Sorted
⊢ ms.seq.Sorted
have h_coef : ∀ x ∈ ms.seq, x.2.Sorted
Tactic: cases h with | seq _ h_coef h_Pairwise =>
    constructor
    · simpa using h_coef
    · simpa using h_Pairwise
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.Sorted
h_coef : ∀ x ∈ ms.seq, x.2.Sorted
⊢ ms.seq.Sorted
have h_Pairwise : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) ms.seq
Tactic: cases h with | seq _ h_coef h_Pairwise =>
    constructor
    · simpa using h_coef
    · simpa using h_Pairwise
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk ms.seq 0).seq
⊢ ms.Sorted
have seq : ∀ x ∈ ms.seq, x.2.Sorted
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk ms.seq 0).seq
seq : ∀ x ∈ ms.seq, x.2.Sorted
⊢ ms.Sorted
have seq₁ : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) ms.seq
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.seq.Sorted
⊢ ms.Sorted
have h_coef : ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted
Tactic: cases h with | seq _ h_coef h_Pairwise =>
    constructor
    · simpa using h_coef
    · simpa using h_Pairwise
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.seq.Sorted
h_coef : ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted
⊢ ms.Sorted
have h_Pairwise : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk ms.seq 0).seq
Tactic: cases h with | seq _ h_coef h_Pairwise =>
    constructor
    · simpa using h_coef
    · simpa using h_Pairwise
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Sorted (basis_hd := basis_hd) (basis_tl := basis_tl) Multiseries.nil
have h_coef : ∀ (x : ℝ × MultiseriesExpansion basis_tl),
  Membership.mem (γ := Multiseries basis_hd basis_tl) (seq (mk Multiseries.nil 0)) x → x.2.Sorted
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
h_coef :
  ∀ (x : ℝ × MultiseriesExpansion basis_tl),
    Membership.mem (γ := Multiseries basis_hd basis_tl) (seq (mk Multiseries.nil 0)) x → x.2.Sorted
⊢ Sorted (basis_hd := basis_hd) (basis_tl := basis_tl) Multiseries.nil
have h_Pairwise : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (seq (mk Multiseries.nil 0))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
⊢ Sorted (basis_hd := basis_hd) (cons exp coef Multiseries.nil)
have h_coef₁ : ∀ (x : ℝ × MultiseriesExpansion basis_tl),
  Membership.mem (γ := Multiseries basis_hd basis_tl) (seq (mk (cons exp coef Multiseries.nil) 0)) x → x.2.Sorted
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
h_coef₁ :
  ∀ (x : ℝ × MultiseriesExpansion basis_tl),
    Membership.mem (γ := Multiseries basis_hd basis_tl) (seq (mk (cons exp coef Multiseries.nil) 0)) x → x.2.Sorted
⊢ Sorted (basis_hd := basis_hd) (cons exp coef Multiseries.nil)
have h_Pairwise : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (seq (mk (cons exp coef Multiseries.nil) 0))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < (↑exp : WithBot ℝ)
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk tl 0).seq
⊢ (Multiseries.cons exp coef tl).Sorted
have seq : ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < (↑exp : WithBot ℝ)
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk tl 0).seq
seq : ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted
⊢ (Multiseries.cons exp coef tl).Sorted
have seq₁ : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk (Multiseries.cons exp coef tl) 0).seq
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < (↑exp : WithBot ℝ)
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk tl 0).seq
⊢ ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted
have seq : ∀ (h_tl_coef : ∀ (a : ℝ) (b : MultiseriesExpansion basis_tl), (a, b) ∈ tl → b.Sorted),
  coef.Sorted ∧ ∀ (a : ℝ) (b : MultiseriesExpansion basis_tl), (a, b) ∈ tl → b.Sorted
Tactic: simp at h_tl_coef ⊢
Cleared hypotheses: h_tl_coef
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < (↑exp : WithBot ℝ)
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk tl 0).seq
⊢ Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk (Multiseries.cons exp coef tl) 0).seq
have seq : ∀ (h_comp : leadingExp (basis_hd := basis_hd) (basis_tl := basis_tl) Multiseries.nil < (↑exp : WithBot ℝ))
  (h_tl_coef :
    ∀ (x : ℝ × MultiseriesExpansion basis_tl),
      Membership.mem (γ := Multiseries basis_hd basis_tl) (seq (mk Multiseries.nil 0)) x → x.2.Sorted)
  (h_tl_tl : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (seq (mk Multiseries.nil 0))),
  Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2)
    (seq (mk (Multiseries.cons exp coef Multiseries.nil) 0))
Tactic: cases tl
Cleared hypotheses: tl, h_comp, h_tl_coef, h_tl_tl
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < (↑exp : WithBot ℝ)
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk tl 0).seq
seq :
  ∀ (h_comp : leadingExp (basis_hd := basis_hd) (basis_tl := basis_tl) Multiseries.nil < (↑exp : WithBot ℝ))
    (h_tl_coef :
      ∀ (x : ℝ × MultiseriesExpansion basis_tl),
        Membership.mem (γ := Multiseries basis_hd basis_tl) (MultiseriesExpansion.seq (mk Multiseries.nil 0)) x →
          x.2.Sorted)
    (h_tl_tl :
      Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2)
        (MultiseriesExpansion.seq (mk Multiseries.nil 0))),
    Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2)
      (MultiseriesExpansion.seq (mk (Multiseries.cons exp coef Multiseries.nil) 0))
⊢ Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk (Multiseries.cons exp coef tl) 0).seq
have seq₁ : ∀ (exp_1 : ℝ) (coef_1 : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl)
  (h_comp : (Multiseries.cons exp_1 coef_1 tl).leadingExp < (↑exp : WithBot ℝ))
  (h_tl_coef : ∀ x ∈ (mk (Multiseries.cons exp_1 coef_1 tl) 0).seq, x.2.Sorted)
  (h_tl_tl :
    Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2)
      (mk (Multiseries.cons exp_1 coef_1 tl) 0).seq),
  Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2)
    (mk (Multiseries.cons exp coef (Multiseries.cons exp_1 coef_1 tl)) 0).seq
Tactic: cases tl
Cleared hypotheses: tl, h_comp, h_tl_coef, h_tl_tl
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < (↑exp : WithBot ℝ)
h_tl : tl.Sorted
⊢ (Multiseries.cons exp coef tl).Sorted
have h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
Tactic: cases h_tl with | seq _ h_tl_coef h_tl_tl =>
  constructor
  · simp at h_tl_coef ⊢
    grind
  · cases tl
    · exact Seq.Pairwise_cons_nil
    · exact h_tl_tl.cons_cons_of_trans (by simpa [lt_iff_lt] using h_comp)
Cleared hypotheses: h_tl
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < (↑exp : WithBot ℝ)
h_tl : tl.Sorted
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
⊢ (Multiseries.cons exp coef tl).Sorted
have h_tl_tl : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk tl 0).seq
Tactic: cases h_tl with | seq _ h_tl_coef h_tl_tl =>
  constructor
  · simp at h_tl_coef ⊢
    grind
  · cases tl
    · exact Seq.Pairwise_cons_nil
    · exact h_tl_tl.cons_cons_of_trans (by simpa [lt_iff_lt] using h_comp)
Cleared hypotheses: h_tl
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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
⊢ coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ tl.Sorted
have seq : coef.Sorted
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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 : coef.Sorted
⊢ coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ tl.Sorted
have seq₁ : tl.leadingExp < (↑exp : WithBot ℝ) ∧ tl.Sorted
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
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 :
  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
have h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
Tactic: obtain ⟨h_all, h_Pairwise⟩ := h_Pairwise.cons_elim
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
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 :
  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
⊢ (Multiseries.cons tl_exp tl_coef tl_tl).leadingExp < (↑exp : WithBot ℝ) ∧
    (Multiseries.cons tl_exp tl_coef tl_tl).Sorted
have h_Pairwise₁ : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
Tactic: obtain ⟨h_all, h_Pairwise⟩ := h_Pairwise.cons_elim
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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).leadingExp < (↑exp : WithBot ℝ) ∧
    (Multiseries.cons tl_exp tl_coef tl_tl).Sorted
have seq : (Multiseries.cons tl_exp tl_coef tl_tl).leadingExp < (↑exp : WithBot ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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)
seq : (Multiseries.cons tl_exp tl_coef tl_tl).leadingExp < (↑exp : WithBot ℝ)
⊢ (Multiseries.cons tl_exp tl_coef tl_tl).leadingExp < (↑exp : WithBot ℝ) ∧
    (Multiseries.cons tl_exp tl_coef tl_tl).Sorted
have seq₁ : (Multiseries.cons tl_exp tl_coef tl_tl).Sorted
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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).leadingExp < (↑exp : WithBot ℝ)
have seq : tl_exp < exp
Tactic: simp only [leadingExp_cons, WithBot.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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
⊢ tl.leadingExp < (↑exp : WithBot ℝ) ∧ tl.Sorted
have seq : ∀
  (h_coef :
    ∀ (x : ℝ × MultiseriesExpansion basis_tl),
      Membership.mem (γ := Multiseries basis_hd basis_tl) (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)
      (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
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
Cleared hypotheses: tl, h_coef, h_Pairwise
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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
⊢ tl.leadingExp < (↑exp : WithBot ℝ) ∧ tl.Sorted
have 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
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
Cleared hypotheses: tl, h_coef, h_Pairwise
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : (Multiseries.cons exp coef tl).Sorted
⊢ coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ tl.Sorted
have h_coef : ∀ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (hypothesis)
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
⊢ coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ tl.Sorted
have h_Pairwise : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
h : ms.Sorted
⊢ ms.tail.Sorted
have 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)
Tactic: cases ms with
  | nil => simp
  | cons exp coef tl => simpa using h.elim_cons.right.right
Cleared hypotheses: ms, h