awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ leadingExp (basis_hd := basis_hd) (basis_tl := basis_tl) nil = ⊥

Tactic:
rfl

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
⊢ (cons exp coef tl).leadingExp = (↑exp : WithBot ℝ)

Tactic:
rfl

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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
cons :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    (Multiseries.cons exp coef tl).leadingExp = ⊥ ↔ Multiseries.cons exp coef tl = Multiseries.nil
⊢ s.leadingExp = ⊥ ↔ s = Multiseries.nil

Tactic:
cases s
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ leadingExp (basis_hd := basis_hd) (basis_tl := basis_tl) nil = ⊥ ↔ Eq (α := Multiseries basis_hd basis_tl) nil 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
⊢ (cons exp coef tl).leadingExp = ⊥ ↔ cons exp coef tl = nil

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
⊢ ms.leadingExp = ms.seq.leadingExp

Tactic:
rfl

Premises used: ComputeAsymptotics.MultiseriesExpansion.leadingExp, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis : Basis
exp1 exp2 : ℝ
coef1 coef2 : MultiseriesExpansion basis
⊢ (exp1, coef1) < (exp2, coef2) ↔ exp1 < exp2

Tactic:
rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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
seq₁ : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk ms.seq 0).seq
⊢ ms.seq.Sorted

Tactic:
constructor
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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
⊢ ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted

Tactic:
simpa using h_coef
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk ms.seq 0).seq

Tactic:
simpa using h_Pairwise
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.Sorted
⊢ ∀ x ∈ ms.seq, x.2.Sorted

Tactic:
cases h with | seq _ h_coef h_Pairwise =>
    constructor
    · simpa using h_coef
    · simpa using h_Pairwise

Premises used: ComputeAsymptotics.MultiseriesExpansion.seq
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.Sorted
h_coef : ∀ x ∈ ms.seq, x.2.Sorted
⊢ 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

Premises used: ComputeAsymptotics.MultiseriesExpansion.seq
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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
seq₁ : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) ms.seq
⊢ ms.Sorted

Tactic:
constructor
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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
⊢ ∀ x ∈ ms.seq, x.2.Sorted

Tactic:
simpa using h_coef
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) ms.seq

Tactic:
simpa using h_Pairwise
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.seq.Sorted
⊢ ∀ 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

Premises used: ComputeAsymptotics.MultiseriesExpansion.seq
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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
⊢ 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

Premises used: ComputeAsymptotics.MultiseriesExpansion.seq
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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
h_Pairwise : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (seq (mk Multiseries.nil 0))
⊢ Sorted (basis_hd := basis_hd) (basis_tl := basis_tl) Multiseries.nil

Tactic:
constructor
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ (x : ℝ × MultiseriesExpansion basis_tl),
    Membership.mem (γ := Multiseries basis_hd basis_tl) (seq (mk Multiseries.nil 0)) x → x.2.Sorted

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (seq (mk Multiseries.nil 0))

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
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
h_Pairwise :
  Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (seq (mk (cons exp coef Multiseries.nil) 0))
⊢ Sorted (basis_hd := basis_hd) (cons exp coef Multiseries.nil)

Tactic:
constructor
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
⊢ ∀ (x : ℝ × MultiseriesExpansion basis_tl),
    Membership.mem (γ := Multiseries basis_hd basis_tl) (seq (mk (cons exp coef Multiseries.nil) 0)) x → x.2.Sorted

Tactic:
simpa
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
⊢ Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (seq (mk (cons exp coef Multiseries.nil) 0))

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_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
seq₁ :
  Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk (Multiseries.cons exp coef tl) 0).seq
⊢ (Multiseries.cons exp coef tl).Sorted

Tactic:
constructor
-- 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 : 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_tl_coef : ∀ (a : ℝ) (b : MultiseriesExpansion basis_tl), (a, b) ∈ tl → b.Sorted),
    coef.Sorted ∧ ∀ (a : ℝ) (b : MultiseriesExpansion basis_tl), (a, b) ∈ tl → b.Sorted
⊢ ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted

Tactic:
simp at h_tl_coef ⊢
-- 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 : coef.Sorted
h_comp : tl.leadingExp < (↑exp : WithBot ℝ)
h_tl_tl : Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk tl 0).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:
grind
-- 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 : 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₁ :
  ∀ (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
⊢ Seq.Pairwise (fun (x1 x2 : ℝ × MultiseriesExpansion basis_tl) ↦ x1 > x2) (mk (Multiseries.cons exp coef tl) 0).seq

Tactic:
cases tl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
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:
Seq.Pairwise_cons_nil

Premises used: Stream'.Seq.Pairwise_cons_nil, Stream'.Seq.cons, ComputeAsymptotics.MultiseriesExpansion.seq, ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
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:
exact Seq.Pairwise_cons_nil

Premises used: Stream'.Seq.Pairwise_cons_nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
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
⊢ (exp, coef) > (exp_1, coef_1)

Tactic:
simpa [lt_iff_lt] using h_comp

Premises used: _private.0.ComputeAsymptotics.MultiseriesExpansion.lt_iff_lt
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
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:
exact h_tl_tl.cons_cons_of_trans (by simpa [lt_iff_lt] using h_comp)

Premises used: Stream'.Seq.Pairwise.cons_cons_of_trans
-- 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 : coef.Sorted
h_comp : tl.leadingExp < (↑exp : WithBot ℝ)
h_tl : tl.Sorted
⊢ ∀ 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)

Premises used: Stream'.Seq.Pairwise_cons_nil, 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_coef : coef.Sorted
h_comp : tl.leadingExp < (↑exp : WithBot ℝ)
h_tl : tl.Sorted
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
⊢ 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)

Premises used: Stream'.Seq.Pairwise_cons_nil, 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_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
seq₁ : tl.leadingExp < (↑exp : WithBot ℝ) ∧ tl.Sorted
⊢ coef.Sorted ∧ tl.leadingExp < (↑exp : WithBot ℝ) ∧ tl.Sorted

Tactic:
constructor
-- 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
⊢ (exp, coef) ∈ (mk (Multiseries.cons exp coef tl) 0).seq

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_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

Tactic:
simpa using h_coef (exp, coef) (by simp)

Premises used: Prod.mk
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
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:
simp
-- 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 :
  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
⊢ ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x

Tactic:
obtain ⟨h_all, h_Pairwise⟩ := h_Pairwise.cons_elim

Premises used: Stream'.Seq.Pairwise.cons_elim
-- 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 :
  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
⊢ 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

Premises used: Stream'.Seq.Pairwise.cons_elim
-- 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)
seq : (Multiseries.cons tl_exp tl_coef tl_tl).leadingExp < (↑exp : WithBot ℝ)
seq₁ : (Multiseries.cons tl_exp tl_coef tl_tl).Sorted
⊢ (Multiseries.cons tl_exp tl_coef tl_tl).leadingExp < (↑exp : WithBot ℝ) ∧
    (Multiseries.cons tl_exp tl_coef tl_tl).Sorted

Tactic:
constructor
-- 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)
seq : tl_exp < exp
⊢ (Multiseries.cons tl_exp tl_coef tl_tl).leadingExp < (↑exp : WithBot ℝ)

Tactic:
simp only [leadingExp_cons, WithBot.coe_lt_coe]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.leadingExp_cons, WithBot.coe_lt_coe
-- 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)
⊢ (tl_exp, tl_coef) ∈ Multiseries.cons tl_exp tl_coef tl_tl

Tactic:
simp [Multiseries.cons]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons
-- 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)
⊢ tl_exp < exp

Tactic:
exact h_all (tl_exp, tl_coef) (by simp [Multiseries.cons])

Premises used: Prod.mk