awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ s.destruct =
    Option.map
      ((fun (x : ℝ × MultiseriesExpansion basis_tl × Multiseries basis_hd basis_tl) ↦ ((x.1, x.2.1), x.2.2)) ∘
        fun (x : Seq1 (ℝ × MultiseriesExpansion basis_tl)) ↦
        match (motive :=
          Seq1 (ℝ × MultiseriesExpansion basis_tl) → ℝ × MultiseriesExpansion basis_tl × Multiseries basis_hd basis_tl)
          x with
        | ((exp, coef), tl) => (exp, coef, tl))
      s.destruct

Tactic:
Option.map_id_apply.symm

Premises used: Option.map_id_apply, Stream'.Seq1, Eq.symm
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ s.destruct =
    Option.map
      ((fun (x : ℝ × MultiseriesExpansion basis_tl × Multiseries basis_hd basis_tl) ↦ ((x.1, x.2.1), x.2.2)) ∘
        fun (x : Seq1 (ℝ × MultiseriesExpansion basis_tl)) ↦
        match (motive :=
          Seq1 (ℝ × MultiseriesExpansion basis_tl) → ℝ × MultiseriesExpansion basis_tl × Multiseries basis_hd basis_tl)
          x with
        | ((exp, coef), tl) => (exp, coef, tl))
      s.destruct

Tactic:
exact Option.map_id_apply.symm

Premises used: Option.map_id_apply, Eq.symm
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
x y : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x y
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y →
      x = nil ∧ y = nil ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (x' : Multiseries basis_hd basis_tl) (y' :
          Multiseries basis_hd basis_tl), x = cons exp coef x' ∧ y = cons exp coef y' ∧ motive x' y'
⊢ ∀ (s₁ s₂ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive s₁ s₂ →
      s₁ = Seq.nil ∧ s₂ = Seq.nil ∨
        ∃ (x : ℝ × MultiseriesExpansion basis_tl) (s₁' : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)) (s₂' :
          Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)), s₁ = Seq.cons x s₁' ∧ s₂ = Seq.cons x s₂' ∧ motive s₁' s₂'

Tactic:
grind [nil, cons]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil, ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
x y : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x y
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y →
      x = y ∨
        ∃ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (x' : Multiseries basis_hd basis_tl) (y' :
          Multiseries basis_hd basis_tl), x = cons exp coef x' ∧ y = cons exp coef y' ∧ motive x' y'
⊢ ∀ (s₁ s₂ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive s₁ s₂ →
      s₁ = s₂ ∨
        ∃ (x : ℝ × MultiseriesExpansion basis_tl) (s₁' : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)) (s₂' :
          Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)), s₁ = Seq.cons x s₁' ∧ s₂ = Seq.cons x s₂' ∧ motive s₁' s₂'

Tactic:
grind [nil, cons]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil, ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : Seq.cons (exp, coef) tl = Seq.nil
⊢ False

Tactic:
apply Seq.cons_ne_nil h

Premises used: Stream'.Seq.cons_ne_nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
⊢ nil ≠ cons exp coef tl

Tactic:
cons_ne_nil.symm

Premises used: Ne.symm, ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons_ne_nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp1 exp2 : ℝ
coef1 coef2 : MultiseriesExpansion basis_tl
tl1 tl2 : Multiseries basis_hd basis_tl
rw : (exp1, coef1) = (exp2, coef2) ∧ tl1 = tl2 ↔ exp1 = exp2 ∧ coef1 = coef2 ∧ tl1 = tl2
⊢ cons exp1 coef1 tl1 = cons exp2 coef2 tl2 ↔ exp1 = exp2 ∧ coef1 = coef2 ∧ tl1 = tl2

Tactic:
rw [cons, cons, Seq.cons_eq_cons]

Premises used: Stream'.Seq.cons_eq_cons, ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp1 exp2 : ℝ
coef1 coef2 : MultiseriesExpansion basis_tl
tl1 tl2 : Multiseries basis_hd basis_tl
⊢ (exp1, coef1) = (exp2, coef2) ∧ tl1 = tl2 ↔ exp1 = exp2 ∧ coef1 = coef2 ∧ tl1 = tl2

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
β : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)
b : β
h : f b = none
h₁ :
  Eq (α := Option ((ℝ × MultiseriesExpansion basis_tl) × β))
    (Option.map (fun (x : ℝ × MultiseriesExpansion basis_tl × β) ↦ ((x.1, x.2.1), x.2.2)) (f b)) none
⊢ Eq (α := Multiseries basis_hd basis_tl)
    (Seq.corec
      (fun (a : β) ↦ Option.map (fun (x : ℝ × MultiseriesExpansion basis_tl × β) ↦ ((x.1, x.2.1), x.2.2)) (f a)) b)
    Seq.nil

Tactic:
rw [Seq.corec_nil]

Premises used: Stream'.Seq.corec_nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
β : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)
b : β
h : f b = none
⊢ Eq (α := Option ((ℝ × MultiseriesExpansion basis_tl) × β))
    (Option.map (fun (x : ℝ × MultiseriesExpansion basis_tl × β) ↦ ((x.1, x.2.1), x.2.2)) (f b)) none

Tactic:
simpa
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
β : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
next : β
f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)
b : β
h : f b = some (exp, coef, next)
rw :
  Option.map (fun (x : ℝ × MultiseriesExpansion basis_tl × β) ↦ ((x.1, x.2.1), x.2.2)) (f b) = some ((exp, coef), next)
⊢ Seq.corec (fun (a : β) ↦ Option.map (fun (x : ℝ × MultiseriesExpansion basis_tl × β) ↦ ((x.1, x.2.1), x.2.2)) (f a))
      b =
    Seq.cons (exp, coef)
      (Seq.corec
        (fun (a : β) ↦ Option.map (fun (x : ℝ × MultiseriesExpansion basis_tl × β) ↦ ((x.1, x.2.1), x.2.2)) (f a)) next)

Tactic:
rw [Seq.corec_cons]

Premises used: Stream'.Seq.corec_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
β : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
next : β
f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)
b : β
h : f b = some (exp, coef, next)
⊢ Option.map (fun (x : ℝ × MultiseriesExpansion basis_tl × β) ↦ ((x.1, x.2.1), x.2.2)) (f b) = some ((exp, coef), next)

Tactic:
simpa
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Eq (α := Option (ℝ × MultiseriesExpansion basis_tl × Multiseries basis_hd basis_tl)) (destruct nil) none

Tactic:
simp [destruct, nil]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil, ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct
-- 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).destruct = some (exp, coef, tl)

Tactic:
simp [destruct, cons]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons, ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
h : ms.destruct = none
a : Seq.destruct ms = none
⊢ ms = nil

Tactic:
apply Stream'.Seq.destruct_eq_none

Premises used: Stream'.Seq.destruct_eq_none
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
h : ms.destruct = none
⊢ Seq.destruct ms = none

Tactic:
simpa [destruct] using h

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : ms.destruct = some (exp, coef, tl)
a : Seq.destruct ms = some ((exp, coef), tl)
⊢ ms = cons exp coef tl

Tactic:
apply Stream'.Seq.destruct_eq_cons

Premises used: Stream'.Seq.destruct_eq_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : ms.destruct = some (exp, coef, tl)
a :
  Option.map
      (fun (x : ℝ × MultiseriesExpansion basis_tl × Multiseries basis_hd basis_tl) ↦
        match (motive :=
          ℝ × MultiseriesExpansion basis_tl × Multiseries basis_hd basis_tl → Seq1 (ℝ × MultiseriesExpansion basis_tl))
          x with
        | (exp, coef, tl) => ((exp, coef), tl))
      (some (exp, coef, tl)) =
    some ((exp, coef), tl)
⊢ Seq.destruct ms = some ((exp, coef), tl)

Tactic:
rw [destruct_eq_destruct_map, h]

Premises used: _private.0.ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct_eq_destruct_map
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : ms.destruct = some (exp, coef, tl)
⊢ Option.map
      (fun (x : ℝ × MultiseriesExpansion basis_tl × Multiseries basis_hd basis_tl) ↦
        match (motive :=
          ℝ × MultiseriesExpansion basis_tl × Multiseries basis_hd basis_tl → Seq1 (ℝ × MultiseriesExpansion basis_tl))
          x with
        | (exp, coef, tl) => ((exp, coef), tl))
      (some (exp, coef, tl)) =
    some ((exp, coef), tl)

Tactic:
rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Eq (α := Option (ℝ × MultiseriesExpansion basis_tl)) (head (basis_hd := basis_hd) nil) none

Tactic:
simp [head, nil]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil, ComputeAsymptotics.MultiseriesExpansion.Multiseries.head
-- 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).head = some (exp, coef)

Tactic:
simp [head, cons]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons, ComputeAsymptotics.MultiseriesExpansion.Multiseries.head
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Eq (α := Multiseries basis_hd basis_tl) (tail nil) nil

Tactic:
simp [tail, nil]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil, ComputeAsymptotics.MultiseriesExpansion.Multiseries.tail
-- 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).tail = tl

Tactic:
simp [tail, cons]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.tail, ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
basis_hd' : ℝ → ℝ
basis_tl' : Basis
f : ℝ → ℝ
g : MultiseriesExpansion basis_tl → MultiseriesExpansion basis_tl'
⊢ Eq (α := Multiseries basis_hd' basis_tl') (map (basis_hd := basis_hd) f g nil) nil

Tactic:
simp [map, nil]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil, ComputeAsymptotics.MultiseriesExpansion.Multiseries.map
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
basis_hd' : ℝ → ℝ
basis_tl' : Basis
f : ℝ → ℝ
g : MultiseriesExpansion basis_tl → MultiseriesExpansion basis_tl'
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
⊢ Eq (α := Multiseries basis_hd' basis_tl') (map f g (cons exp coef tl)) (cons (f exp) (g coef) (map f g tl))

Tactic:
simp [map, cons]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons, ComputeAsymptotics.MultiseriesExpansion.Multiseries.map
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
⊢ map (fun (exp : ℝ) ↦ exp) (fun (coef : MultiseriesExpansion basis_tl) ↦ coef) ms = ms

Tactic:
Stream'.Seq.map_id ms

Premises used: Stream'.Seq.map_id, ComputeAsymptotics.MultiseriesExpansion.Multiseries.map, ComputeAsymptotics.MultiseriesExpansion.Multiseries
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
b₁ b₂ b₃ : ℝ → ℝ
bs₁ bs₂ bs₃ : Basis
f₁ : ℝ → ℝ
g₁ : MultiseriesExpansion bs₁ → MultiseriesExpansion bs₂
f₂ : ℝ → ℝ
g₂ : MultiseriesExpansion bs₂ → MultiseriesExpansion bs₃
ms : Multiseries b₁ bs₁
simp :
  Eq (α := Multiseries b₃ bs₃) (Seq.map (fun (x : ℝ × MultiseriesExpansion bs₁) ↦ (f₂ (f₁ x.1), g₂ (g₁ x.2))) ms)
    (Seq.map
      ((fun (x : ℝ × MultiseriesExpansion bs₂) ↦ (f₂ x.1, g₂ x.2)) ∘ fun (x : ℝ × MultiseriesExpansion bs₁) ↦
        (f₁ x.1, g₁ x.2))
      ms)
⊢ Eq (α := Multiseries b₃ bs₃) (map (f₂ ∘ f₁) (g₂ ∘ g₁) ms) (map (basis_hd := b₂) f₂ g₂ (map f₁ g₁ ms))

Tactic:
simp [map, ← Stream'.Seq.map_comp]

Premises used: Stream'.Seq.map_comp, ComputeAsymptotics.MultiseriesExpansion.Multiseries.map
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
b₁ b₂ b₃ : ℝ → ℝ
bs₁ bs₂ bs₃ : Basis
f₁ : ℝ → ℝ
g₁ : MultiseriesExpansion bs₁ → MultiseriesExpansion bs₂
f₂ : ℝ → ℝ
g₂ : MultiseriesExpansion bs₂ → MultiseriesExpansion bs₃
ms : Multiseries b₁ bs₁
⊢ Eq (α := Multiseries b₃ bs₃) (Seq.map (fun (x : ℝ × MultiseriesExpansion bs₁) ↦ (f₂ (f₁ x.1), g₂ (g₁ x.2))) ms)
    (Seq.map
      ((fun (x : ℝ × MultiseriesExpansion bs₂) ↦ (f₂ x.1, g₂ x.2)) ∘ fun (x : ℝ × MultiseriesExpansion bs₁) ↦
        (f₁ x.1, g₁ x.2))
      ms)

Tactic:
rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
x : ℝ × MultiseriesExpansion basis_tl
⊢ x ∉ nil

Tactic:
Seq.notMem_nil _

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.toSeq, ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil, Stream'.Seq.notMem_nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
x : ℝ × MultiseriesExpansion basis_tl
⊢ x ∈ cons exp coef tl ↔ x = (exp, coef) ∨ x ∈ tl

Tactic:
Seq.mem_cons_iff

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.toSeq, Stream'.Seq.mem_cons_iff, ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
R : ℝ × MultiseriesExpansion basis_tl → ℝ × MultiseriesExpansion basis_tl → Prop
⊢ Seq.Pairwise R nil

Tactic:
simp [nil]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
R : ℝ × MultiseriesExpansion basis_tl → ℝ × MultiseriesExpansion basis_tl → Prop
exp : ℝ
coef : MultiseriesExpansion basis_tl
⊢ Seq.Pairwise R (cons exp coef nil)

Tactic:
simp [cons, nil]

Premises used: ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil, ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Sort u_1
nil : (f : ℝ → ℝ) → motive (mk Multiseries.nil f)
cons :
  (exp : ℝ) →
    (coef : MultiseriesExpansion basis_tl) →
      (tl : Multiseries basis_hd basis_tl) → (f : ℝ → ℝ) → motive (mk (Multiseries.cons exp coef tl) f)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
let : (s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)) → (f : ℝ → ℝ) → motive (s, f)
⊢ motive ms

Tactic:
let ⟨s, f⟩ := ms
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Sort u_1
nil : (f : ℝ → ℝ) → motive (mk Multiseries.nil f)
cons :
  (exp : ℝ) →
    (coef : MultiseriesExpansion basis_tl) →
      (tl : Multiseries basis_hd basis_tl) → (f : ℝ → ℝ) → motive (mk (Multiseries.cons exp coef tl) f)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
⊢ motive (Seq.nil, f)

Tactic:
apply nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Sort u_1
nil : (f : ℝ → ℝ) → motive (mk Multiseries.nil f)
cons :
  (exp : ℝ) →
    (coef : MultiseriesExpansion basis_tl) →
      (tl : Multiseries basis_hd basis_tl) → (f : ℝ → ℝ) → motive (mk (Multiseries.cons exp coef tl) f)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
hd : ℝ × MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ motive (Seq.cons hd tl, f)

Tactic:
apply cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Sort u_1
nil : (f : ℝ → ℝ) → motive (mk Multiseries.nil f)
cons :
  (exp : ℝ) →
    (coef : MultiseriesExpansion basis_tl) →
      (tl : Multiseries basis_hd basis_tl) → (f : ℝ → ℝ) → motive (mk (Multiseries.cons exp coef tl) f)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
f : ℝ → ℝ
nil₁ : motive (Seq.nil, f)
cons₁ :
  (hd : ℝ × MultiseriesExpansion basis_tl) →
    (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)) → motive (Seq.cons hd tl, f)
⊢ motive (s, f)

Tactic:
cases s with
  | nil => apply nil
  | cons hd tl => apply cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
⊢ ms = mk ms.seq ms.toFun

Tactic:
rfl

Premises used: ComputeAsymptotics.MultiseriesExpansion.toFun, ComputeAsymptotics.MultiseriesExpansion.seq, ComputeAsymptotics.MultiseriesExpansion.mk, rfl, ComputeAsymptotics.MultiseriesExpansion
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s t : Multiseries basis_hd basis_tl
f g : ℝ → ℝ
h : mk s f = mk t g
rwa : ∀ (h : (s, f) = mk t g), s = t ∧ f = g
rwa₁ : ∀ (h : (s, f) = (t, g)), s = t ∧ f = g
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : s = t ∧ f = g), s = t ∧ f = g
⊢ s = t ∧ f = g

Tactic:
rwa [mk, mk, Prod.mk_inj] at h

Premises used: Prod.mk_inj, ComputeAsymptotics.MultiseriesExpansion.mk
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s t : Multiseries basis_hd basis_tl
f g : ℝ → ℝ
h : s = t ∧ f = g
⊢ mk s f = mk t g

Tactic:
simp [h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
lhs : ms = mk s f
| ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f

Tactic:
lhs
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
lhs : ms
| ms = mk s f

Tactic:
lhs
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
rw : mk ms.seq ms.toFun
| ms

Tactic:
rw [eq_mk ms]

Premises used: ComputeAsymptotics.MultiseriesExpansion.eq_mk
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
rw : mk ms.seq ms.toFun
| ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f

Tactic:
lhs; lhs; rw [eq_mk ms]

Premises used: ComputeAsymptotics.MultiseriesExpansion.eq_mk
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
conv : mk ms.seq ms.toFun = mk s f ↔ ms.seq = s ∧ ms.toFun = f
⊢ ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f

Tactic:
conv => lhs; lhs; rw [eq_mk ms]

Premises used: ComputeAsymptotics.MultiseriesExpansion.eq_mk
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
rw rw₁ : ms.seq = s ∧ ms.toFun = f ↔ ms.seq = s ∧ ms.toFun = f
⊢ mk ms.seq ms.toFun = mk s f ↔ ms.seq = s ∧ ms.toFun = f

Tactic:
rw [mk_eq_mk_iff]

Premises used: ComputeAsymptotics.MultiseriesExpansion.mk_eq_mk_iff
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
rw : ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f
rw₁ rw₂ : ms.seq = s ∧ ms.toFun = f ↔ ms.seq = s ∧ ms.toFun = f
⊢ mk s f = ms ↔ ms.seq = s ∧ ms.toFun = f

Tactic:
rw [@Eq.comm _ (mk s f) ms, ms_eq_mk_iff]

Premises used: ComputeAsymptotics.MultiseriesExpansion.ms_eq_mk_iff, Eq.comm
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms₁ ms₂ : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms₁ = ms₂
⊢ ms₁.seq = ms₂.seq ∧ ms₁.toFun = ms₂.toFun

Tactic:
simp [h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms₁ ms₂ : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms₁.seq = ms₂.seq ∧ ms₁.toFun = ms₂.toFun
rw : mk ms₁.seq ms₁.toFun = mk ms₂.seq ms₂.toFun
⊢ ms₁ = ms₂

Tactic:
rw [eq_mk ms₁, eq_mk ms₂]

Premises used: ComputeAsymptotics.MultiseriesExpansion.eq_mk
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms₁ ms₂ : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms₁.seq = ms₂.seq ∧ ms₁.toFun = ms₂.toFun
⊢ mk ms₁.seq ms₁.toFun = mk ms₂.seq ms₂.toFun

Tactic:
simp [h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
ms : MultiseriesExpansion []
⊢ ms.toFun = fun (x : ℝ) ↦ ms.toReal

Tactic:
rfl

Premises used: ComputeAsymptotics.MultiseriesExpansion.toFun, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
⊢ (mk s f).toFun = f

Tactic:
rfl

Premises used: ComputeAsymptotics.MultiseriesExpansion.toFun, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
⊢ (mk s f).seq = s

Tactic:
rfl

Premises used: ComputeAsymptotics.MultiseriesExpansion.seq, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
f g : ℝ → ℝ
⊢ (mk s f).replaceFun g = mk s g

Tactic:
rfl

Premises used: ComputeAsymptotics.MultiseriesExpansion.replaceFun, ComputeAsymptotics.MultiseriesExpansion.seq, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
⊢ (ms.replaceFun f).toFun = f

Tactic:
rfl

Premises used: ComputeAsymptotics.MultiseriesExpansion.toFun, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
⊢ (ms.replaceFun f).seq = ms.seq

Tactic:
rfl

Premises used: ComputeAsymptotics.MultiseriesExpansion.replaceFun, ComputeAsymptotics.MultiseriesExpansion.seq, ComputeAsymptotics.MultiseriesExpansion.mk, rfl, ComputeAsymptotics.MultiseriesExpansion