no goals
α : Type u
β : Type ?u.22731
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊔ y \ z = x ⊓ (y ⊓ z) ⊔ y \ z
rw [inf_assoc]
no goals
α : Type u
β : Type ?u.22731
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y ⊓ z) ⊔ y \ z = (x ⊔ y \ z) ⊓ y
rw [sup_inf_right, sup_inf_sdiff]
no goals
α : Type u
β : Type ?u.22731
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ y \ z) ⊓ y = x ⊓ y ⊔ y \ z
rw [inf_sup_right, inf_sdiff_left]