α : Type u
β : Type ?u.56262
w x y z : α
inst✝ : BooleanAlgebra α
h✝ : yᶜ ≤ xᶜ
h : xᶜᶜ ≤ yᶜᶜ
⊢ x ≤ y
α : Type u
β : Type ?u.56262
w x y z : α
inst✝ : BooleanAlgebra α
h : yᶜ ≤ xᶜ
⊢ x ≤ y
have h := compl_le_compl h
α : Type u
β : Type ?u.56262
w x y z : α
inst✝ : BooleanAlgebra α
h✝ : yᶜ ≤ xᶜ
h : x ≤ y
⊢ x ≤ y
α : Type u
β : Type ?u.56262
w x y z : α
inst✝ : BooleanAlgebra α
h✝ : yᶜ ≤ xᶜ
h : xᶜᶜ ≤ yᶜᶜ
⊢ x ≤ y
simp at h
no goals
α : Type u
β : Type ?u.56262
w x y z : α
inst✝ : BooleanAlgebra α
h✝ : yᶜ ≤ xᶜ
h : x ≤ y
⊢ x ≤ y
assumption