no goals
ι : Type ?u.34249
α : Type u_1
β : Type ?u.34255
π : ι → Type ?u.34260
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b ∆ (a ⊓ b) = a ⊔ b
rw [← symmDiff_sdiff_inf a, sdiff_symmDiff_eq_sup, symmDiff_sup_inf]