no goals
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
⊢ Disjoint (map f s) (map g t) ↔ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a ≠ g b
simp [Disjoint, @eq_comm _ (f _) (g _)]