α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
⊢ ∃ x, x ∈ lowerBound? cut t none ∧ cut x = Ordering.eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
⊢ MemP cut t ↔ ∃ x, x ∈ lowerBound? cut t none ∧ cut x = Ordering.eq
refine memP_def.trans ⟨fun ⟨y, hy, ey⟩ => ?_, fun ⟨x, hx, e⟩ => ⟨_, lowerBound?_mem hx, e⟩⟩
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
⊢ ∃ x, x ∈ lowerBound? cut t none ∧ cut x = Ordering.eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
⊢ ∃ x, x ∈ lowerBound? cut t none ∧ cut x = Ordering.eq
have ⟨x, hx⟩ := ht.lowerBound?_exists.2 ⟨_, hy, fun h => nomatch ey.symm.trans h⟩
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
⊢ cut x = Ordering.eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
⊢ ∃ x, x ∈ lowerBound? cut t none ∧ cut x = Ordering.eq
refine ⟨x, hx, ?_⟩
case lt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.lt
⊢ Ordering.lt = Ordering.eq

case eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.eq
⊢ Ordering.eq = Ordering.eq

case gt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.gt
⊢ Ordering.gt = Ordering.eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
⊢ cut x = Ordering.eq
cases ex : cut x
no goals
case lt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.lt
⊢ Ordering.lt = Ordering.eq
cases lowerBound?_le hx ex
no goals
case eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.eq
⊢ Ordering.eq = Ordering.eq
rfl
case gt.lt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.gt
e : cmp x y = Ordering.lt
⊢ Ordering.gt = Ordering.eq

case gt.eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.gt
e : cmp x y = Ordering.eq
⊢ Ordering.gt = Ordering.eq

case gt.gt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.gt
e : cmp x y = Ordering.gt
⊢ Ordering.gt = Ordering.eq
case gt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.gt
⊢ Ordering.gt = Ordering.eq
cases e : cmp x y
no goals
case gt.lt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.gt
e : cmp x y = Ordering.lt
⊢ Ordering.gt = Ordering.eq
cases ey.symm.trans <| ht.lowerBound?_least hx hy e ex
no goals
case gt.eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.gt
e : cmp x y = Ordering.eq
⊢ Ordering.gt = Ordering.eq
cases ey.symm.trans <| IsCut.congr e |>.symm.trans ex
no goals
case gt.gt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : x ∈ lowerBound? cut t none
ex : cut x = Ordering.gt
e : cmp x y = Ordering.gt
⊢ Ordering.gt = Ordering.eq
cases ey.symm.trans <| IsCut.gt_trans (OrientedCmp.cmp_eq_gt.1 e) ex