α : Type u_1
β : Type ?u.487540
γ : Type ?u.487543
s t u : Multiset α
⊢ Disjoint t s ∧ Disjoint u s ↔ Disjoint s t ∧ Disjoint s u
α : Type u_1
β : Type ?u.487540
γ : Type ?u.487543
s t u : Multiset α
⊢ Disjoint s (t + u) ↔ Disjoint s t ∧ Disjoint s u
rw [disjoint_comm, disjoint_add_left]
no goals
α : Type u_1
β : Type ?u.487540
γ : Type ?u.487543
s t u : Multiset α
⊢ Disjoint t s ∧ Disjoint u s ↔ Disjoint s t ∧ Disjoint s u
tauto