α : Type u_1
β : Type ?u.492563
γ : Type ?u.492566
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t
α : Type u_1
β : Type ?u.492563
γ : Type ?u.492566
a : α
s t : Multiset α
⊢ Disjoint s (a ::ₘ t) ↔ ¬a ∈ s ∧ Disjoint s t
rw [disjoint_comm, disjoint_cons_left]
no goals
α : Type u_1
β : Type ?u.492563
γ : Type ?u.492566
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t
tauto