-- Mathlib/Data/Seq/WSeq.lean
theorem toList_cons (a : α) (s) : toList (cons a s) = (List.cons a <$> toList s).think :=
  destruct_eq_think <| by
    unfold toList
    simp only [toList'_cons, Computation.destruct_think, Sum.inr.injEq]
    rw [toList'_map]
    simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append]
    rfl

Proof state:
α : Type u
a : α
s : WSeq α
⊢ (fun x => [a].reverse ++ x) <$> s.toList =
    List.cons a <$>
      Computation.corec
        (fun x =>
          match Seq.destruct x.snd with
          | none => Sum.inl x.fst.reverse
          | some (none, s') => Sum.inr (x.fst, s')
          | some (some a, s') => Sum.inr (a :: x.fst, s'))
        ([], s)

Tactic:
simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append]

Result:
α : Type u
a : α
s : WSeq α
⊢ (fun x => a :: x) <$> s.toList =
    List.cons a <$>
      Computation.corec
        (fun x =>
          match Seq.destruct x.snd with
          | none => Sum.inl x.fst.reverse
          | some (none, s') => Sum.inr (x.fst, s')
          | some (some a, s') => Sum.inr (a :: x.fst, s'))
        ([], s)

Proof state:
α : Type u
a : α
s : WSeq α
⊢ (cons a s).toList.destruct = Sum.inr (List.cons a <$> s.toList)

Tactic:
unfold toList

Result:
α : Type u
a : α
s : WSeq α
⊢ (Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        ([], cons a s)).destruct =
    Sum.inr
      (List.cons a <$>
        Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          ([], s))

Proof state:
α : Type u
a : α
s : WSeq α
⊢ (fun x => a :: x) <$> s.toList =
    List.cons a <$>
      Computation.corec
        (fun x =>
          match Seq.destruct x.snd with
          | none => Sum.inl x.fst.reverse
          | some (none, s') => Sum.inr (x.fst, s')
          | some (some a, s') => Sum.inr (a :: x.fst, s'))
        ([], s)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
a : α
s : WSeq α
⊢ Computation.corec
      (fun x =>
        match Seq.destruct x.snd with
        | none => Sum.inl x.fst.reverse
        | some (none, s') => Sum.inr (x.fst, s')
        | some (some a, s') => Sum.inr (a :: x.fst, s'))
      ([a], s) =
    List.cons a <$>
      Computation.corec
        (fun x =>
          match Seq.destruct x.snd with
          | none => Sum.inl x.fst.reverse
          | some (none, s') => Sum.inr (x.fst, s')
          | some (some a, s') => Sum.inr (a :: x.fst, s'))
        ([], s)

Tactic:
rw [toList'_map]

Result:
α : Type u
a : α
s : WSeq α
⊢ (fun x => [a].reverse ++ x) <$> s.toList =
    List.cons a <$>
      Computation.corec
        (fun x =>
          match Seq.destruct x.snd with
          | none => Sum.inl x.fst.reverse
          | some (none, s') => Sum.inr (x.fst, s')
          | some (some a, s') => Sum.inr (a :: x.fst, s'))
        ([], s)

Proof state:
α : Type u
a : α
s : WSeq α
⊢ (Computation.corec
        (fun x =>
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        ([], cons a s)).destruct =
    Sum.inr
      (List.cons a <$>
        Computation.corec
          (fun x =>
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          ([], s))

Tactic:
simp only [toList'_cons, Computation.destruct_think, Sum.inr.injEq]

Result:
α : Type u
a : α
s : WSeq α
⊢ Computation.corec
      (fun x =>
        match Seq.destruct x.snd with
        | none => Sum.inl x.fst.reverse
        | some (none, s') => Sum.inr (x.fst, s')
        | some (some a, s') => Sum.inr (a :: x.fst, s'))
      ([a], s) =
    List.cons a <$>
      Computation.corec
        (fun x =>
          match Seq.destruct x.snd with
          | none => Sum.inl x.fst.reverse
          | some (none, s') => Sum.inr (x.fst, s')
          | some (some a, s') => Sum.inr (a :: x.fst, s'))
        ([], s)