-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.lowerBound?_greatest_lb [@TransCmp α cmp] [IsCut cmp cut] (h : Ordered cmp t)
    (hlb : ∀ {x}, lb = some x → t.All (cmpLT cmp x ·)) :
    t.lowerBound? cut lb = some x → y ∈ t → cut x = .gt → cmp x y = .lt → cut y = .lt

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
lb : Option α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
hlb : ∀ {x : α}, lb = some x → All (fun x_1 => cmpLT cmp x x_1) t
h1 : upperBound? (fun x => (cut x).swap) t.reverse lb = some x
⊢ y ∈ t → (cut x).swap = Ordering.gt.swap → cmp x y = Ordering.lt → (cut y).swap = Ordering.lt.swap

Tactic:
simpa [-Ordering.swap_inj] using
  h.reverse.upperBound?_least_ub (fun h => All.reverse.2 <| (hlb h).imp .flip) h1

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
lb : Option α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
hlb : ∀ {x : α}, lb = some x → All (fun x_1 => cmpLT cmp x x_1) t
h1 : lowerBound? cut t lb = some x
h2 : y ∈ t
h3 : cut x = Ordering.gt
h4 : cmp x y = Ordering.lt
⊢ cut y = Ordering.lt

Tactic:
rw [← reverse_reverse t, lowerBound?_reverse] at h1

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
lb : Option α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
hlb : ∀ {x : α}, lb = some x → All (fun x_1 => cmpLT cmp x x_1) t
h1 : upperBound? (fun x => (cut x).swap) t.reverse lb = some x
h2 : y ∈ t
h3 : cut x = Ordering.gt
h4 : cmp x y = Ordering.lt
⊢ cut y = Ordering.lt

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
lb : Option α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
hlb : ∀ {x : α}, lb = some x → All (fun x_1 => cmpLT cmp x x_1) t
h1 : upperBound? (fun x => (cut x).swap) t.reverse lb = some x
h2 : y ∈ t
h3 : (cut x).swap = Ordering.gt.swap
h4 : cmp x y = Ordering.lt
⊢ (cut y).swap = Ordering.lt.swap

Tactic:
revert h2 h3 h4

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
lb : Option α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
hlb : ∀ {x : α}, lb = some x → All (fun x_1 => cmpLT cmp x x_1) t
h1 : upperBound? (fun x => (cut x).swap) t.reverse lb = some x
⊢ y ∈ t → (cut x).swap = Ordering.gt.swap → cmp x y = Ordering.lt → (cut y).swap = Ordering.lt.swap

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
lb : Option α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
hlb : ∀ {x : α}, lb = some x → All (fun x_1 => cmpLT cmp x x_1) t
⊢ lowerBound? cut t lb = some x → y ∈ t → cut x = Ordering.gt → cmp x y = Ordering.lt → cut y = Ordering.lt

Tactic:
intro h1 h2 h3 h4

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
lb : Option α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
hlb : ∀ {x : α}, lb = some x → All (fun x_1 => cmpLT cmp x x_1) t
h1 : lowerBound? cut t lb = some x
h2 : y ∈ t
h3 : cut x = Ordering.gt
h4 : cmp x y = Ordering.lt
⊢ cut y = Ordering.lt

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
lb : Option α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
hlb : ∀ {x : α}, lb = some x → All (fun x_1 => cmpLT cmp x x_1) t
h1 : upperBound? (fun x => (cut x).swap) t.reverse lb = some x
h2 : y ∈ t
h3 : cut x = Ordering.gt
h4 : cmp x y = Ordering.lt
⊢ cut y = Ordering.lt

Tactic:
rw [← Ordering.swap_inj] at h3 ⊢

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
lb : Option α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
hlb : ∀ {x : α}, lb = some x → All (fun x_1 => cmpLT cmp x x_1) t
h1 : upperBound? (fun x => (cut x).swap) t.reverse lb = some x
h2 : y ∈ t
h3 : (cut x).swap = Ordering.gt.swap
h4 : cmp x y = Ordering.lt
⊢ (cut y).swap = Ordering.lt.swap