Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
l : List α
s : WSeq α
s1 : Computation (List α)
⊢ ∀ ⦃s₂ : Computation (List α)⦄,
    (fun c1 c2 ↦
          ∃ l' s,
            c1 =
                Computation.corec
                  (fun x ↦
                    match x with
                    | (l, s) =>
                      match Seq.destruct s with
                      | none => Sum.inl l.reverse
                      | some (none, s') => Sum.inr (l, s')
                      | some (some a, s') => Sum.inr (a :: l, s'))
                  (l' ++ l, s) ∧
              c2 =
                Computation.map (fun x ↦ l.reverse ++ x)
                  (Computation.corec
                    (fun x ↦
                      match x with
                      | (l, s) =>
                        match Seq.destruct s with
                        | none => Sum.inl l.reverse
                        | some (none, s') => Sum.inr (l, s')
                        | some (some a, s') => Sum.inr (a :: l, s'))
                    (l', s)))
        s1 s₂ →
      BisimO
        (fun c1 c2 ↦
          ∃ l' s,
            c1 =
                Computation.corec
                  (fun x ↦
                    match x with
                    | (l, s) =>
                      match Seq.destruct s with
                      | none => Sum.inl l.reverse
                      | some (none, s') => Sum.inr (l, s')
                      | some (some a, s') => Sum.inr (a :: l, s'))
                  (l' ++ l, s) ∧
              c2 =
                Computation.map (fun x ↦ l.reverse ++ x)
                  (Computation.corec
                    (fun x ↦
                      match x with
                      | (l, s) =>
                        match Seq.destruct s with
                        | none => Sum.inl l.reverse
                        | some (none, s') => Sum.inr (l, s')
                        | some (some a, s') => Sum.inr (a :: l, s'))
                    (l', s)))
        s1.destruct s₂.destruct

Tactic:
s2

Goal state after:
α : Type u
l : List α
s : WSeq α
s1 s2 : Computation (List α)
⊢ (fun c1 c2 ↦
        ∃ l' s,
          c1 =
              Computation.corec
                (fun x ↦
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl l.reverse
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l' ++ l, s) ∧
            c2 =
              Computation.map (fun x ↦ l.reverse ++ x)
                (Computation.corec
                  (fun x ↦
                    match x with
                    | (l, s) =>
                      match Seq.destruct s with
                      | none => Sum.inl l.reverse
                      | some (none, s') => Sum.inr (l, s')
                      | some (some a, s') => Sum.inr (a :: l, s'))
                  (l', s)))
      s1 s2 →
    BisimO
      (fun c1 c2 ↦
        ∃ l' s,
          c1 =
              Computation.corec
                (fun x ↦
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl l.reverse
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l' ++ l, s) ∧
            c2 =
              Computation.map (fun x ↦ l.reverse ++ x)
                (Computation.corec
                  (fun x ↦
                    match x with
                    | (l, s) =>
                      match Seq.destruct s with
                      | none => Sum.inl l.reverse
                      | some (none, s') => Sum.inr (l, s')
                      | some (some a, s') => Sum.inr (a :: l, s'))
                  (l', s)))
      s1.destruct s2.destruct