no goals
α : Type u
β : Type ?u.41421
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ⊔ y \ x ⊔ x ⊓ y = (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y)
rw [sup_inf_left]
no goals
α : Type u
β : Type ?u.41421
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y) = (x \ y ⊔ x ⊔ y \ x) ⊓ (x \ y ⊔ (y \ x ⊔ y))
ac_rfl
no goals
α : Type u
β : Type ?u.41421
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x \ y ⊔ x ⊔ y \ x) ⊓ (x \ y ⊔ (y \ x ⊔ y)) = (x ⊔ y \ x) ⊓ (x \ y ⊔ y)
rw [sup_sdiff_right, sup_sdiff_right]
no goals
α : Type u
β : Type ?u.41421
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ y \ x) ⊓ (x \ y ⊔ y) = x ⊔ y
rw [sup_sdiff_self_right, sup_sdiff_self_left, inf_idem]