α : Type u
β : Type ?u.21257
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x \ y = x
⊢ y = ⊥
α : Type u
β : Type ?u.21257
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
⊢ x \ y < x
refine' sdiff_le.lt_of_ne fun h => hy _
α : Type u
β : Type ?u.21257
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
⊢ y = ⊥
α : Type u
β : Type ?u.21257
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x \ y = x
⊢ y = ⊥
rw [sdiff_eq_self_iff_disjoint', disjoint_iff] at h
no goals
α : Type u
β : Type ?u.21257
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
⊢ y = ⊥
rw [← h, inf_eq_right.mpr hx]