-- Mathlib/Data/Seq/WSeq.lean
theorem destruct_ofSeq (s : Seq α) :
    destruct (ofSeq s) = Computation.pure (s.head.map fun a => (a, ofSeq s.tail)) :=
  destruct_eq_pure <| by
    simp only [destruct, Seq.destruct, Option.map_eq_map, ofSeq, Computation.corec_eq, rmap,
      Seq.head]
    rw [show Seq.get? (some <$> s) 0 = some <$> Seq.get? s 0 by apply Seq.map_get?]
    rcases Seq.get? s 0 with - | a
    · rfl
    dsimp only [(· <$> ·)]
    simp [destruct]

Proof state:
α : Type u
s : Seq α
⊢ (some <$> s).get? 0 = some <$> s.get? 0

Tactic:
apply Seq.map_get?

Result:
no goals

Proof state:
case some
α : Type u
s : Seq α
a : α
⊢ (match
      match Option.map (fun a' => (a', (Seq.map some s).tail)) (Option.map some (some a)) with
      | none => Sum.inl none
      | some (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 =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, Seq.map some s.tail)) (some a))

Tactic:
simp [destruct]

Result:
no goals

Proof state:
α : Type u
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', (some <$> s).tail)) ((some <$> s).get? 0) with
      | none => Sum.inl none
      | some (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 =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> s.tail)) (s.get? 0))

Tactic:
rw [show Seq.get? (some <$> s) 0 = some <$> Seq.get? s 0 by apply Seq.map_get?]

Result:
α : Type u
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', (some <$> s).tail)) (some <$> s.get? 0) with
      | none => Sum.inl none
      | some (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 =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> s.tail)) (s.get? 0))

Proof state:
case none
α : Type u
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', (some <$> s).tail)) (some <$> none) with
      | none => Sum.inl none
      | some (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 =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> s.tail)) none)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', (some <$> s).tail)) (some <$> s.get? 0) with
      | none => Sum.inl none
      | some (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 =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> s.tail)) (s.get? 0))

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

Result:
case none
α : Type u
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', (some <$> s).tail)) (some <$> none) with
      | none => Sum.inl none
      | some (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 =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> s.tail)) none)

case some
α : Type u
s : Seq α
a : α
⊢ (match
      match Option.map (fun a' => (a', (some <$> s).tail)) (some <$> some a) with
      | none => Sum.inl none
      | some (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 =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> s.tail)) (some a))

Proof state:
α : Type u
s : Seq α
⊢ (↑s).destruct.destruct = Sum.inl (Option.map (fun a => (a, ↑s.tail)) s.head)

Tactic:
simp only [destruct, Seq.destruct, Option.map_eq_map, ofSeq, Computation.corec_eq, rmap,
  Seq.head]

Result:
α : Type u
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', (some <$> s).tail)) ((some <$> s).get? 0) with
      | none => Sum.inl none
      | some (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 =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> s.tail)) (s.get? 0))