-- Mathlib/Data/Seq/Seq.lean
theorem cons_append (a : α) (s t) : append (cons a s) t = cons a (append s t) :=
  destruct_eq_cons <| by
    dsimp [append]; rw [corec_eq]
    dsimp [append]; rw [destruct_cons]

Proof state:
α : Type u
a : α
s t : Seq α
⊢ omap
      (corec fun x =>
        match x.fst.destruct with
        | none =>
          match x.snd.destruct with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.snd))
      (match (cons a s, t).fst.destruct with
      | none =>
        match (cons a s, t).snd.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a_1, s₁') => some (a_1, s₁', (cons a s, t).snd)) =
    some
      (a,
        corec
          (fun x =>
            match x.fst.destruct with
            | none =>
              match x.snd.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.snd))
          (s, t))

Tactic:
dsimp [append]

Result:
α : Type u
a : α
s t : Seq α
⊢ (match
      match (cons a s).destruct with
      | none =>
        match t.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', t) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match x.fst.destruct with
              | none =>
                match x.snd.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b)) =
    some
      (a,
        corec
          (fun x =>
            match x.fst.destruct with
            | none =>
              match x.snd.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.snd))
          (s, t))

Proof state:
α : Type u
a : α
s t : Seq α
⊢ (match
      match (cons a s).destruct with
      | none =>
        match t.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', t) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x =>
              match x.fst.destruct with
              | none =>
                match x.snd.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.snd))
            b)) =
    some
      (a,
        corec
          (fun x =>
            match x.fst.destruct with
            | none =>
              match x.snd.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.snd))
          (s, t))

Tactic:
rw [destruct_cons]

Result:
no goals

Proof state:
α : Type u
a : α
s t : Seq α
⊢ (corec
        (fun x =>
          match x.fst.destruct with
          | none =>
            match x.snd.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.snd))
        (cons a s, t)).destruct =
    some
      (a,
        corec
          (fun x =>
            match x.fst.destruct with
            | none =>
              match x.snd.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.snd))
          (s, t))

Tactic:
rw [corec_eq]

Result:
α : Type u
a : α
s t : Seq α
⊢ omap
      (corec fun x =>
        match x.fst.destruct with
        | none =>
          match x.snd.destruct with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.snd))
      (match (cons a s, t).fst.destruct with
      | none =>
        match (cons a s, t).snd.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a_1, s₁') => some (a_1, s₁', (cons a s, t).snd)) =
    some
      (a,
        corec
          (fun x =>
            match x.fst.destruct with
            | none =>
              match x.snd.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.snd))
          (s, t))

Proof state:
α : Type u
a : α
s t : Seq α
⊢ ((cons a s).append t).destruct = some (a, s.append t)

Tactic:
dsimp [append]

Result:
α : Type u
a : α
s t : Seq α
⊢ (corec
        (fun x =>
          match x.fst.destruct with
          | none =>
            match x.snd.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.snd))
        (cons a s, t)).destruct =
    some
      (a,
        corec
          (fun x =>
            match x.fst.destruct with
            | none =>
              match x.snd.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.snd))
          (s, t))