-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
val : Seq1 (Option α)
some :
  ∀ (o : Option α) (s' : Seq (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 α))) Option.some (o, s') with
        | none => none
        | Option.some (a, b) => Option.some (a, Computation.pure b) with
      | none => none
      | Option.some (a, b) =>
        Option.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
                  | Option.some (a, b) => Option.some (a, Computation.pure b)
                | Sum.inr c' => Option.some (none, c'))
              b),
      Option.some (o, s') with
    | none, none => True
    | Option.some (a, s), Option.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
                | Option.some (a, b) => Option.some (a, Computation.pure b)
              | Sum.inr c' => Option.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 α))) Option.some val with
      | none => none
      | Option.some (a, b) => Option.some (a, Computation.pure b) with
    | none => none
    | Option.some (a, b) =>
      Option.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
                | Option.some (a, b) => Option.some (a, Computation.pure b)
              | Sum.inr c' => Option.some (none, c'))
            b),
    Option.some val with
  | none, none => True
  | Option.some (a, s), Option.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
              | Option.some (a, b) => Option.some (a, Computation.pure b)
            | Sum.inr c' => Option.some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
obtain ⟨o, s'⟩ := val