awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl t : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = t
x : α
s : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = Seq.cons x s
this : (Seq.cons x s).head = t.head
cons :
  ∀ (ht : op (Seq.cons s_hd s_tl) = nil) (this : (Seq.cons x s).head = Seq.head nil),
    Eq.{u_1 + 1} (α := Option (Seq1 α)) (destruct nil)
      (Option.map
        (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
          (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) s_tl))
        (match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          (Seq.cons x s).destruct with
        | none => none
        | some (t_hd, snd) =>
          some
            (t_hd,
              Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) ⋯)))
⊢ t.destruct =
    Option.map
      (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) s_tl))
      (match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        (Seq.cons x s).destruct with
      | none => none
      | some (t_hd, snd) =>
        some
          (t_hd, Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) ⋯))
have cons₁ : ∀ (x_1 : α) (s_1 : Stream'.Seq α) (ht : op (Seq.cons s_hd s_tl) = Seq.cons x_1 s_1)
  (this : (Seq.cons x s).head = (Seq.cons x_1 s_1).head),
  (Seq.cons x_1 s_1).destruct =
    Option.map
      (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) s_tl))
      (match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        (Seq.cons x s).destruct with
      | none => none
      | some (t_hd, snd) =>
        some
          (t_hd, Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) sorry))
Tactic: cases t with
      | nil => simp at this
      | cons => simp_all
Cleared hypotheses: t, ht, this
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl t0 : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = t0
t : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = t
this : t0.head = t.head
⊢ t.destruct =
    Option.map
      (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) s_tl))
      (match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        t0.destruct with
      | none => none
      | some (t_hd, snd) =>
        some
          (t_hd, Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) ⋯))
have cons : ∀ (ht0 : op (Seq.cons s_hd nil) = nil) (this : Seq.head nil = t.head),
  t.destruct =
    Option.map
      (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) s_tl))
      (match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        destruct nil with
      | none => none
      | some (t_hd, snd) =>
        some
          (t_hd, Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) sorry))
Tactic: cases t0 with
    | nil =>
      cases t with
      | nil => simp
      | cons => simp at this
    | cons =>
      cases t with
      | nil => simp at this
      | cons => simp_all
Cleared hypotheses: t0, ht0, this
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl t0 : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = t0
t : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = t
this : t0.head = t.head
cons :
  ∀ (ht0 : op (Seq.cons s_hd nil) = nil) (this : Seq.head nil = t.head),
    t.destruct =
      Option.map
        (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
          (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) s_tl))
        (match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          destruct nil with
        | none => none
        | some (t_hd, snd) =>
          some
            (t_hd, Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) ⋯))
⊢ t.destruct =
    Option.map
      (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) s_tl))
      (match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        t0.destruct with
      | none => none
      | some (t_hd, snd) =>
        some
          (t_hd, Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) ⋯))
have cons₁ : ∀ (x : α) (s : Stream'.Seq α) (ht0 : op (Seq.cons s_hd nil) = Seq.cons x s) (this : (Seq.cons x s).head = t.head),
  t.destruct =
    Option.map
      (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) s_tl))
      (match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        (Seq.cons x s).destruct with
      | none => none
      | some (t_hd, snd) =>
        some
          (t_hd, Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) sorry))
Tactic: cases t0 with
    | nil =>
      cases t with
      | nil => simp
      | cons => simp at this
    | cons =>
      cases t with
      | nil => simp at this
      | cons => simp_all
Cleared hypotheses: t0, ht0, this
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s : Stream'.Seq α
⊢ (op s).destruct =
    Option.map
      (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        match (motive := α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation → Seq1 α) x with
        | (hd, op') => (hd, (↑op' : Stream'.Seq α → Stream'.Seq α) s.tail))
      (match (motive := Option α → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        s.head with
      | none =>
        match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          (op nil).destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, Subtype.mk (p := FriendlyOperation) (fun (x : Stream'.Seq α) ↦ t_tl) ⋯)
      | some s_hd =>
        match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) =>
          some
            (t_hd, Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) ⋯))
have nil : (op nil).destruct =
  Option.map
    (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
      match (motive := α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation → Seq1 α) x with
      | (hd, op') => (hd, (↑op' : Stream'.Seq α → Stream'.Seq α) (Seq.tail nil)))
    (match (motive := Option α → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
      Seq.head nil with
    | none =>
      match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        (op nil).destruct with
      | none => none
      | some (t_hd, t_tl) => some (t_hd, Subtype.mk (p := FriendlyOperation) (fun (x : Stream'.Seq α) ↦ t_tl) sorry)
    | some s_hd =>
      match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        (op (Seq.cons s_hd nil)).destruct with
      | none => none
      | some (t_hd, snd) =>
        some
          (t_hd, Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) sorry))
Tactic: cases s with
  | nil =>
    generalize op nil = t
    cases t <;> simp
  | cons s_hd s_tl =>
    simp only [Seq.tail_cons, Seq.head_cons]
    generalize ht0 : op (.cons s_hd nil) = t0 at *
    generalize ht : op (.cons s_hd s_tl) = t at *
    have : t0.head = t.head := by
      rw [← ht0, ← ht, FriendlyOperation.op_cons_head_eq h]
    cases t0 with
    | nil =>
      cases t with
      | nil => simp
      | cons => simp at this
    | cons =>
      cases t with
      | nil => simp at this
      | cons => simp_all
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s t : Stream'.Seq α
h_head : s.head = t.head
⊢ (op s).head = (op t).head
have simp : ∀ (h_head : Option.map Prod.fst s.destruct = Option.map Prod.fst t.destruct),
  Eq (α := Option α)
    (Option.map
      (Function.comp (β := α × Stream'.Seq α) Prod.fst
        fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) s.tail))
      (h.unfold (Option.map Prod.fst s.destruct)))
    (Option.map
      (Function.comp (β := α × Stream'.Seq α) Prod.fst
        fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) t.tail))
      (h.unfold (Option.map Prod.fst t.destruct)))
Tactic: simp only [head_eq_destruct, Option.map_eq_map, h.destruct_apply_eq_unfold, Option.map_map]
    at h_head ⊢
Cleared hypotheses: h_head
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s t : Stream'.Seq α
h_head : Option.map Prod.fst s.destruct = Option.map Prod.fst t.destruct
⊢ Eq (α := Option α)
    (Option.map
      (Function.comp (β := α × Stream'.Seq α) Prod.fst
        fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) s.tail))
      (h.unfold (Option.map Prod.fst s.destruct)))
    (Option.map
      (Function.comp (β := α × Stream'.Seq α) Prod.fst
        fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) t.tail))
      (h.unfold (Option.map Prod.fst t.destruct)))
have simp : Eq (α := Option α)
  (Option.map
    (Function.comp (β := α × Stream'.Seq α) Prod.fst
      fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
      (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) s.tail))
    (h.unfold (Option.map Prod.fst t.destruct)))
  (Option.map
    (Function.comp (β := α × Stream'.Seq α) Prod.fst
      fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
      (x.1, (↑x.2 : Stream'.Seq α → Stream'.Seq α) t.tail))
    (h.unfold (Option.map Prod.fst t.destruct)))
Tactic: simp [h_head]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ HPow.hPow (α := ℝ) 2⁻¹ n → dist (op s) (op t) ≤ HPow.hPow (α := ℝ) 2⁻¹ n
⊢ FriendlyOperation op
have rw : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
Tactic: rw [friendlyOperation_iff_dist_le_dist]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ HPow.hPow (α := ℝ) 2⁻¹ n → dist (op s) (op t) ≤ HPow.hPow (α := ℝ) 2⁻¹ n
s t : Stream'.Seq α
⊢ dist (op s) (op t) ≤ dist s t
have pos : ∀ (hst : s = t), dist (op s) (op t) ≤ dist s t
Tactic: by_cases hst : s = t
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ HPow.hPow (α := ℝ) 2⁻¹ n → dist (op s) (op t) ≤ HPow.hPow (α := ℝ) 2⁻¹ n
s t : Stream'.Seq α
pos : ∀ (hst : s = t), dist (op s) (op t) ≤ dist s t
⊢ dist (op s) (op t) ≤ dist s t
have neg : ∀ (hst : ¬s = t), dist (op s) (op t) ≤ dist s t
Tactic: by_cases hst : s = t
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ HPow.hPow (α := ℝ) 2⁻¹ n → dist (op s) (op t) ≤ HPow.hPow (α := ℝ) 2⁻¹ n
s t : Stream'.Seq α
hst : ¬s = t
⊢ dist (op s) (op t) ≤ dist s t
have neg : ∀ (n : ℕ) (hst : dist s t = HPow.hPow (α := ℝ) 2⁻¹ n), dist (op s) (op t) ≤ dist s t
Tactic: obtain ⟨n, hst⟩ := dist_eq_two_inv_pow hst
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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) ↦
        match (motive :=
          ℝ × MultiseriesExpansion basis_tl × Multiseries basis_hd basis_tl → Seq1 (ℝ × MultiseriesExpansion basis_tl))
          x with
        | (exp, coef, tl) => ((exp, coef), tl))
      (destruct s)
have simp : 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: simp only [destruct, Option.map_map]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
exp1 exp2 : ℝ
coef1 coef2 : MultiseriesExpansion basis_tl
tl1 tl2 : Multiseries basis_hd basis_tl
⊢ cons exp1 coef1 tl1 = cons exp2 coef2 tl2 ↔ exp1 = exp2 ∧ coef1 = coef2 ∧ tl1 = tl2
have rw : (exp1, coef1) = (exp2, coef2) ∧ tl1 = tl2 ↔ exp1 = exp2 ∧ coef1 = coef2 ∧ tl1 = tl2
Tactic: rw [cons, cons, Seq.cons_eq_cons]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
β : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
f : β → Option (ℝ × MultiseriesExpansion basis_tl × β)
b : β
h : 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
have h₁ : Eq (α := Option ((ℝ × MultiseriesExpansion basis_tl) × β))
  (Option.map (fun (x : ℝ × MultiseriesExpansion basis_tl × β) ↦ ((x.1, x.2.1), x.2.2)) (f b)) none
Tactic: rw [Seq.corec_nil]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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)
⊢ 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)
have rw : Option.map (fun (x : ℝ × MultiseriesExpansion basis_tl × β) ↦ ((x.1, x.2.1), x.2.2)) (f b) = some ((exp, coef), next)
Tactic: rw [Seq.corec_cons]
-- 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.destruct = none
⊢ ms = nil
have a : Seq.destruct ms = none
Tactic: apply Stream'.Seq.destruct_eq_none
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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)
⊢ ms = cons exp coef tl
have a : Seq.destruct ms = some ((exp, coef), tl)
Tactic: apply Stream'.Seq.destruct_eq_cons
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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)
⊢ Seq.destruct ms = some ((exp, coef), tl)
have 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)
Tactic: rw [destruct_eq_destruct_map, h]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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₃) (map (f₂ ∘ f₁) (g₂ ∘ g₁) ms) (map (basis_hd := b₂) f₂ g₂ (map f₁ g₁ ms))
have 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)
Tactic: simp [map, ← Stream'.Seq.map_comp]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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)
⊢ motive ms
have let : (s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)) → (f : ℝ → ℝ) → motive (s, f)
Tactic: let ⟨s, f⟩ := ms
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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 : ℝ → ℝ
⊢ motive (s, f)
have nil₁ : motive (Seq.nil, f)
Tactic: cases s with
  | nil => apply nil
  | cons hd tl => apply cons
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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)
⊢ motive (s, f)
have cons₁ : (hd : ℝ × MultiseriesExpansion basis_tl) →
  (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)) → motive (Seq.cons hd tl, f)
Tactic: cases s with
  | nil => apply nil
  | cons hd tl => apply cons
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s t : Multiseries basis_hd basis_tl
f g : ℝ → ℝ
h : mk s f = mk t g
⊢ s = t ∧ f = g
have rwa : ∀ (h : (s, f) = mk t g), s = t ∧ f = g
Tactic: rwa [mk, mk, Prod.mk_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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
⊢ s = t ∧ f = g
have rwa₁ : ∀ (h : (s, f) = (t, g)), s = t ∧ f = g
Tactic: rwa [mk, mk, Prod.mk_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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
⊢ s = t ∧ f = g
have rwa₂ : ∀ (h : s = t ∧ f = g), s = t ∧ f = g
Tactic: rwa [mk, mk, Prod.mk_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
| ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f
have lhs : ms = mk s f
Tactic: lhs
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
| ms = mk s f
have lhs : ms
Tactic: lhs
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
| ms
have rw : mk ms.seq ms.toFun
Tactic: rw [eq_mk ms]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
| ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f
have rw : mk ms.seq ms.toFun
Tactic: lhs; lhs; rw [eq_mk ms]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
⊢ ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f
have conv : mk ms.seq ms.toFun = mk s f ↔ ms.seq = s ∧ ms.toFun = f
Tactic: conv => lhs; lhs; rw [eq_mk ms]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
⊢ mk ms.seq ms.toFun = mk s f ↔ ms.seq = s ∧ ms.toFun = f
have rw : ms.seq = s ∧ ms.toFun = f ↔ ms.seq = s ∧ ms.toFun = f
Tactic: rw [mk_eq_mk_iff]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
⊢ mk s f = ms ↔ ms.seq = s ∧ ms.toFun = f
have rw : ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f
Tactic: rw [@Eq.comm _ (mk s f) ms, ms_eq_mk_iff]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
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
⊢ mk s f = ms ↔ ms.seq = s ∧ ms.toFun = f
have rw₁ : ms.seq = s ∧ ms.toFun = f ↔ ms.seq = s ∧ ms.toFun = f
Tactic: rw [@Eq.comm _ (mk s f) ms, ms_eq_mk_iff]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms₁ ms₂ : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms₁.seq = ms₂.seq ∧ ms₁.toFun = ms₂.toFun
⊢ ms₁ = ms₂
have rw : mk ms₁.seq ms₁.toFun = mk ms₂.seq ms₂.toFun
Tactic: rw [eq_mk ms₁, eq_mk ms₂]