α : Type u_1
β : Type ?u.495543
γ : Type ?u.495546
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ⊆ 0 ↔ Disjoint s t
α : Type u_1
β : Type ?u.495543
γ : Type ?u.495546
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t = 0 ↔ Disjoint s t
rw [← subset_zero]
no goals
α : Type u_1
β : Type ?u.495543
γ : Type ?u.495546
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ⊆ 0 ↔ Disjoint s t
simp [subset_iff, Disjoint]