no goals
ι : Type ?u.87749
α : Type u_1
β : Type ?u.87755
π : ι → Type ?u.87760
inst✝ : BooleanAlgebra α
a b c d : α
⊢ (a ∆ b)ᶜ = a ⇔ b
simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]