awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
x : α
s : Stream'.Seq α
⊢ (Seq.cons x 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 α) (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))
          (Seq.cons x s).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) ⋯))

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
cons :
  (op (Seq.cons s_hd s_tl)).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))
        (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) ⋯))
⊢ (op (Seq.cons s_hd s_tl)).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.cons s_hd s_tl).tail))
      (match (motive := Option α → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        (Seq.cons s_hd s_tl).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) ⋯))

Tactic:
simp only [Seq.tail_cons, Seq.head_cons]

Premises used: Stream'.Seq.tail_cons, Stream'.Seq.head_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
cons :
  ∀ (t0 : Stream'.Seq α) (ht0 : op (Seq.cons s_hd nil) = t0),
    (op (Seq.cons s_hd s_tl)).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) ⋯))
⊢ (op (Seq.cons s_hd s_tl)).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))
        (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) ⋯))

Tactic:
generalize ht0 : op (.cons s_hd nil) = t0 at *

Premises used: Stream'.Seq.nil, Stream'.Seq.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
cons :
  ∀ (t : Stream'.Seq α) (ht : op (Seq.cons s_hd s_tl) = t),
    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) ⋯))
⊢ (op (Seq.cons s_hd s_tl)).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) ⋯))

Tactic:
generalize ht : op (.cons s_hd s_tl) = t at *

Premises used: Stream'.Seq.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
rw : (op (Seq.cons s_hd nil)).head = t.head
rw₁ : (op (Seq.cons s_hd nil)).head = (op (Seq.cons s_hd s_tl)).head
rw₂ : (op (Seq.cons s_hd s_tl)).head = (op (Seq.cons s_hd s_tl)).head
rw₃ : Stream'.Seq α
rw₄ : (op (Seq.cons s_hd s_tl)).head = (op (Seq.cons s_hd s_tl)).head
rw₅ : Stream'.Seq α
⊢ t0.head = t.head

Tactic:
rw [← ht0, ← ht, FriendlyOperation.op_cons_head_eq h]

Premises used: Tactic.ComputeAsymptotics.Seq.FriendlyOperation.op_cons_head_eq
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
⊢ t0.head = t.head

Tactic:
have : t0.head = t.head := by
      rw [← ht0, ← ht, FriendlyOperation.op_cons_head_eq h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = nil
ht : op (Seq.cons s_hd s_tl) = nil
this : Eq.{u_1 + 1} (α := Option α) (Seq.head nil) (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))
        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) ⋯)))

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = nil
x : α
s : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = Seq.cons x s
this : Seq.head nil = (Seq.cons x s).head
⊢ (Seq.cons x s).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) ⋯))

Tactic:
simp at this
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
ht0 : op (Seq.cons s_hd nil) = nil
this : Seq.head nil = t.head
cons :
  ∀ (ht : op (Seq.cons s_hd s_tl) = nil) (this : Eq.{u_1 + 1} (α := Option α) (Seq.head nil) (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))
          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) ⋯)))
cons₁ :
  ∀ (x : α) (s : Stream'.Seq α) (ht : op (Seq.cons s_hd s_tl) = Seq.cons x s)
    (this : Seq.head nil = (Seq.cons x s).head),
    (Seq.cons x s).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))
        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) ⋯))

Tactic:
cases t with
      | nil => simp
      | cons => simp at this

Premises used: Stream'.Seq.nil, Tactic.ComputeAsymptotics.Seq.FriendlyOperation.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
x : α
s : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = Seq.cons x s
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) ⋯)))

Tactic:
simp at this
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
x : α
s : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = Seq.cons x s
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) ⋯))

Tactic:
simp_all
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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) ⋯)))
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) ⋯))
⊢ 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) ⋯))

Tactic:
cases t with
      | nil => simp at this
      | cons => simp_all

Premises used: Stream'.Seq.nil, Tactic.ComputeAsymptotics.Seq.FriendlyOperation.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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) ⋯))
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) ⋯))
⊢ 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) ⋯))

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

Premises used: Stream'.Seq.nil, Tactic.ComputeAsymptotics.Seq.FriendlyOperation.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s t : Stream'.Seq α
h_head : s.head = t.head
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)))
⊢ (op s).head = (op t).head

Tactic:
simp only [head_eq_destruct, Option.map_eq_map, h.destruct_apply_eq_unfold, Option.map_map]
    at h_head ⊢

Premises used: Tactic.ComputeAsymptotics.Seq.FriendlyOperation.destruct_apply_eq_unfold, Option.map_map, Stream'.Seq.head_eq_destruct, Option.map_eq_map
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
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)))
⊢ 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 [h_head]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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 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:
rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
rw : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
⊢ FriendlyOperation op

Tactic:
rw [friendlyOperation_iff_dist_le_dist]

Premises used: Tactic.ComputeAsymptotics.Seq.friendlyOperation_iff_dist_le_dist
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
neg : ∀ (hst : ¬s = t), dist (op s) (op t) ≤ dist s t
⊢ dist (op s) (op t) ≤ dist s t

Tactic:
by_cases hst : s = t
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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

Tactic:
simp [hst]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
neg : ∀ (n : ℕ) (hst : dist s t = HPow.hPow (α := ℝ) 2⁻¹ n), dist (op s) (op t) ≤ dist s t
⊢ dist (op s) (op t) ≤ dist s t

Tactic:
obtain ⟨n, hst⟩ := dist_eq_two_inv_pow hst

Premises used: Tactic.ComputeAsymptotics.Seq.dist_eq_two_inv_pow
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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_1 : ¬s = t
n : ℕ
hst : dist s t = HPow.hPow (α := ℝ) 2⁻¹ n
⊢ dist (op s) (op t) ≤ dist s t

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
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
⊢ 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)

Tactic:
simp only [destruct, Option.map_map]

Premises used: Option.map_map, ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct