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

Proof state:
case node
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α},
    Ordered cmp l✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) l✝) →
        upperBound? cut l✝ ub = some x → y ∈ l✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ihr :
  ∀ {ub : Option α},
    Ordered cmp r✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) r✝) →
        upperBound? cut r✝ ub = some x → y ∈ r✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ub : Option α
h : Ordered cmp (node c✝ l✝ v✝ r✝)
hub : ∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) (node c✝ l✝ v✝ r✝)
⊢ (match cut v✝ with
      | Ordering.lt => upperBound? cut l✝ (some v✝)
      | Ordering.gt => upperBound? cut r✝ ub
      | Ordering.eq => some v✝) =
      some x →
    y = v✝ ∨ y ∈ l✝ ∨ y ∈ r✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt

Tactic:
split <;> rename_i hv <;> rintro h₁ (rfl | hy' | hy') hx h₂

Result:
case node.h_1.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ r✝ : RBNode α
ihl :
  ∀ {ub : Option α},
    Ordered cmp l✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) l✝) →
        upperBound? cut l✝ ub = some x → y ∈ l✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ihr :
  ∀ {ub : Option α},
    Ordered cmp r✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) r✝) →
        upperBound? cut r✝ ub = some x → y ∈ r✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ub : Option α
x✝ : Ordering
h : Ordered cmp (node c✝ l✝ y r✝)
hub : ∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) (node c✝ l✝ y r✝)
hv : cut y = Ordering.lt
h₁ : upperBound? cut l✝ (some y) = some x
hx : cut x = Ordering.lt
h₂ : cmp y x = Ordering.lt
⊢ cut y = Ordering.gt

case node.h_1.inr.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α},
    Ordered cmp l✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) l✝) →
        upperBound? cut l✝ ub = some x → y ∈ l✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ihr :
  ∀ {ub : Option α},
    Ordered cmp r✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) r✝) →
        upperBound? cut r✝ ub = some x → y ∈ r✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ub : Option α
h : Ordered cmp (node c✝ l✝ v✝ r✝)
hub : ∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) (node c✝ l✝ v✝ r✝)
x✝ : Ordering
hv : cut v✝ = Ordering.lt
h₁ : upperBound? cut l✝ (some v✝) = some x
hy' : y ∈ l✝
hx : cut x = Ordering.lt
h₂ : cmp y x = Ordering.lt
⊢ cut y = Ordering.gt

case node.h_1.inr.inr
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α},
    Ordered cmp l✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) l✝) →
        upperBound? cut l✝ ub = some x → y ∈ l✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ihr :
  ∀ {ub : Option α},
    Ordered cmp r✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) r✝) →
        upperBound? cut r✝ ub = some x → y ∈ r✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ub : Option α
h : Ordered cmp (node c✝ l✝ v✝ r✝)
hub : ∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) (node c✝ l✝ v✝ r✝)
x✝ : Ordering
hv : cut v✝ = Ordering.lt
h₁ : upperBound? cut l✝ (some v✝) = some x
hy' : y ∈ r✝
hx : cut x = Ordering.lt
h₂ : cmp y x = Ordering.lt
⊢ cut y = Ordering.gt

case node.h_2.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ r✝ : RBNode α
ihl :
  ∀ {ub : Option α},
    Ordered cmp l✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) l✝) →
        upperBound? cut l✝ ub = some x → y ∈ l✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ihr :
  ∀ {ub : Option α},
    Ordered cmp r✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) r✝) →
        upperBound? cut r✝ ub = some x → y ∈ r✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ub : Option α
x✝ : Ordering
h₁ : upperBound? cut r✝ ub = some x
h : Ordered cmp (node c✝ l✝ y r✝)
hub : ∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) (node c✝ l✝ y r✝)
hv : cut y = Ordering.gt
hx : cut x = Ordering.lt
h₂ : cmp y x = Ordering.lt
⊢ cut y = Ordering.gt

case node.h_2.inr.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α},
    Ordered cmp l✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) l✝) →
        upperBound? cut l✝ ub = some x → y ∈ l✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ihr :
  ∀ {ub : Option α},
    Ordered cmp r✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) r✝) →
        upperBound? cut r✝ ub = some x → y ∈ r✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ub : Option α
h : Ordered cmp (node c✝ l✝ v✝ r✝)
hub : ∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) (node c✝ l✝ v✝ r✝)
x✝ : Ordering
hv : cut v✝ = Ordering.gt
h₁ : upperBound? cut r✝ ub = some x
hy' : y ∈ l✝
hx : cut x = Ordering.lt
h₂ : cmp y x = Ordering.lt
⊢ cut y = Ordering.gt

case node.h_2.inr.inr
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α},
    Ordered cmp l✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) l✝) →
        upperBound? cut l✝ ub = some x → y ∈ l✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ihr :
  ∀ {ub : Option α},
    Ordered cmp r✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) r✝) →
        upperBound? cut r✝ ub = some x → y ∈ r✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ub : Option α
h : Ordered cmp (node c✝ l✝ v✝ r✝)
hub : ∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) (node c✝ l✝ v✝ r✝)
x✝ : Ordering
hv : cut v✝ = Ordering.gt
h₁ : upperBound? cut r✝ ub = some x
hy' : y ∈ r✝
hx : cut x = Ordering.lt
h₂ : cmp y x = Ordering.lt
⊢ cut y = Ordering.gt

case node.h_3.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ r✝ : RBNode α
ihl :
  ∀ {ub : Option α},
    Ordered cmp l✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) l✝) →
        upperBound? cut l✝ ub = some x → y ∈ l✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ihr :
  ∀ {ub : Option α},
    Ordered cmp r✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) r✝) →
        upperBound? cut r✝ ub = some x → y ∈ r✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ub : Option α
x✝ : Ordering
h : Ordered cmp (node c✝ l✝ y r✝)
hub : ∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) (node c✝ l✝ y r✝)
hv : cut y = Ordering.eq
h₁ : some y = some x
hx : cut x = Ordering.lt
h₂ : cmp y x = Ordering.lt
⊢ cut y = Ordering.gt

case node.h_3.inr.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α},
    Ordered cmp l✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) l✝) →
        upperBound? cut l✝ ub = some x → y ∈ l✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ihr :
  ∀ {ub : Option α},
    Ordered cmp r✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) r✝) →
        upperBound? cut r✝ ub = some x → y ∈ r✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ub : Option α
h : Ordered cmp (node c✝ l✝ v✝ r✝)
hub : ∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) (node c✝ l✝ v✝ r✝)
x✝ : Ordering
hv : cut v✝ = Ordering.eq
h₁ : some v✝ = some x
hy' : y ∈ l✝
hx : cut x = Ordering.lt
h₂ : cmp y x = Ordering.lt
⊢ cut y = Ordering.gt

case node.h_3.inr.inr
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α},
    Ordered cmp l✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) l✝) →
        upperBound? cut l✝ ub = some x → y ∈ l✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ihr :
  ∀ {ub : Option α},
    Ordered cmp r✝ →
      (∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) r✝) →
        upperBound? cut r✝ ub = some x → y ∈ r✝ → cut x = Ordering.lt → cmp y x = Ordering.lt → cut y = Ordering.gt
ub : Option α
h : Ordered cmp (node c✝ l✝ v✝ r✝)
hub : ∀ {x : α}, ub = some x → All (fun x_1 => cmpLT cmp x_1 x) (node c✝ l✝ v✝ r✝)
x✝ : Ordering
hv : cut v✝ = Ordering.eq
h₁ : some v✝ = some x
hy' : y ∈ r✝
hx : cut x = Ordering.lt
h₂ : cmp y x = Ordering.lt
⊢ cut y = Ordering.gt