-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.lowerBound?_lt [@TransCmp α cmp] [IsStrictCut cmp cut] (ht : Ordered cmp t)
    (H : t.lowerBound? cut = some x) (hy : y ∈ t) : cmp x y = .lt ↔ cut y = .lt

Proof state:
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 : lowerBound? cut t = some x
hy : y ∈ t
h : cmp x y = Ordering.lt
e : cut x = Ordering.eq
⊢ cut y = Ordering.lt

Tactic:
exact IsStrictCut.exact e |>.symm.trans h

Result:
no goals

Proof state:
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 : lowerBound? cut t = some x
hy : y ∈ t
h : cut y = Ordering.lt
h' : ¬cmp y x = Ordering.gt
⊢ False

Tactic:
exact lowerBound?_le H <| IsCut.le_lt_trans (cmp := cmp) (cut := cut) h' h

Result:
no goals

Proof state:
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 : lowerBound? cut t = some x
hy : y ∈ t
h : cut y = Ordering.lt
⊢ cmp y x = Ordering.gt

Tactic:
by_contra h'

Result:
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 : lowerBound? cut t = some x
hy : y ∈ t
h : cut y = Ordering.lt
h' : ¬cmp y x = Ordering.gt
⊢ False

Proof state:
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 : lowerBound? cut t = some x
hy : y ∈ t
h : cmp x y = Ordering.lt
⊢ cut y = Ordering.lt

Tactic:
cases e : cut x

Result:
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 : lowerBound? cut t = some x
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 : lowerBound? cut t = some x
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 : lowerBound? cut t = some x
hy : y ∈ t
h : cmp x y = Ordering.lt
e : cut x = Ordering.gt
⊢ cut y = Ordering.lt

Proof state:
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 : lowerBound? cut t = some x
hy : y ∈ t
h : cmp x y = Ordering.lt
e : cut x = Ordering.lt
⊢ cut y = Ordering.lt

Tactic:
cases lowerBound?_le H e

Result:
no goals

Proof state:
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 : lowerBound? cut t = some x
hy : y ∈ t
h : cmp x y = Ordering.lt
e : cut x = Ordering.gt
⊢ cut y = Ordering.lt

Tactic:
exact ht.lowerBound?_greatest H hy h e

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : lowerBound? cut t = some x
hy : y ∈ t
⊢ cmp x y = Ordering.lt ↔ cut y = Ordering.lt

Tactic:
refine ⟨fun h => ?_, fun h => OrientedCmp.cmp_eq_gt.1 ?_⟩

Result:
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 : lowerBound? cut t = some x
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 : lowerBound? cut t = some x
hy : y ∈ t
h : cut y = Ordering.lt
⊢ cmp y x = Ordering.gt