no goals
ι : Type ?u.67558
α : Type u_1
β : Type ?u.67564
π : ι → Type ?u.67569
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ b ≤ a ∆ b ↔ Disjoint a b
rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]