[GOAL]
α : Type u
β : Type u_1
w x✝ y✝ z : α
inst✝ : GeneralizedBooleanAlgebra α
x y : α
⊢ x \ y ⊔ x ⊓ y = x
[PROOFSTEP]
rw [sup_comm, sup_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x✝ y✝ z : α
inst✝ : GeneralizedBooleanAlgebra α
x y : α
⊢ x \ y ⊓ (x ⊓ y) = ⊥
[PROOFSTEP]
rw [inf_comm, inf_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
src✝ : Bot α := toBot
a : α
⊢ ⊥ ≤ a
[PROOFSTEP]
rw [← inf_inf_sdiff a a, inf_assoc]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
src✝ : Bot α := toBot
a : α
⊢ a ⊓ (a ⊓ a \ a) ≤ a
[PROOFSTEP]
exact inf_le_left
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z
[PROOFSTEP]
conv_rhs at s => rw [← sup_inf_sdiff x y, sup_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
| x
[PROOFSTEP]
rw [← sup_inf_sdiff x y, sup_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
| x
[PROOFSTEP]
rw [← sup_inf_sdiff x y, sup_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
| x
[PROOFSTEP]
rw [← sup_inf_sdiff x y, sup_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z
[PROOFSTEP]
rw [sup_comm] at s 
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z
[PROOFSTEP]
conv_rhs at i => rw [← inf_inf_sdiff x y, inf_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
| ⊥
[PROOFSTEP]
rw [← inf_inf_sdiff x y, inf_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
| ⊥
[PROOFSTEP]
rw [← inf_inf_sdiff x y, inf_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
| ⊥
[PROOFSTEP]
rw [← inf_inf_sdiff x y, inf_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = x \ y ⊓ (x ⊓ y)
⊢ x \ y = z
[PROOFSTEP]
rw [inf_comm] at i 
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : z ⊓ (x ⊓ y) = x \ y ⊓ (x ⊓ y)
⊢ x \ y = z
[PROOFSTEP]
exact (eq_of_inf_eq_sup_eq i s).symm
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y \ x ⊔ x = y \ x ⊔ (x ⊔ x ⊓ y)
[PROOFSTEP]
rw [sup_inf_self]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y \ x ⊔ (x ⊔ x ⊓ y) = y ⊓ x ⊔ y \ x ⊔ x
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊔ y \ x ⊔ x = y ⊔ x
[PROOFSTEP]
rw [sup_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ ⊥ = x ⊓ y ⊓ x \ y
[PROOFSTEP]
rw [inf_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ x \ y = x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y
[PROOFSTEP]
rw [sup_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y = (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y
[PROOFSTEP]
rw [inf_sup_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = (y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = (y ⊓ x ⊔ x ⊓ y \ x) ⊓ x \ y
[PROOFSTEP]
rw [inf_idem]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ x ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y
[PROOFSTEP]
rw [inf_sup_right, @inf_comm _ _ x y]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
[PROOFSTEP]
rw [inf_inf_sdiff, bot_sup_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ x ⊓ x \ y = x ⊓ x \ y ⊓ y \ x
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ x \ y ⊓ y \ x = x \ y ⊓ y \ x
[PROOFSTEP]
rw [inf_of_le_right sdiff_le']
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ x = (x ⊓ y ⊔ x \ y) ⊓ y \ x
[PROOFSTEP]
rw [sup_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊔ x \ y) ⊓ y \ x = x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x
[PROOFSTEP]
rw [inf_sup_right]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
[PROOFSTEP]
rw [@inf_comm _ _ x y, inf_inf_sdiff, sdiff_inf_sdiff, bot_sup_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y \ x ⊓ x = ⊥
[PROOFSTEP]
rw [inf_comm, inf_sdiff_self_right]
[GOAL]
α : Type u
β : Type u_1
w x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
src✝¹ : GeneralizedBooleanAlgebra α := inst✝
src✝ : OrderBot α := toOrderBot
y x z : α
h : y \ x ≤ z
⊢ y \ x = x ⊓ y \ x ⊔ z ⊓ y \ x
[PROOFSTEP]
rw [inf_eq_right.2 h, inf_sdiff_self_right, bot_sup_eq]
[GOAL]
α : Type u
β : Type u_1
w x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
src✝¹ : GeneralizedBooleanAlgebra α := inst✝
src✝ : OrderBot α := toOrderBot
y x z : α
h : y \ x ≤ z
⊢ y ⊔ (x ⊔ z) = y \ x ⊔ x ⊔ z
[PROOFSTEP]
rw [← sup_assoc, ← @sdiff_sup_self' _ x y]
[GOAL]
α : Type u
β : Type u_1
w x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
src✝¹ : GeneralizedBooleanAlgebra α := inst✝
src✝ : OrderBot α := toOrderBot
y x z : α
h : y \ x ≤ z
⊢ y \ x ⊔ x ⊔ z = x ⊔ z ⊔ y \ x
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x✝ y✝ z✝ : α
inst✝ : GeneralizedBooleanAlgebra α
src✝¹ : GeneralizedBooleanAlgebra α := inst✝
src✝ : OrderBot α := toOrderBot
y x z : α
h : y ≤ x ⊔ z
⊢ x ⊔ z ⊔ x ≤ z ⊔ x
[PROOFSTEP]
rw [sup_assoc, sup_comm, sup_assoc, sup_idem]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x ≤ y \ z
[PROOFSTEP]
rw [← h.2.sdiff_eq_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x \ z ≤ y \ z
[PROOFSTEP]
exact sdiff_le_sdiff_right h.1
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ y ⊓ x ⊔ z = y
[PROOFSTEP]
rw [h, hs]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ y ⊓ x ⊓ z = ⊥
[PROOFSTEP]
rw [h, hi.eq_bot]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : y ≤ x ⊔ z
⊢ y ⊓ x ⊔ z = y
[PROOFSTEP]
rw [← inf_eq_right] at hs 
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ y ⊓ x ⊔ z = y
[PROOFSTEP]
rwa [sup_inf_right, inf_sup_right, @sup_comm _ _ x, inf_sup_self, inf_comm, @sup_comm _ _ z, hs, sup_eq_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : y ≤ x ⊔ z
⊢ y ⊓ x ⊓ z = ⊥
[PROOFSTEP]
rw [inf_assoc, hd.eq_bot, inf_bot_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ x ⊔ y \ x
[PROOFSTEP]
rw [sup_sdiff_cancel_right hx]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ y
[PROOFSTEP]
refine' le_trans (sup_le_sup_left sdiff_le z) _
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y ≤ y
[PROOFSTEP]
rw [sup_eq_right.2 hz]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ z ⊓ y \ x = ⊥ ↔ z ≤ x
[PROOFSTEP]
rw [← disjoint_iff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ Disjoint z (y \ x) ↔ z ≤ x
[PROOFSTEP]
exact disjoint_sdiff_iff_le hz hx
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y = z ⊔ y \ x
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ≤ z ⊔ y \ x
[PROOFSTEP]
conv_lhs => rw [← sup_inf_sdiff y x]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
| y
[PROOFSTEP]
rw [← sup_inf_sdiff y x]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
| y
[PROOFSTEP]
rw [← sup_inf_sdiff y x]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
| y
[PROOFSTEP]
rw [← sup_inf_sdiff y x]
[GOAL]
case a
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊓ x ⊔ y \ x ≤ z ⊔ y \ x
[PROOFSTEP]
apply sup_le_sup_right
[GOAL]
case a.h₁
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊓ x ≤ z
[PROOFSTEP]
rwa [inf_eq_right.2 hx]
[GOAL]
case a
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ z ⊔ y \ x ≤ y
[PROOFSTEP]
apply le_trans
[GOAL]
case a.a
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ z ⊔ y \ x ≤ ?a.b✝
[PROOFSTEP]
apply sup_le_sup_right hz
[GOAL]
case a.a
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ≤ z
⊢ y ⊔ y \ x ≤ y
[PROOFSTEP]
rw [sup_sdiff_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
⊢ x ≤ z
[PROOFSTEP]
conv_lhs at H => rw [← sup_sdiff_cancel_right hx]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
| y
[PROOFSTEP]
rw [← sup_sdiff_cancel_right hx]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
| y
[PROOFSTEP]
rw [← sup_sdiff_cancel_right hx]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : y = z ⊔ y \ x
| y
[PROOFSTEP]
rw [← sup_sdiff_cancel_right hx]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ x ≤ z
[PROOFSTEP]
refine' le_of_inf_le_sup_le _ H.le
[GOAL]
α : Type u
β : Type u_1
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
[PROOFSTEP]
rw [inf_sdiff_self_right]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ ⊥ ≤ z ⊓ y \ x
[PROOFSTEP]
exact bot_le
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ (x ⊔ z) ⊔ y \ x ⊓ y \ z = (y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z)
[PROOFSTEP]
rw [sup_inf_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z) = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)
[PROOFSTEP]
rw [@inf_sup_left _ _ y]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z) = (y ⊓ z ⊔ (y ⊓ x ⊔ y \ x)) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z))
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ z ⊔ (y ⊓ x ⊔ y \ x)) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z)) = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y)
[PROOFSTEP]
rw [sup_inf_sdiff, sup_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y) = (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x) = y
[PROOFSTEP]
rw [sup_inf_self, sup_inf_self, inf_idem]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ (x ⊔ z) ⊓ (y \ x ⊓ y \ z) = (y ⊓ x ⊔ y ⊓ z) ⊓ (y \ x ⊓ y \ z)
[PROOFSTEP]
rw [inf_sup_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ x ⊔ y ⊓ z) ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z)
[PROOFSTEP]
rw [inf_sup_right]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ y \ x ⊓ y \ z ⊔ y \ x ⊓ (y \ z ⊓ (y ⊓ z))
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y ⊓ x ⊓ y \ x ⊓ y \ z ⊔ y \ x ⊓ (y \ z ⊓ (y ⊓ z)) = ⊥
[PROOFSTEP]
rw [inf_inf_sdiff, bot_inf_eq, bot_sup_eq, @inf_comm _ _ (y \ z), inf_inf_sdiff, inf_bot_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
⊢ y ⊓ x ⊓ ?m.20593 h = y ⊓ z ⊓ ?m.20593 h
[PROOFSTEP]
rw [inf_inf_sdiff, h, inf_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
⊢ y ⊓ x ⊔ y \ x = y ⊓ z ⊔ y \ x
[PROOFSTEP]
rw [sup_inf_sdiff, h, sup_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ⊓ x = y ⊓ z
⊢ y \ x = y \ z
[PROOFSTEP]
rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = x ↔ x \ y = x \ ⊥
[PROOFSTEP]
rw [sdiff_bot]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y = x ⊓ ⊥ ↔ Disjoint y x
[PROOFSTEP]
rw [inf_bot_eq, inf_comm, disjoint_iff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = x ↔ Disjoint x y
[PROOFSTEP]
rw [sdiff_eq_self_iff_disjoint, disjoint_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
⊢ x \ y < x
[PROOFSTEP]
refine' sdiff_le.lt_of_ne fun h => hy _
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x \ y = x
⊢ y = ⊥
[PROOFSTEP]
rw [sdiff_eq_self_iff_disjoint', disjoint_iff] at h 
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
⊢ y = ⊥
[PROOFSTEP]
rw [← h, inf_eq_right.mpr hx]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊔ y \ z = x ⊓ (y ⊓ z) ⊔ y \ z
[PROOFSTEP]
rw [inf_assoc]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y ⊓ z) ⊔ y \ z = (x ⊔ y \ z) ⊓ y
[PROOFSTEP]
rw [sup_inf_right, sup_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ y \ z) ⊓ y = x ⊓ y ⊔ y \ z
[PROOFSTEP]
rw [inf_sup_right, inf_sdiff_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z
[PROOFSTEP]
rw [sup_comm, inf_comm, ← inf_assoc, sup_inf_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = z ⊓ x ⊔ x \ y
[PROOFSTEP]
apply sdiff_unique
[GOAL]
case s
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x
[PROOFSTEP]
calc
  x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) := by rw [sup_inf_right]
  _ = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) := by ac_rfl
  _ = x ⊓ (y \ z ⊔ x ⊓ z ⊔ x \ y) := by rw [sup_inf_self, sup_sdiff_left, ← sup_assoc]
  _ = x ⊓ (y \ z ⊓ (z ⊔ y) ⊔ x ⊓ (z ⊔ y) ⊔ x \ y) := by
    rw [sup_inf_left, sdiff_sup_self', inf_sup_right, @sup_comm _ _ y]
  _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) := by rw [inf_sdiff_sup_right, @inf_sup_left _ _ x z y]
  _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) := by ac_rfl
  _ = x ⊓ (y \ z ⊔ (x ⊔ x ⊓ z)) := by rw [sup_inf_sdiff, @sup_comm _ _ (x ⊓ z)]
  _ = x := by rw [sup_inf_self, sup_comm, inf_sup_self]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y))
[PROOFSTEP]
rw [sup_inf_right]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y))
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ x ⊓ z ⊔ x \ y)
[PROOFSTEP]
rw [sup_inf_self, sup_sdiff_left, ← sup_assoc]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ x ⊓ z ⊔ x \ y) = x ⊓ (y \ z ⊓ (z ⊔ y) ⊔ x ⊓ (z ⊔ y) ⊔ x \ y)
[PROOFSTEP]
rw [sup_inf_left, sdiff_sup_self', inf_sup_right, @sup_comm _ _ y]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ (z ⊔ y) ⊔ x ⊓ (z ⊔ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
[PROOFSTEP]
rw [inf_sdiff_sup_right, @inf_sup_left _ _ x z y]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y)))
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) = x ⊓ (y \ z ⊔ (x ⊔ x ⊓ z))
[PROOFSTEP]
rw [sup_inf_sdiff, @sup_comm _ _ (x ⊓ z)]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ (x ⊔ x ⊓ z)) = x
[PROOFSTEP]
rw [sup_inf_self, sup_comm, inf_sup_self]
[GOAL]
case i
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
[PROOFSTEP]
calc
  x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by rw [inf_sup_left]
  _ = x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by ac_rfl
  _ = x ⊓ y \ z ⊓ x \ y := by rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]
  _ = x ⊓ (y \ z ⊓ y) ⊓ x \ y := by conv_lhs => rw [← inf_sdiff_left]
  _ = x ⊓ (y \ z ⊓ (y ⊓ x \ y)) := by ac_rfl
  _ = ⊥ := by rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y
[PROOFSTEP]
rw [inf_sup_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y = x ⊓ y \ z ⊓ x \ y
[PROOFSTEP]
rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ z ⊓ x \ y = x ⊓ (y \ z ⊓ y) ⊓ x \ y
[PROOFSTEP]
conv_lhs => rw [← inf_sdiff_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
| x ⊓ y \ z ⊓ x \ y
[PROOFSTEP]
rw [← inf_sdiff_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
| x ⊓ y \ z ⊓ x \ y
[PROOFSTEP]
rw [← inf_sdiff_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
| x ⊓ y \ z ⊓ x \ y
[PROOFSTEP]
rw [← inf_sdiff_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ y) ⊓ x \ y = x ⊓ (y \ z ⊓ (y ⊓ x \ y))
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊓ (y ⊓ x \ y)) = ⊥
[PROOFSTEP]
rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ⊔ x ⊓ y ⊓ z = z ⊓ x ⊓ y ⊔ x \ y
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z ⊓ x ⊓ y ⊔ x \ y = x \ y ⊔ x ⊓ z
[PROOFSTEP]
rw [sup_inf_inf_sdiff, sup_comm, inf_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : z ≤ x
⊢ x \ (y \ z) = x \ y ⊔ z
[PROOFSTEP]
rw [sdiff_sdiff_right', inf_eq_right.2 h]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (x \ y) = x ⊓ y
[PROOFSTEP]
rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ≤ x
⊢ x \ (x \ y) = y
[PROOFSTEP]
rw [sdiff_sdiff_right_self, inf_of_le_right h]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hy : y ≤ x
h : x \ y = z
⊢ x \ z = y
[PROOFSTEP]
rw [← h, sdiff_sdiff_eq_self hy]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hxz : x ≤ z
hyz : y ≤ z
h : z \ x = z \ y
⊢ x = y
[PROOFSTEP]
rw [← sdiff_sdiff_eq_self hxz, h, sdiff_sdiff_eq_self hyz]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x \ y) \ z = x \ y ⊓ x \ z
[PROOFSTEP]
rw [sdiff_sdiff_left, sdiff_sup]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ (x \ y ⊔ y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
[PROOFSTEP]
rw [sdiff_sup, sdiff_sdiff_right, sdiff_sdiff_right]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
[PROOFSTEP]
rw [sup_inf_left, sup_comm, sup_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
[PROOFSTEP]
rw [sup_inf_left, @sup_comm _ _ (z \ y), sup_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x)) = z ⊓ z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z ⊓ z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)
[PROOFSTEP]
rw [inf_idem]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ (x \ y) ⊓ z \ (y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
[PROOFSTEP]
rw [sdiff_sdiff_right, sdiff_sdiff_right]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = (z \ x ⊔ z ⊓ y ⊓ x) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ z ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
[PROOFSTEP]
rw [sup_inf_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊓ z ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
[PROOFSTEP]
rw [sup_inf_right, sup_sdiff_self_right, inf_sup_right, inf_sdiff_sup_right]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) = (y ⊓ x ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z)
[PROOFSTEP]
rw [inf_sup_self, sup_inf_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ x ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z
[PROOFSTEP]
rw [@inf_comm _ _ y, sup_inf_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊓ (x \ z ⊓ y \ z) = x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z = ⊥
[PROOFSTEP]
rw [inf_sdiff_self_right, inf_bot_eq, bot_inf_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊔ x ⊓ y \ z = x ⊓ (y ⊓ z) ⊔ x ⊓ y \ z
[PROOFSTEP]
rw [inf_assoc]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y ⊓ z ⊔ y \ z) = x ⊓ y
[PROOFSTEP]
rw [sup_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊓ (x ⊓ y \ z) = x ⊓ x ⊓ (y ⊓ z ⊓ y \ z)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ x ⊓ (y ⊓ z ⊓ y \ z) = ⊥
[PROOFSTEP]
rw [inf_inf_sdiff, inf_bot_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ z ⊓ y = (x ⊓ y) \ z
[PROOFSTEP]
rw [@inf_comm _ _ x, inf_comm, inf_sdiff_assoc]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
[PROOFSTEP]
rw [sdiff_inf, sdiff_eq_bot_iff.2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)
[PROOFSTEP]
simp_rw [@inf_comm _ _ _ c, inf_sdiff_distrib_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ Disjoint (x \ z) y ↔ Disjoint x (y \ z)
[PROOFSTEP]
simp_rw [disjoint_iff, inf_sdiff_right_comm, inf_sdiff_assoc]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ⊔ y \ x ⊔ x ⊓ y = (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y)
[PROOFSTEP]
rw [sup_inf_left]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y) = (x \ y ⊔ x ⊔ y \ x) ⊓ (x \ y ⊔ (y \ x ⊔ y))
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x \ y ⊔ x ⊔ y \ x) ⊓ (x \ y ⊔ (y \ x ⊔ y)) = (x ⊔ y \ x) ⊓ (x \ y ⊔ y)
[PROOFSTEP]
rw [sup_sdiff_right, sup_sdiff_right]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ y \ x) ⊓ (x \ y ⊔ y) = x ⊔ y
[PROOFSTEP]
rw [sup_sdiff_self_right, sup_sdiff_self_left, inf_idem]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < z
[PROOFSTEP]
rw [← sup_sdiff_cancel_right hxz]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < x ⊔ z \ x
[PROOFSTEP]
refine' (sup_le_sup_left h.le _).lt_of_not_le fun h' => h.not_le _
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ z \ x ≤ y
[PROOFSTEP]
rw [← sdiff_idem]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ (z \ x) \ x ≤ y
[PROOFSTEP]
exact (sdiff_le_sdiff_of_sup_le_sup_left h').trans sdiff_le
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z
[PROOFSTEP]
rw [← sdiff_sup_cancel hyz]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z \ y ⊔ y
[PROOFSTEP]
refine' (sup_le_sup_right h.le _).lt_of_not_le fun h' => h.not_le _
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ z \ y ≤ x
[PROOFSTEP]
rw [← sdiff_idem]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ (z \ y) \ y ≤ x
[PROOFSTEP]
exact (sdiff_le_sdiff_of_sup_le_sup_right h').trans sdiff_le
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : OrderTop α
src✝² : GeneralizedBooleanAlgebra α := inst✝¹
src✝¹ : OrderBot α := toOrderBot
src✝ : OrderTop α := inst✝
x✝¹ x✝ : α
⊢ x✝¹ \ x✝ = x✝¹ ⊓ x✝ᶜ
[PROOFSTEP]
erw [← inf_sdiff_assoc, inf_top_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
src✝ : BooleanAlgebra α := inst✝
a b : α
⊢ a ⊓ b ⊔ a \ b = a
[PROOFSTEP]
rw [sdiff_eq, ← inf_sup_left, sup_compl_eq_top, inf_top_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
src✝ : BooleanAlgebra α := inst✝
a b : α
⊢ a ⊓ b ⊓ a \ b = ⊥
[PROOFSTEP]
rw [sdiff_eq, ← inf_inf_distrib_left, inf_compl_eq_bot', inf_bot_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
src✝¹ : BooleanAlgebra α := inst✝
src✝ : GeneralizedCoheytingAlgebra α := GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra
a b c : α
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c
[PROOFSTEP]
rw [himp_eq, isCompl_compl.le_sup_right_iff_inf_left_le]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
src✝¹ : BooleanAlgebra α := inst✝
src✝ : GeneralizedCoheytingAlgebra α := GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra
a : α
⊢ ⊤ \ a = ￢a
[PROOFSTEP]
rw [sdiff_eq, top_inf_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
src✝¹ : BooleanAlgebra α := inst✝
src✝ : GeneralizedCoheytingAlgebra α := GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra
a : α
⊢ aᶜ = ￢a
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl x y
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl yᶜ y
[PROOFSTEP]
exact isCompl_compl.symm
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x y
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x xᶜ
[PROOFSTEP]
exact isCompl_compl
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
⊢ xᶜ = y ↔ yᶜ = x
[PROOFSTEP]
rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
⊢ x = yᶜ ↔ y = xᶜ
[PROOFSTEP]
rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
h : yᶜ ≤ xᶜ
⊢ x ≤ y
[PROOFSTEP]
have h := compl_le_compl h
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
h✝ : yᶜ ≤ xᶜ
h : xᶜᶜ ≤ yᶜᶜ
⊢ x ≤ y
[PROOFSTEP]
simp at h 
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
h✝ : yᶜ ≤ xᶜ
h : x ≤ y
⊢ x ≤ y
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
h : yᶜ ≤ x
⊢ xᶜ ≤ y
[PROOFSTEP]
simpa only [compl_compl] using compl_le_compl h
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ≤ x ↔ x = ⊤
[PROOFSTEP]
simpa using le_compl_self (a := xᶜ)
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : Nontrivial α
⊢ xᶜ < x ↔ x = ⊤
[PROOFSTEP]
simpa using lt_compl_self (a := xᶜ)
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
⊢ x \ yᶜ = x ⊓ y
[PROOFSTEP]
rw [sdiff_eq, compl_compl]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
⊢ x ⊓ y ⊔ x ⊓ yᶜ = x
[PROOFSTEP]
rw [← sdiff_eq, sup_inf_sdiff _ _]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
⊢ (x \ y)ᶜ = x ⇨ y
[PROOFSTEP]
rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
⊢ xᶜ \ yᶜ = y \ x
[PROOFSTEP]
rw [sdiff_compl, sdiff_eq, inf_comm]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
⊢ Disjoint xᶜ y ↔ y ≤ x
[PROOFSTEP]
rw [← le_compl_iff_disjoint_left, compl_compl]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝ : BooleanAlgebra α
⊢ Disjoint x yᶜ ↔ x ≤ y
[PROOFSTEP]
rw [← le_compl_iff_disjoint_right, compl_compl]
[GOAL]
α✝ : Type u
β✝ : Type u_1
w x✝ y z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x : α × β
⊢ x ⊓ xᶜ ≤ ⊥
[PROOFSTEP]
constructor
[GOAL]
case left
α✝ : Type u
β✝ : Type u_1
w x✝ y z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x : α × β
⊢ (x ⊓ xᶜ).fst ≤ ⊥.fst
[PROOFSTEP]
simp
[GOAL]
case right
α✝ : Type u
β✝ : Type u_1
w x✝ y z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x : α × β
⊢ (x ⊓ xᶜ).snd ≤ ⊥.snd
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β✝ : Type u_1
w x✝ y z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x : α × β
⊢ ⊤ ≤ x ⊔ xᶜ
[PROOFSTEP]
constructor
[GOAL]
case left
α✝ : Type u
β✝ : Type u_1
w x✝ y z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x : α × β
⊢ ⊤.fst ≤ (x ⊔ xᶜ).fst
[PROOFSTEP]
simp
[GOAL]
case right
α✝ : Type u
β✝ : Type u_1
w x✝ y z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x : α × β
⊢ ⊤.snd ≤ (x ⊔ xᶜ).snd
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β✝ : Type u_1
w x✝ y✝ z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x y : α × β
⊢ x \ y = x ⊓ yᶜ
[PROOFSTEP]
ext
[GOAL]
case h₁
α✝ : Type u
β✝ : Type u_1
w x✝ y✝ z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x y : α × β
⊢ (x \ y).fst = (x ⊓ yᶜ).fst
[PROOFSTEP]
simp [sdiff_eq]
[GOAL]
case h₂
α✝ : Type u
β✝ : Type u_1
w x✝ y✝ z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x y : α × β
⊢ (x \ y).snd = (x ⊓ yᶜ).snd
[PROOFSTEP]
simp [sdiff_eq]
[GOAL]
α✝ : Type u
β✝ : Type u_1
w x✝ y✝ z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x y : α × β
⊢ x ⇨ y = y ⊔ xᶜ
[PROOFSTEP]
ext
[GOAL]
case h₁
α✝ : Type u
β✝ : Type u_1
w x✝ y✝ z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x y : α × β
⊢ (x ⇨ y).fst = (y ⊔ xᶜ).fst
[PROOFSTEP]
simp [himp_eq]
[GOAL]
case h₂
α✝ : Type u
β✝ : Type u_1
w x✝ y✝ z : α✝
α : Type ?u.67933
β : Type ?u.67936
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
src✝¹ : HeytingAlgebra (α × β) := heytingAlgebra
src✝ : DistribLattice (α × β) := distribLattice α β
x y : α × β
⊢ (x ⇨ y).snd = (y ⊔ xᶜ).snd
[PROOFSTEP]
simp [himp_eq]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
src✝¹ : LinearOrder Bool := Bool.linearOrder
src✝ : BoundedOrder Bool := Bool.boundedOrder
⊢ ∀ (x y z : Bool), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
[PROOFSTEP]
decide
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝¹ : GeneralizedCoheytingAlgebra α := Injective.generalizedCoheytingAlgebra f hf map_sup map_inf map_bot map_sdiff
src✝ : DistribLattice α := Injective.distribLattice f hf map_sup map_inf
a b : α
⊢ f (a ⊓ b ⊔ a \ b) = f a
[PROOFSTEP]
erw [map_sup, map_sdiff, map_inf, sup_inf_sdiff]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝⁴ : Sup α
inst✝³ : Inf α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝¹ : GeneralizedCoheytingAlgebra α := Injective.generalizedCoheytingAlgebra f hf map_sup map_inf map_bot map_sdiff
src✝ : DistribLattice α := Injective.distribLattice f hf map_sup map_inf
a b : α
⊢ f (a ⊓ b ⊓ a \ b) = f ⊥
[PROOFSTEP]
erw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HasCompl α
inst✝¹ : SDiff α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝ : GeneralizedBooleanAlgebra α := Injective.generalizedBooleanAlgebra f hf map_sup map_inf map_bot map_sdiff
a : α
⊢ f a ⊓ f aᶜ = f ⊥
[PROOFSTEP]
rw [map_compl, inf_compl_eq_bot, map_bot]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HasCompl α
inst✝¹ : SDiff α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝ : GeneralizedBooleanAlgebra α := Injective.generalizedBooleanAlgebra f hf map_sup map_inf map_bot map_sdiff
a : α
⊢ f a ⊔ f aᶜ = f ⊤
[PROOFSTEP]
rw [map_compl, sup_compl_eq_top, map_top]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HasCompl α
inst✝¹ : SDiff α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝ : GeneralizedBooleanAlgebra α := Injective.generalizedBooleanAlgebra f hf map_sup map_inf map_bot map_sdiff
a b : α
⊢ a \ b = a ⊓ bᶜ
[PROOFSTEP]
refine hf ((map_sdiff _ _).trans (sdiff_eq.trans ?_))
[GOAL]
α : Type u
β : Type u_1
w x y z : α
inst✝⁶ : Sup α
inst✝⁵ : Inf α
inst✝⁴ : Top α
inst✝³ : Bot α
inst✝² : HasCompl α
inst✝¹ : SDiff α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
src✝ : GeneralizedBooleanAlgebra α := Injective.generalizedBooleanAlgebra f hf map_sup map_inf map_bot map_sdiff
a b : α
⊢ f a ⊓ (f b)ᶜ = f (a ⊓ bᶜ)
[PROOFSTEP]
rw [map_inf, map_compl]
[GOAL]
α : Type u
β : Type u_1
w x y z : α
⊢ BooleanAlgebra PUnit
[PROOFSTEP]
refine' { PUnit.biheytingAlgebra with .. }
[GOAL]
case refine'_1
α : Type u
β : Type u_1
w x y z : α
src✝ : BiheytingAlgebra PUnit := biheytingAlgebra
⊢ ∀ (x y z : PUnit), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
β : Type u_1
w x y z : α
src✝ : BiheytingAlgebra PUnit := biheytingAlgebra
x✝ y✝ z✝ : PUnit
⊢ (x✝ ⊔ y✝) ⊓ (x✝ ⊔ z✝) ≤ x✝ ⊔ y✝ ⊓ z✝
[PROOFSTEP]
trivial
[GOAL]
case refine'_2
α : Type u
β : Type u_1
w x y z : α
src✝ : BiheytingAlgebra PUnit := biheytingAlgebra
⊢ ∀ (x : PUnit), x ⊓ xᶜ ≤ ⊥
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u
β : Type u_1
w x y z : α
src✝ : BiheytingAlgebra PUnit := biheytingAlgebra
x✝ : PUnit
⊢ x✝ ⊓ x✝ᶜ ≤ ⊥
[PROOFSTEP]
trivial
[GOAL]
case refine'_3
α : Type u
β : Type u_1
w x y z : α
src✝ : BiheytingAlgebra PUnit := biheytingAlgebra
⊢ ∀ (x : PUnit), ⊤ ≤ x ⊔ xᶜ
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
β : Type u_1
w x y z : α
src✝ : BiheytingAlgebra PUnit := biheytingAlgebra
x✝ : PUnit
⊢ ⊤ ≤ x✝ ⊔ x✝ᶜ
[PROOFSTEP]
trivial
[GOAL]
case refine'_4
α : Type u
β : Type u_1
w x y z : α
src✝ : BiheytingAlgebra PUnit := biheytingAlgebra
⊢ ∀ (x y : PUnit), x \ y = x ⊓ yᶜ
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u
β : Type u_1
w x y z : α
src✝ : BiheytingAlgebra PUnit := biheytingAlgebra
x✝ y✝ : PUnit
⊢ x✝ \ y✝ = x✝ ⊓ y✝ᶜ
[PROOFSTEP]
trivial
[GOAL]
case refine'_5
α : Type u
β : Type u_1
w x y z : α
src✝ : BiheytingAlgebra PUnit := biheytingAlgebra
⊢ ∀ (x y : PUnit), x ⇨ y = y ⊔ xᶜ
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type u
β : Type u_1
w x y z : α
src✝ : BiheytingAlgebra PUnit := biheytingAlgebra
x✝ y✝ : PUnit
⊢ x✝ ⇨ y✝ = y✝ ⊔ x✝ᶜ
[PROOFSTEP]
trivial
