[GOAL]
P : Type u_1
inst✝ : Preorder P
x y : P
F s t : PFilter P
p q : P
⊢ principal q ≤ principal p ↔ p ≤ q
[PROOFSTEP]
simp
[GOAL]
P : Type u_1
inst✝ : CompleteSemilatticeInf P
F✝ : PFilter P
x : P
F : (PFilter P)ᵒᵈ
⊢ (fun x => ↑toDual (principal x)) x ≤ F ↔ x ≤ (fun F => sInf ↑(↑ofDual F)) F
[PROOFSTEP]
simp
[GOAL]
P : Type u_1
inst✝ : CompleteSemilatticeInf P
F✝ : PFilter P
x : P
F : (PFilter P)ᵒᵈ
⊢ ↑toDual (principal x) ≤ F ↔ ∀ (b : P), b ∈ ↑ofDual F → x ≤ b
[PROOFSTEP]
rfl


[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


[GOAL]
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ¬Acc r a
⊢ ∃ b, ¬Acc r b ∧ r b a
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
⊢ Acc r a
[PROOFSTEP]
refine' ⟨_, fun b hr => _⟩
[GOAL]
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
⊢ Acc r b
[PROOFSTEP]
by_contra hb
[GOAL]
α : Type u_1
r✝ : α → α → Prop
inst✝ : IsStrictOrder α r✝
a : α
r : α → α → Prop
h : ∀ (b : α), ¬Acc r b → ¬r b a
b : α
hr : r b a
hb : ¬Acc r b
⊢ False
[PROOFSTEP]
exact h b hb hr
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ Acc r x ↔ IsEmpty { f // x ∈ Set.range ↑f }
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ Acc r x → IsEmpty { f // x ∈ Set.range ↑f }
[PROOFSTEP]
refine' fun h => h.recOn fun x _ IH => _
[GOAL]
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ↑f }
⊢ IsEmpty { f // x ∈ Set.range ↑f }
[PROOFSTEP]
constructor
[GOAL]
case mp.false
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ↑f }
⊢ { f // x ∈ Set.range ↑f } → False
[PROOFSTEP]
rintro ⟨f, k, hf⟩
[GOAL]
case mp.false.mk.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ↑f }
f : (fun x x_1 => x > x_1) ↪r r
k : ℕ
hf : ↑f k = x
⊢ False
[PROOFSTEP]
exact IsEmpty.elim' (IH (f (k + 1)) (hf ▸ f.map_rel_iff.2 (lt_add_one k))) ⟨f, _, rfl⟩
[GOAL]
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ IsEmpty { f // x ∈ Set.range ↑f } → Acc r x
[PROOFSTEP]
have : ∀ x : { a // ¬Acc r a }, ∃ y : { a // ¬Acc r a }, r y.1 x.1 :=
  by
  rintro ⟨x, hx⟩
  cases exists_not_acc_lt_of_not_acc hx with
  | intro w h => exact ⟨⟨w, h.1⟩, h.2⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mk
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝ x : α
hx : ¬Acc r x
⊢ ∃ y, r ↑y ↑{ val := x, property := hx }
[PROOFSTEP]
cases exists_not_acc_lt_of_not_acc hx with
| intro w h => exact ⟨⟨w, h.1⟩, h.2⟩
[GOAL]
case mk
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ x : α
hx : ¬Acc r x
x✝ : ∃ b, ¬Acc r b ∧ r b x
⊢ ∃ y, r ↑y ↑{ val := x, property := hx }
[PROOFSTEP]
cases exists_not_acc_lt_of_not_acc hx with
| intro w h => exact ⟨⟨w, h.1⟩, h.2⟩
[GOAL]
case mk.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝ x : α
hx : ¬Acc r x
w : α
h : ¬Acc r w ∧ r w x
⊢ ∃ y, r ↑y ↑{ val := x, property := hx }
[PROOFSTEP]

| intro w h => exact ⟨⟨w, h.1⟩, h.2⟩
[GOAL]
case mk.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝ x : α
hx : ¬Acc r x
w : α
h : ¬Acc r w ∧ r w x
⊢ ∃ y, r ↑y ↑{ val := x, property := hx }
[PROOFSTEP]
exact ⟨⟨w, h.1⟩, h.2⟩
[GOAL]
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
this : ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
⊢ IsEmpty { f // x ∈ Set.range ↑f } → Acc r x
[PROOFSTEP]
obtain ⟨f, h⟩ := Classical.axiom_of_choice this
[GOAL]
case mpr.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
this : ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
⊢ IsEmpty { f // x ∈ Set.range ↑f } → Acc r x
[PROOFSTEP]
refine' fun E => by_contradiction fun hx => E.elim' ⟨natGT (fun n => (f^[n] ⟨x, hx⟩).1) fun n => _, 0, rfl⟩
[GOAL]
case mpr.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
this : ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
E : IsEmpty { f // x ∈ Set.range ↑f }
hx : ¬Acc r x
n : ℕ
⊢ r ((fun n => ↑(f^[n] { val := x, property := hx })) (n + 1)) ((fun n => ↑(f^[n] { val := x, property := hx })) n)
[PROOFSTEP]
simp only [Function.iterate_succ']
[GOAL]
case mpr.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
this : ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
E : IsEmpty { f // x ∈ Set.range ↑f }
hx : ¬Acc r x
n : ℕ
⊢ r ↑((f ∘ f^[n]) { val := x, property := hx }) ↑(f^[n] { val := x, property := hx })
[PROOFSTEP]
apply h
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
k : ℕ
⊢ ¬Acc r (↑f k)
[PROOFSTEP]
rw [acc_iff_no_decreasing_seq, not_isEmpty_iff]
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
k : ℕ
⊢ Nonempty { f_1 // ↑f k ∈ Set.range ↑f_1 }
[PROOFSTEP]
exact ⟨⟨f, k, rfl⟩⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
⊢ WellFounded r ↔ IsEmpty ((fun x x_1 => x > x_1) ↪r r)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
⊢ WellFounded r → IsEmpty ((fun x x_1 => x > x_1) ↪r r)
[PROOFSTEP]
rintro ⟨h⟩
[GOAL]
case mp.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
h : ∀ (a : α), Acc r a
⊢ IsEmpty ((fun x x_1 => x > x_1) ↪r r)
[PROOFSTEP]
exact ⟨fun f => not_acc_of_decreasing_seq f 0 (h _)⟩
[GOAL]
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
⊢ IsEmpty ((fun x x_1 => x > x_1) ↪r r) → WellFounded r
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
h : IsEmpty ((fun x x_1 => x > x_1) ↪r r)
⊢ WellFounded r
[PROOFSTEP]
exact ⟨fun x => acc_iff_no_decreasing_seq.2 inferInstance⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
⊢ ¬WellFounded r
[PROOFSTEP]
rw [wellFounded_iff_no_descending_seq, not_isEmpty_iff]
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x x_1 => x > x_1) ↪r r
⊢ Nonempty ((fun x x_1 => x > x_1) ↪r r)
[PROOFSTEP]
exact ⟨f⟩
[GOAL]
α : Type u_1
s : Set ℕ
inst✝ : Infinite ↑s
⊢ ℕ ≃o ↑s
[PROOFSTEP]
classical exact
  RelIso.ofSurjective
    (RelEmbedding.orderEmbeddingOfLTEmbedding
      (RelEmbedding.natLT (Nat.Subtype.ofNat s) fun n => Nat.Subtype.lt_succ_self _))
    Nat.Subtype.ofNat_surjective
[GOAL]
α : Type u_1
s : Set ℕ
inst✝ : Infinite ↑s
⊢ ℕ ≃o ↑s
[PROOFSTEP]
exact
  RelIso.ofSurjective
    (RelEmbedding.orderEmbeddingOfLTEmbedding
      (RelEmbedding.natLT (Nat.Subtype.ofNat s) fun n => Nat.Subtype.lt_succ_self _))
    Nat.Subtype.ofNat_surjective
[GOAL]
α : Type u_1
s : Set ℕ
inst✝ : Infinite ↑s
dP : DecidablePred fun x => x ∈ s
n : ℕ
⊢ ↑(orderIsoOfNat s) n = ofNat s n
[PROOFSTEP]
simp [orderIsoOfNat]
[GOAL]
α : Type u_1
s : Set ℕ
inst✝ : Infinite ↑s
dP : DecidablePred fun x => x ∈ s
n : ℕ
⊢ ofNat s n = ofNat s n
[PROOFSTEP]
congr!
[GOAL]
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
[PROOFSTEP]
classical
have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
  simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
    Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
cases this
exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
  ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]
[GOAL]
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
[PROOFSTEP]
have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
  simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
    Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
[GOAL]
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ Infinite ↑(e ⁻¹' s) ∨ Infinite ↑(e ⁻¹' t)
[PROOFSTEP]
simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
  Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
[GOAL]
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
this : Infinite ↑(e ⁻¹' s) ∨ Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
[PROOFSTEP]
cases this
[GOAL]
case inl
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' s)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
case inr
α : Type u_1
s✝ : Set ℕ
inst✝ : Infinite ↑s✝
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h✝ : Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (↑g n) ∈ s) ∨ ∀ (n : ℕ), e (↑g n) ∈ t
[PROOFSTEP]
exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
  ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
classical
let bad : Set ℕ := {m | ∀ n, m < n → ¬r (f m) (f n)}
by_cases hbad : Infinite bad
· haveI := hbad
  refine' ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => _⟩
  have h := @Set.mem_range_self _ _ (↑(Nat.orderEmbeddingOfSet bad)) m
  rw [Nat.orderEmbeddingOfSet_range bad] at h
  exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)
· rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad
  obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → ¬n ∈ bad :=
    by
    by_cases he : hbad.toFinset.Nonempty
    ·
      refine'
        ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
          Nat.not_succ_le_self _ (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
    · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
  have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) :=
    by
    intro n
    have h := hm _ (le_add_of_nonneg_left n.zero_le)
    simp only [exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h
    obtain ⟨n', hn1, hn2⟩ := h
    obtain ⟨x, hpos, rfl⟩ := exists_pos_add_of_lt hn1
    refine' ⟨n + x, add_lt_add_left hpos n, _⟩
    rw [add_assoc, add_comm x m, ← add_assoc]
    exact hn2
  let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
  exact
    ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
          Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
      Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
let bad : Set ℕ := {m | ∀ n, m < n → ¬r (f m) (f n)}
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
by_cases hbad : Infinite bad
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
haveI := hbad
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad this : Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
refine' ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => _⟩
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad this : Infinite ↑bad
m n : ℕ
mn : m < n
⊢ ¬r (f (↑(Nat.orderEmbeddingOfSet bad) m)) (f (↑(Nat.orderEmbeddingOfSet bad) n))
[PROOFSTEP]
have h := @Set.mem_range_self _ _ (↑(Nat.orderEmbeddingOfSet bad)) m
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad this : Infinite ↑bad
m n : ℕ
mn : m < n
h : ↑(Nat.orderEmbeddingOfSet bad) m ∈ Set.range ↑(Nat.orderEmbeddingOfSet bad)
⊢ ¬r (f (↑(Nat.orderEmbeddingOfSet bad) m)) (f (↑(Nat.orderEmbeddingOfSet bad) n))
[PROOFSTEP]
rw [Nat.orderEmbeddingOfSet_range bad] at h
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad this : Infinite ↑bad
m n : ℕ
mn : m < n
h : ↑(Nat.orderEmbeddingOfSet bad) m ∈ bad
⊢ ¬r (f (↑(Nat.orderEmbeddingOfSet bad) m)) (f (↑(Nat.orderEmbeddingOfSet bad) n))
[PROOFSTEP]
exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)
[GOAL]
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : ¬Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad
[GOAL]
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → ¬n ∈ bad :=
  by
  by_cases he : hbad.toFinset.Nonempty
  ·
    refine'
      ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
        Nat.not_succ_le_self _ (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
  · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
[PROOFSTEP]
by_cases he : hbad.toFinset.Nonempty
[GOAL]
case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
he : Finset.Nonempty (Set.Finite.toFinset hbad)
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
[PROOFSTEP]
refine'
  ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
    Nat.not_succ_le_self _ (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
[GOAL]
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
he : ¬Finset.Nonempty (Set.Finite.toFinset hbad)
⊢ ∃ m, ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
[PROOFSTEP]
exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
[GOAL]
case neg.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) :=
  by
  intro n
  have h := hm _ (le_add_of_nonneg_left n.zero_le)
  simp only [exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h
  obtain ⟨n', hn1, hn2⟩ := h
  obtain ⟨x, hpos, rfl⟩ := exists_pos_add_of_lt hn1
  refine' ⟨n + x, add_lt_add_left hpos n, _⟩
  rw [add_assoc, add_comm x m, ← add_assoc]
  exact hn2
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
⊢ ∀ (n : ℕ), ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n : ℕ
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
have h := hm _ (le_add_of_nonneg_left n.zero_le)
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n : ℕ
h : ¬n + m ∈ bad
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
simp only [exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h
[GOAL]
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n : ℕ
h : ∃ x, n + m < x ∧ r (f (n + m)) (f x)
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
obtain ⟨n', hn1, hn2⟩ := h
[GOAL]
case intro.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
obtain ⟨x, hpos, rfl⟩ := exists_pos_add_of_lt hn1
[GOAL]
case intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n x : ℕ
hpos : 0 < x
hn1 : n + m < n + m + x
hn2 : r (f (n + m)) (f (n + m + x))
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
[PROOFSTEP]
refine' ⟨n + x, add_lt_add_left hpos n, _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n x : ℕ
hpos : 0 < x
hn1 : n + m < n + m + x
hn2 : r (f (n + m)) (f (n + m + x))
⊢ r (f (n + m)) (f (n + x + m))
[PROOFSTEP]
rw [add_assoc, add_comm x m, ← add_assoc]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
n x : ℕ
hpos : 0 < x
hn1 : n + m < n + m + x
hn2 : r (f (n + m)) (f (n + m + x))
⊢ r (f (n + m)) (f (n + m + x))
[PROOFSTEP]
exact hn2
[GOAL]
case neg.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
h : ∀ (n : ℕ), ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
[GOAL]
case neg.intro
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Set.Finite bad
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → ¬n ∈ bad
h : ∀ (n : ℕ), ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
g' : ℕ → ℕ := Nat.rec m fun n gn => Nat.find (_ : ∃ n', gn < n' ∧ r (f (gn + m)) (f (n' + m)))
⊢ ∃ g, (∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
exact
  ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
        Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
    Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (↑g m)) (f (↑g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f
[GOAL]
case intro.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (↑g m)) (f (↑g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
refine' ⟨g, Or.intro_left _ fun m n mn => _⟩
[GOAL]
case intro.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
m n : ℕ
mn : m < n
⊢ r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
obtain ⟨x, rfl⟩ := exists_add_of_le (Nat.succ_le_iff.2 mn)
[GOAL]
case intro.inl.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
m x : ℕ
mn : m < Nat.succ m + x
⊢ r (f (↑g m)) (f (↑g (Nat.succ m + x)))
[PROOFSTEP]
induction' x with x ih
[GOAL]
case intro.inl.intro.zero
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
m x : ℕ
mn✝ : m < Nat.succ m + x
mn : m < Nat.succ m + Nat.zero
⊢ r (f (↑g m)) (f (↑g (Nat.succ m + Nat.zero)))
[PROOFSTEP]
apply hr
[GOAL]
case intro.inl.intro.succ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
m x✝ : ℕ
mn✝ : m < Nat.succ m + x✝
x : ℕ
ih : m < Nat.succ m + x → r (f (↑g m)) (f (↑g (Nat.succ m + x)))
mn : m < Nat.succ m + Nat.succ x
⊢ r (f (↑g m)) (f (↑g (Nat.succ m + Nat.succ x)))
[PROOFSTEP]
apply IsTrans.trans _ _ _ _ (hr _)
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (↑g n)) (f (↑g (n + 1)))
m x✝ : ℕ
mn✝ : m < Nat.succ m + x✝
x : ℕ
ih : m < Nat.succ m + x → r (f (↑g m)) (f (↑g (Nat.succ m + x)))
mn : m < Nat.succ m + Nat.succ x
⊢ r (f (↑g m)) (f (↑g (Nat.add (Nat.succ m) x)))
[PROOFSTEP]
exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))
[GOAL]
case intro.inr
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (↑g m)) (f (↑g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
[PROOFSTEP]
exact ⟨g, Or.intro_right _ hnr⟩
[GOAL]
α : Type u_1
inst✝ : Preorder α
⊢ (WellFounded fun x x_1 => x > x_1) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
[PROOFSTEP]
refine' ⟨fun h a => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
[PROOFSTEP]
have hne : (Set.range a).Nonempty := ⟨a 0, by simp⟩
[GOAL]
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
⊢ ↑a 0 ∈ Set.range ↑a
[PROOFSTEP]
simp
[GOAL]
case refine'_1
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
hne : Set.Nonempty (Set.range ↑a)
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
[PROOFSTEP]
obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.has_min _ hne
[GOAL]
case refine'_1.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
hne : Set.Nonempty (Set.range ↑a)
n : ℕ
H : ∀ (x : α), x ∈ Set.range ↑a → ¬x > ↑a n
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
[PROOFSTEP]
exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩
[GOAL]
case refine'_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
refine' RelEmbedding.wellFounded_iff_no_descending_seq.2 ⟨fun a => _⟩
[GOAL]
case refine'_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ False
[PROOFSTEP]
obtain ⟨n, hn⟩ := h (a.swap : ((· < ·) : ℕ → ℕ → Prop) →r ((· < ·) : α → α → Prop)).toOrderHom
[GOAL]
case refine'_2.intro
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      ¬↑(RelHom.toOrderHom (RelEmbedding.toRelHom (RelEmbedding.swap a))) n <
          ↑(RelHom.toOrderHom (RelEmbedding.toRelHom (RelEmbedding.swap a))) m
⊢ False
[PROOFSTEP]
exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
⊢ (∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ↑a n = ↑a m
[PROOFSTEP]
congr! 4
[GOAL]
case a.h.h.e'_2.h.h.a
α : Type u_1
inst✝ : PartialOrder α
a✝¹ : ℕ →o α
x✝ a✝ : ℕ
⊢ x✝ ≤ a✝ → ¬↑a✝¹ x✝ < ↑a✝¹ a✝ ↔ x✝ ≤ a✝ → ↑a✝¹ x✝ = ↑a✝¹ a✝
[PROOFSTEP]
rename_i a n m
[GOAL]
case a.h.h.e'_2.h.h.a
α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
⊢ n ≤ m → ¬↑a n < ↑a m ↔ n ≤ m → ↑a n = ↑a m
[PROOFSTEP]
simp (config := { contextual := true }) [lt_iff_le_and_ne, fun h => a.mono h]
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
⊢ iSup ↑a = monotonicSequenceLimit a
[PROOFSTEP]
refine' (iSup_le fun m => _).antisymm (le_iSup a _)
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
⊢ ↑a m ≤ monotonicSequenceLimit a
[PROOFSTEP]
cases' le_or_lt m (monotonicSequenceLimitIndex a) with hm hm
[GOAL]
case inl
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : m ≤ monotonicSequenceLimitIndex a
⊢ ↑a m ≤ monotonicSequenceLimit a
[PROOFSTEP]
exact a.monotone hm
[GOAL]
case inr
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ ↑a m ≤ monotonicSequenceLimit a
[PROOFSTEP]
cases' WellFounded.monotone_chain_condition'.1 h a with n hn
[GOAL]
case inr.intro
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
⊢ ↑a m ≤ monotonicSequenceLimit a
[PROOFSTEP]
have : n ∈ {n | ∀ m, n ≤ m → a n = a m} := fun k hk => (a.mono hk).eq_of_not_lt (hn k hk)
[GOAL]
case inr.intro
α : Type u_1
inst✝ : CompleteLattice α
h : WellFounded fun x x_1 => x > x_1
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬↑a n < ↑a m
this : n ∈ {n | ∀ (m : ℕ), n ≤ m → ↑a n = ↑a m}
⊢ ↑a m ≤ monotonicSequenceLimit a
[PROOFSTEP]
exact (Nat.sInf_mem ⟨n, this⟩ m hm.le).ge