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

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

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

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