case a
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ≤ z ⊔ y \ x

case a
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ z ⊔ y \ x ≤ y
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y = z ⊔ y \ x
apply le_antisymm
case a
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊓ x ⊔ y \ x ≤ z ⊔ y \ x
case a
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ≤ z ⊔ y \ x
conv_lhs => rw [← sup_inf_sdiff y x]
case a.h₁
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊓ x ≤ z
case a
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊓ x ⊔ y \ x ≤ z ⊔ y \ x
apply sup_le_sup_right
no goals
case a.h₁
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊓ x ≤ z
rwa [inf_eq_right.2 hx]
case a.a
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ z ⊔ y \ x ≤ ?a.b✝

case a.a
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ ?a.b✝ ≤ y

case a.b
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ α
case a
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ z ⊔ y \ x ≤ y
apply le_trans
no goals
case a.a
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ z ⊔ y \ x ≤ ?a.b✝
apply sup_le_sup_right hz
no goals
case a.a
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊔ y \ x ≤ y
rw [sup_sdiff_left]
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ≤ z
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
⊢ x ≤ z
conv_lhs at H => rw [← sup_sdiff_cancel_right hx]
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ⊓ y \ x ≤ z ⊓ y \ x
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ≤ z
refine' le_of_inf_le_sup_le _ H.le
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ ⊥ ≤ z ⊓ y \ x
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ⊓ y \ x ≤ z ⊓ y \ x
rw [inf_sdiff_self_right]
no goals
α : Type u
β : Type ?u.15123
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ ⊥ ≤ z ⊓ y \ x
exact bot_le