α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
⊢ Disjoint s (ndinsert a t) ↔ ¬a ∈ s ∧ Disjoint s t
rw [disjoint_comm, disjoint_ndinsert_left]
no goals
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t
tauto