no goals
α : Type u
β : Type ?u.7223
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ x = (x ⊓ y ⊔ x \ y) ⊓ y \ x
rw [sup_inf_sdiff]
no goals
α : Type u
β : Type ?u.7223
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊔ x \ y) ⊓ y \ x = x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x
rw [inf_sup_right]
no goals
α : Type u
β : Type ?u.7223
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
rw [@inf_comm _ _ x y, inf_inf_sdiff, sdiff_inf_sdiff, bot_sup_eq]