no goals
ι : Type ?u.903489
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq α
x y z : Multiset α
h : z ≤ y
⊢ x + y = x ∪ z ↔ y = z ∧ Disjoint x y
simpa only [and_comm] using add_eq_union_left_of_le h