case refine_1
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cmp x y = Ordering.lt
⊢ cut y = Ordering.lt

case refine_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cut y = Ordering.lt
⊢ cmp y x = Ordering.gt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
⊢ cmp x y = Ordering.lt ↔ cut y = Ordering.lt
refine ⟨fun h => ?_, fun h => OrientedCmp.cmp_eq_gt.1 ?_⟩
case refine_1.lt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cmp x y = Ordering.lt
e : cut x = Ordering.lt
⊢ cut y = Ordering.lt

case refine_1.eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cmp x y = Ordering.lt
e : cut x = Ordering.eq
⊢ cut y = Ordering.lt

case refine_1.gt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cmp x y = Ordering.lt
e : cut x = Ordering.gt
⊢ cut y = Ordering.lt
case refine_1
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cmp x y = Ordering.lt
⊢ cut y = Ordering.lt
cases e : cut x
no goals
case refine_1.lt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cmp x y = Ordering.lt
e : cut x = Ordering.lt
⊢ cut y = Ordering.lt
cases lowerBound?_le H e
no goals
case refine_1.eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cmp x y = Ordering.lt
e : cut x = Ordering.eq
⊢ cut y = Ordering.lt
exact IsStrictCut.exact e |>.symm.trans h
no goals
case refine_1.gt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cmp x y = Ordering.lt
e : cut x = Ordering.gt
⊢ cut y = Ordering.lt
exact ht.lowerBound?_least H hy h e
case refine_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cut y = Ordering.lt
h' : ¬cmp y x = Ordering.gt
⊢ False
case refine_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cut y = Ordering.lt
⊢ cmp y x = Ordering.gt
by_contra h'
no goals
case refine_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : x ∈ lowerBound? cut t none
hy : y ∈ t
h : cut y = Ordering.lt
h' : ¬cmp y x = Ordering.gt
⊢ False
exact lowerBound?_le H <| IsCut.le_lt_trans (cmp := cmp) (cut := cut) h' h