no goals
ι : Type ?u.428249
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
l₁ l₂ : List α
⊢ map f (List.diff l₁ l₂) = List.diff (map f l₁) (map f l₂)
simp only [diff_eq_foldl, foldl_map, map_foldl_erase finj]