no goals
α : Type u_2
β : Type u_1
γ : Type ?u.168994
inst✝¹ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
s t : Multiset α
l₁ l₂ : List α
⊢ List.map f (List.diff l₁ l₂ ++ l₂) = List.diff (List.map f l₁) (List.map f l₂) ++ List.map f l₂
rw [List.map_append f, List.map_diff finj]