no goals
ι : Type ?u.26272
α : Type u_1
β : Type ?u.26278
π : ι → Type ?u.26283
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
h : Disjoint a b
⊢ a ∆ b = a ⊔ b
rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]