Module: Mathlib.Data.WSeq.Defs

Goal state before:
pp: α : Type u
s : WSeq α
s1 s2 : Computation ℕ
⊢ (fun c1 c2 ↦
        ∃ l s,
          c1 =
              Computation.corec
                (fun x ↦
                  match x with
                  | (n, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl n
                    | some (none, s') => Sum.inr (n, s')
                    | some (some val, s') => Sum.inr (n + 1, s'))
                (l.length, s) ∧
            c2 =
              Computation.map List.length
                (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 →
    Computation.BisimO
      (fun c1 c2 ↦
        ∃ l s,
          c1 =
              Computation.corec
                (fun x ↦
                  match x with
                  | (n, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl n
                    | some (none, s') => Sum.inr (n, s')
                    | some (some val, s') => Sum.inr (n + 1, s'))
                (l.length, s) ∧
            c2 =
              Computation.map List.length
                (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

Tactic:
h

Goal state after:
α : Type u
s : WSeq α
s1 s2 : Computation ℕ
h :
  ∃ l s,
    s1 =
        Computation.corec
          (fun x ↦
            match x with
            | (n, s) =>
              match Seq.destruct s with
              | none => Sum.inl n
              | some (none, s') => Sum.inr (n, s')
              | some (some val, s') => Sum.inr (n + 1, s'))
          (l.length, s) ∧
      s2 =
        Computation.map List.length
          (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))
⊢ Computation.BisimO
    (fun c1 c2 ↦
      ∃ l s,
        c1 =
            Computation.corec
              (fun x ↦
                match x with
                | (n, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl n
                  | some (none, s') => Sum.inr (n, s')
                  | some (some val, s') => Sum.inr (n + 1, s'))
              (l.length, s) ∧
          c2 =
            Computation.map List.length
              (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