Theorem: LoVe.reverse_append (LoVe/Lectures/LoVe04_ForwardProofs_Demo.lean)

State before:
α : Type
ys : List α
⊢ reverse ([] ++ ys) = reverse ys ++ reverse []
Tactic:
simp [reverse]
State after:
no goals

State before:
α : Type
x : α
xs ys : List α
⊢ reverse (x :: xs ++ ys) = reverse ys ++ reverse (x :: xs)
Tactic:
simp [reverse, reverse_append xs]
State after:
no goals