-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
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', (some <$> s).tail)) (some <$> Option.none) with
        | Option.none => Sum.inl Option.none
        | some (Option.none, s') => Sum.inr s'
        | some (some a, s') => Sum.inl (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
              | some (Option.none, s') => Sum.inr s'
              | some (some a, s') => Sum.inl (some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) Option.none) :
      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', (some <$> s).tail)) (some <$> s.get? 0) with
        | Option.none => Sum.inl Option.none
        | some (Option.none, s') => Sum.inr s'
        | some (some a, s') => Sum.inl (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
              | some (Option.none, s') => Sum.inr s'
              | some (some a, s') => Sum.inl (some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) (s.get? 0)) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
have 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', (some <$> s).tail)) (some <$> some a) with
        | Option.none => Sum.inl Option.none
        | some (Option.none, s') => Sum.inr s'
        | some (some a, s') => Sum.inl (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
              | some (Option.none, s') => Sum.inr s'
              | some (some a, s') => Sum.inl (some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) (some a)) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
Tactic: rcases Seq.get? s 0 with - | a