Theorem: List.reverse_dropLast (Algorithm/Data/Classes/ToList.lean)

State before:
C : Type u_1
α : Type u_2
l✝ l : List α
x head✝ : α
tail✝ : List α
⊢ (x :: head✝ :: tail✝).dropLast.reverse = (x :: head✝ :: tail✝).reverse.tail
Tactic:
rw [dropLast, reverse_cons x, reverse_cons x, reverse_dropLast (_::_),
  tail_append_of_ne_nil] <;> simp
State after:
no goals