no goals
α : Type u
β : Type ?u.3131
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y \ x ⊔ x = y \ x ⊔ (x ⊔ x ⊓ y)
rw [sup_inf_self]
no goals
α : Type u
β : Type ?u.3131
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y \ x ⊔ (x ⊔ x ⊓ y) = y ⊓ x ⊔ y \ x ⊔ x
ac_rfl
no goals
α : Type u
β : Type ?u.3131
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊔ y \ x ⊔ x = y ⊔ x
rw [sup_inf_sdiff]