-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s_1 : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ match (motive := Option (Seq1 (Option α)) → Option (Seq1 (Option α)) → Prop)
    match (motive := Option (Option α × Computation (WSeq α)) → Option (Option α × Seq (Option α)))
      match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α))) s.destruct with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun (c : Computation (WSeq α)) ↦
              match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
              | Sum.inl s =>
                match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α)))
                  Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun (c : Computation (WSeq α)) ↦
            match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
            | Sum.inl s =>
              match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α)))
                Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False
have cases : ∀ (x : Option (Seq1 (Option α))),
  match (motive := Option (Seq1 (Option α)) → Option (Seq1 (Option α)) → Prop)
    match (motive := Option (Option α × Computation (WSeq α)) → Option (Option α × Seq (Option α)))
      match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α))) x with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun (c : Computation (WSeq α)) ↦
              match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
              | Sum.inl s =>
                match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α)))
                  Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    x with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun (c : Computation (WSeq α)) ↦
            match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
            | Sum.inl s =>
              match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α)))
                Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False
Tactic: cases Seq.destruct s with
  | none => simp
  | some val =>
    obtain ⟨o, s'⟩ := val
    simp