no goals
α : Type u
β : Type ?u.12230
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ y ⊓ x ⊔ z = y
rw [h, hs]
no goals
α : Type u
β : Type ?u.12230
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ y ⊓ x ⊓ z = ⊥
rw [h, hi.eq_bot]