-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
l : List α
s_1 : WSeq α
s1 s2 : Computation (List α)
l' : List α
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) 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, cons a s) ∧
    s2 =
      Computation.map (fun (x : List α) ↦ l.reverse ++ x)
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) 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', cons a s))
refine_1 :
  Eq (α := Computation (List α))
    (Computation.tail
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) 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, cons a s)))
    (Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
        | (l, s) =>
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) 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'))
      (a :: l' ++ l, s))
⊢ BisimO (α := List α)
    (fun (c1 c2 : Computation (List α)) ↦
      ∃ (l' : List α) (s : WSeq α),
        c1 =
            Computation.corec
              (fun (x : List α × WSeq α) ↦
                match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                | (l, s) =>
                  match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) 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 : List α) ↦ l.reverse ++ x)
              (Computation.corec
                (fun (x : List α × WSeq α) ↦
                  match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                  | (l, s) =>
                    match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) 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.destruct
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) 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, cons a s)))
    (Computation.destruct
      (Computation.map (fun (x : List α) ↦ l.reverse ++ x)
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) 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', cons a s))))
have refine_2 : Eq (α := Computation (List α))
  (Computation.tail
    (Computation.map (fun (x : List α) ↦ l.reverse ++ x)
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) 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', cons a s))))
  (Computation.map (fun (x : List α) ↦ l.reverse ++ x)
    (Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
        | (l, s) =>
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) 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'))
      (a :: l', s)))
Tactic: refine ⟨a :: l', s, ?_, ?_⟩