no goals
α : Type u
β : Type ?u.38191
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊔ x ⊓ y \ z = x ⊓ (y ⊓ z) ⊔ x ⊓ y \ z
rw [inf_assoc]
no goals
α : Type u
β : Type ?u.38191
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y ⊓ z ⊔ y \ z) = x ⊓ y
rw [sup_inf_sdiff]
no goals
α : Type u
β : Type ?u.38191
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊓ (x ⊓ y \ z) = x ⊓ x ⊓ (y ⊓ z ⊓ y \ z)
ac_rfl
no goals
α : Type u
β : Type ?u.38191
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ x ⊓ (y ⊓ z ⊓ y \ z) = ⊥
rw [inf_inf_sdiff, inf_bot_eq]