awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ dist (Seq.cons a s) (Seq.cons a t)
⊢ (op (Seq.cons a s)).head = (op (Seq.cons a t)).head
have h₁ : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹ * dist s t
Tactic: simp only [dist_cons_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹ * dist s t
⊢ dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹
have apply : 2⁻¹ * dist s t ≤ 2⁻¹
Tactic: apply h.trans
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹ * dist s t
⊢ (op (Seq.cons a s)).head = (op (Seq.cons a t)).head
have h₁ : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹
Tactic: replace h : dist (op (.cons a s)) (op (.cons a t)) ≤ 2⁻¹ := by
    apply h.trans
    simp
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹
⊢ (op (Seq.cons a s)).head = (op (Seq.cons a t)).head
have h₁ : op (Seq.cons a s) = nil ∧ op (Seq.cons a t) = nil ∨
  ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α),
    op (Seq.cons a s) = Seq.cons hd s' ∧ op (Seq.cons a t) = Seq.cons hd t'
Tactic: rw [dist_le_half_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h :
  op (Seq.cons a s) = nil ∧ op (Seq.cons a t) = nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α),
      op (Seq.cons a s) = Seq.cons hd s' ∧ op (Seq.cons a t) = Seq.cons hd t'
⊢ (op (Seq.cons a s)).head = (op (Seq.cons a t)).head
have generalize : ∀ (s' : Stream'.Seq α)
  (h :
    s' = nil ∧ op (Seq.cons a t) = nil ∨
      ∃ (hd : α) (s'_1 : Stream'.Seq α) (t' : Stream'.Seq α),
        s' = Seq.cons hd s'_1 ∧ op (Seq.cons a t) = Seq.cons hd t'),
  s'.head = (op (Seq.cons a t)).head
Tactic: generalize op (Seq.cons a s) = s' at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t s' : Stream'.Seq α
h :
  s' = nil ∧ op (Seq.cons a t) = nil ∨
    ∃ (hd : α) (s'_1 : Stream'.Seq α) (t' : Stream'.Seq α), s' = Seq.cons hd s'_1 ∧ op (Seq.cons a t) = Seq.cons hd t'
⊢ s'.head = (op (Seq.cons a t)).head
have generalize : ∀ (t' : Stream'.Seq α)
  (h :
    s' = nil ∧ t' = nil ∨
      ∃ (hd : α) (s'_1 : Stream'.Seq α) (t'_1 : Stream'.Seq α), s' = Seq.cons hd s'_1 ∧ t' = Seq.cons hd t'_1),
  s'.head = t'.head
Tactic: generalize op (Seq.cons a t) = t' at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t s' t' : Stream'.Seq α
h :
  s' = nil ∧ t' = nil ∨
    ∃ (hd : α) (s'_1 : Stream'.Seq α) (t'_1 : Stream'.Seq α), s' = Seq.cons hd s'_1 ∧ t' = Seq.cons hd t'_1
⊢ s'.head = t'.head
have inl : Eq.{u_1 + 1} (α := Option α) (Seq.head nil) (Seq.head nil)
Tactic: obtain ⟨rfl, rfl⟩ | ⟨hd, s_tl, t_tl, rfl, rfl⟩ := h
Cleared hypotheses: s', t', h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t s' t' : Stream'.Seq α
h :
  s' = nil ∧ t' = nil ∨
    ∃ (hd : α) (s'_1 : Stream'.Seq α) (t'_1 : Stream'.Seq α), s' = Seq.cons hd s'_1 ∧ t' = Seq.cons hd t'_1
inl : Eq.{u_1 + 1} (α := Option α) (Seq.head nil) (Seq.head nil)
⊢ s'.head = t'.head
have inr : ∀ (hd : α) (s_tl t_tl : Stream'.Seq α), (Seq.cons hd s_tl).head = (Seq.cons hd t_tl).head
Tactic: obtain ⟨rfl, rfl⟩ | ⟨hd, s_tl, t_tl, rfl, rfl⟩ := h
Cleared hypotheses: s', t', h
-- 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))
      (h.unfold s.head)
have unfold : (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) 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: unfold unfold
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
⊢ (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) ⋯)
      | 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 : ∀ (t : Stream'.Seq α),
  t.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))
          t.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: generalize op nil = t
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
t : Stream'.Seq α
⊢ t.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))
          t.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 : Eq.{u_1 + 1} (α := Option (Seq1 α)) (destruct nil)
  (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))
        destruct nil 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 t
Cleared hypotheses: t
-- 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 : Stream'.Seq α
⊢ (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) ⋯))
have 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) sorry))
Tactic: simp only [Seq.tail_cons, Seq.head_cons]
-- 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 : Stream'.Seq α
⊢ (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) ⋯))
have 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) sorry))
Tactic: generalize ht0 : op (.cons s_hd nil) = t0 at *
-- 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
⊢ (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) ⋯))
have 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) sorry))
Tactic: generalize ht : op (.cons s_hd s_tl) = t at *
-- 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
⊢ t0.head = t.head
have rw : (op (Seq.cons s_hd nil)).head = t.head
Tactic: rw [← ht0, ← ht, FriendlyOperation.op_cons_head_eq h]
-- 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
rw : (op (Seq.cons s_hd nil)).head = t.head
⊢ t0.head = t.head
have rw₁ : (op (Seq.cons s_hd nil)).head = (op (Seq.cons s_hd s_tl)).head
Tactic: rw [← ht0, ← ht, FriendlyOperation.op_cons_head_eq h]
-- 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
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
⊢ t0.head = t.head
have rw₂ : (op (Seq.cons s_hd s_tl)).head = (op (Seq.cons s_hd s_tl)).head
Tactic: rw [← ht0, ← ht, FriendlyOperation.op_cons_head_eq h]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
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
⊢ 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 this : t0.head = t.head
Tactic: have : t0.head = t.head := by
      rw [← ht0, ← ht, FriendlyOperation.op_cons_head_eq h]
-- 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
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) ⋯))
have 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) sorry)))
Tactic: cases t with
      | nil => simp
      | cons => simp at this
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 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) ⋯)))
⊢ 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) ⋯))
have 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) sorry))
Tactic: cases t with
      | nil => simp
      | cons => simp at this
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 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
⊢ 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 : ∀ (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) sorry)))
Tactic: cases t with
      | nil => simp at this
      | cons => simp_all
Cleared hypotheses: t, ht, this