Theorem: LoVe.map_append (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

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

State before:
case nil
α β : Type
f : α → β
ys : List α
⊢ map f ([] ++ ys) = map f [] ++ map f ys
Tactic:
rfl
State after:
no goals

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