no goals
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ Disjoint x (y ∪ z) ↔ Disjoint x y ∧ Disjoint x z
rw [Disjoint.symm_iff, disjoint_union_left, Disjoint.symm_iff _ x, Disjoint.symm_iff _ x]