-- Mathlib/Order/BooleanAlgebra.lean
theorem le_iff_eq_sup_sdiff (hz : z ≤ y) (hx : x ≤ y) : x ≤ z ↔ y = z ⊔ y \ x :=
  ⟨fun H => by
    apply le_antisymm
    · conv_lhs => rw [← sup_inf_sdiff y x]
      apply sup_le_sup_right
      rwa [inf_eq_right.2 hx]
    · apply le_trans
      · apply sup_le_sup_right hz
      · rw [sup_sdiff_left],
    fun H => by
    conv_lhs at H => rw [← sup_sdiff_cancel_right hx]
    refine le_of_inf_le_sup_le ?_ H.le
    rw [inf_sdiff_self_right]
    exact bot_le⟩

Proof state:
case a
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ≤ z ⊔ y \ x

Tactic:
conv_lhs => rw [← sup_inf_sdiff y x]

Result:
case a
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊓ x ⊔ y \ x ≤ z ⊔ y \ x

Proof state:
case a
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊓ x ⊔ y \ x ≤ z ⊔ y \ x

Tactic:
apply sup_le_sup_right

Result:
case a.h₁
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊓ x ≤ z

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y = z ⊔ y \ x

Tactic:
apply le_antisymm

Result:
case a
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ≤ z ⊔ y \ x

case a
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ z ⊔ y \ x ≤ y

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ⊓ y \ x ≤ z ⊓ y \ x

Tactic:
rw [inf_sdiff_self_right]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ ⊥ ≤ z ⊓ y \ x

Proof state:
case a.a
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ z ⊔ y \ x ≤ ?a.b✝

Tactic:
apply sup_le_sup_right hz

Result:
no goals

Proof state:
case a.a
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊔ y \ x ≤ y

Tactic:
rw [sup_sdiff_left]

Result:
no goals

Proof state:
case a
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ z ⊔ y \ x ≤ y

Tactic:
apply le_trans

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

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

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

Proof state:
case a.h₁
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊓ x ≤ z

Tactic:
rwa [inf_eq_right.2 hx]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ ⊥ ≤ z ⊓ y \ x

Tactic:
exact bot_le

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
⊢ x ≤ z

Tactic:
conv_lhs at H => rw [← sup_sdiff_cancel_right hx]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ≤ z

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ≤ z

Tactic:
refine le_of_inf_le_sup_le ?_ H.le

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ⊓ y \ x ≤ z ⊓ y \ x