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

State before:
α : Type
xs ys : List α
⊢ reverse (xs ++ ys) = reverse ys ++ reverse xs
Tactic:
induction xs with
| nil           => simp [reverse]
| cons x xs' ih => simp [reverse, ih]
State after:
no goals

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

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