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

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

State before:
case nil
α β γ : Type
f : α → β
g : β → γ
⊢ map g (map f []) = map (fun x => g (f x)) []
Tactic:
rfl
State after:
no goals

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