-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
t : Stream'.Seq α
nil :
  Eq.{u_1 + 1} (α := Option (Seq1 α)) (destruct Seq.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 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))
          destruct Seq.nil 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) ⋯)))
nil₁ :
  ∀ (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 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))
            (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 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) ⋯))
⊢ 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 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))
          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 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) ⋯))

Tactic:
cases t