-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : Seq α
none :
  Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
        match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
          Option.map (fun (a' : Option α) ↦ (a', (Option.some <$> s).tail)) (Option.some <$> Option.none) with
        | Option.none => Sum.inl Option.none
        | Option.some (Option.none, s') => Sum.inr s'
        | Option.some (Option.some a, s') => Sum.inl (Option.some (a, s')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Computation.corec
            (fun (s : WSeq α) ↦
              match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
                Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
              | Option.none => Sum.inl Option.none
              | Option.some (Option.none, s') => Sum.inr s'
              | Option.some (Option.some a, s') => Sum.inl (Option.some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, Option.some <$> s.tail)) Option.none) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
some :
  ∀ (a : α),
    Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
      (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
          match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
            Option.map (fun (a' : Option α) ↦ (a', (Option.some <$> s).tail)) (Option.some <$> Option.some a) with
          | Option.none => Sum.inl Option.none
          | Option.some (Option.none, s') => Sum.inr s'
          | Option.some (Option.some a, s') => Sum.inl (Option.some (a, s')) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b =>
          Sum.inr
            (Computation.corec
              (fun (s : WSeq α) ↦
                match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
                  Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
                | Option.none => Sum.inl Option.none
                | Option.some (Option.none, s') => Sum.inr s'
                | Option.some (Option.some a, s') => Sum.inl (Option.some (a, s')))
              b) :
        Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
      (Sum.inl (Option.map (fun (a : α) ↦ (a, Option.some <$> s.tail)) (Option.some a)) :
        Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
⊢ Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
        match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
          Option.map (fun (a' : Option α) ↦ (a', (Option.some <$> s).tail)) (Option.some <$> s.get? 0) with
        | Option.none => Sum.inl Option.none
        | Option.some (Option.none, s') => Sum.inr s'
        | Option.some (Option.some a, s') => Sum.inl (Option.some (a, s')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Computation.corec
            (fun (s : WSeq α) ↦
              match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
                Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
              | Option.none => Sum.inl Option.none
              | Option.some (Option.none, s') => Sum.inr s'
              | Option.some (Option.some a, s') => Sum.inl (Option.some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, Option.some <$> s.tail)) (s.get? 0)) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))

Tactic:
rcases Seq.get? s 0 with - | a

Premises used: OfNat.ofNat, Stream'.Seq.get?