ι : Type ?u.136551
α : Type u_1
β : Type ?u.136557
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ a \ d ≤ b ∧ a \ d ≤ c ↔ a \ b ≤ d ∧ a \ c ≤ d
ι : Type ?u.136551
α : Type u_1
β : Type ?u.136557
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ a \ (b ⊓ c) ≤ d ↔ a \ b ⊔ a \ c ≤ d
rw [sup_le_iff, sdiff_le_comm, le_inf_iff]
no goals
ι : Type ?u.136551
α : Type u_1
β : Type ?u.136557
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d✝ a b c d : α
⊢ a \ d ≤ b ∧ a \ d ≤ c ↔ a \ b ≤ d ∧ a \ c ≤ d
simp_rw [sdiff_le_comm]