no goals
ι : Type ?u.61968
α : Type u_1
β : Type ?u.61974
π : ι → Type ?u.61979
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b \ a = b \ a
rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]