no goals
α : Type u
β : Type v
γ : Type w
as : List α
f : α → β
⊢ length (map f as) = length as
induction as with
| nil => simp [List.map]
| cons _ as ih => simp [List.map, ih]
no goals
case nil
α : Type u
β : Type v
γ : Type w
f : α → β
⊢ length (map f nil) = length nil
simp [List.map]
no goals
case cons
α : Type u
β : Type v
γ : Type w
f : α → β
head✝ : α
as : List α
ih : length (map f as) = length as
⊢ length (map f (head✝ :: as)) = length (head✝ :: as)
simp [List.map, ih]