no goals
ι : Type ?u.89407
α : Type u_1
β : Type ?u.89413
π : ι → Type ?u.89418
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ∆ b = ⊤ ↔ IsCompl a b
rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff,
  codisjoint_iff, and_comm]