no goals
α : Type u
β : Type ?u.28604
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ⊔ x ⊓ y ⊓ z = z ⊓ x ⊓ y ⊔ x \ y
ac_rfl
no goals
α : Type u
β : Type ?u.28604
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z ⊓ x ⊓ y ⊔ x \ y = x \ y ⊔ x ⊓ z
rw [sup_inf_inf_sdiff, sup_comm, inf_comm]