Theorem: List.reverse_eq_reverseSpec (Table/BuiltinExtensions.lean)

State before:
case nil
α : Type u_1
⊢ reverse [] = reverseSpec []
Tactic:
simp [reverse, reverseAux, reverseSpec]
State after:
no goals

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : reverse xs = reverseSpec xs
⊢ reverse (x :: xs) = reverseSpec (x :: xs)
Tactic:
simp only [reverse, reverseSpec, reverseAux]
State after:
case cons
α : Type u_1
x : α
xs : List α
ih : reverse xs = reverseSpec xs
⊢ reverseAux xs [x] = reverseSpec xs ++ [x]

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : reverse xs = reverseSpec xs
⊢ reverseAux xs [x] = reverseSpec xs ++ [x]
Tactic:
rw [reverseAux_spec]
State after:
case cons
α : Type u_1
x : α
xs : List α
ih : reverse xs = reverseSpec xs
⊢ reverse xs ++ [x] = reverseSpec xs ++ [x]