-- 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 α
nil :
  (op Seq.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 Seq.nil)))
      (match (motive := Option α → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        Seq.head Seq.nil with
      | none =>
        match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          (op Seq.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 Seq.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 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 Seq.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 Seq.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 : ∀ (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 Seq.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 Seq.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