no goals
α : Type u
β : Type ?u.19830
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
⊢ y ⊓ x ⊓ ?m.19948 h = y ⊓ z ⊓ ?m.19948 h
rw [inf_inf_sdiff, h, inf_inf_sdiff]
no goals
α : Type u
β : Type ?u.19830
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
⊢ y ⊓ x ⊔ y \ x = y ⊓ z ⊔ y \ x
rw [sup_inf_sdiff, h, sup_inf_sdiff]
no goals
α : Type u
β : Type ?u.19830
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ⊓ x = y ⊓ z
⊢ y \ x = y \ z
rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]