no goals
ι : Type ?u.61584
α : Type u_1
β : Type ?u.61590
π : ι → Type ?u.61595
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
rw [sdiff_symmDiff, sdiff_sup, sup_comm]