no goals
ι : Type ?u.19057
α : Type u_1
β : Type ?u.19063
π : ι → Type ?u.19068
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
⊢ a ∆ b = ⊥ ↔ a = b
simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]