-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
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
⊢ 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

Tactic:
cases Seq.destruct s with
  | none => simp
  | some val =>
    obtain ⟨o, s'⟩ := val
    simp

Premises used: Option.some, Option.none, Stream'.Seq.destruct