no goals
ι : Type ?u.21355
α : Type u_1
β : Type ?u.21361
π : ι → Type ?u.21366
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
simp_rw [symmDiff, sup_le_iff, sdiff_le_iff]