Theorem: reverse_append (LAMR/Examples/using_lean_as_a_proof_assistant/induction.lean)

State before:
α : Type
as bs cs : List α
a b c : α
⊢ reverse (as ++ bs) = reverse bs ++ reverse as
Tactic:
rw [reverse, reverseAux_append, reverse, ←reverseAux_append', nil_append,
    reverse]
State after:
no goals