Theorem: List.map_dropLast (One.lean)

State before:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
⊢ map f (dropLast l) = dropLast (map f l)
Tactic:
simp only [dropLast_eq_take, map_take, length_map]
State after:
no goals