-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem upperBound?_eq_find? {t : RBNode α} {cut} (ub) (H : t.find? cut = some x) :
    t.upperBound? cut ub = some x

Proof state:
case node.h_1
α : Type u_1
x : α
cut : α → Ordering
c : RBColor
a : RBNode α
y : α
b : RBNode α
iha : ∀ (ub : Option α), find? cut a = some x → upperBound? cut a ub = some x
ihb : ∀ (ub : Option α), find? cut b = some x → upperBound? cut b ub = some x
ub : Option α
x✝ : Ordering
heq✝ : cut y = Ordering.lt
H : find? cut a = some x
⊢ upperBound? cut a (some y) = some x

Tactic:
apply iha _ H

Result:
no goals

Proof state:
case node
α : Type u_1
x : α
cut : α → Ordering
c : RBColor
a : RBNode α
y : α
b : RBNode α
iha : ∀ (ub : Option α), find? cut a = some x → upperBound? cut a ub = some x
ihb : ∀ (ub : Option α), find? cut b = some x → upperBound? cut b ub = some x
ub : Option α
H :
  (match cut y with
    | Ordering.lt => find? cut a
    | Ordering.gt => find? cut b
    | Ordering.eq => some y) =
    some x
⊢ (match cut y with
    | Ordering.lt => upperBound? cut a (some y)
    | Ordering.gt => upperBound? cut b ub
    | Ordering.eq => some y) =
    some x

Tactic:
split at H

Result:
case node.h_1
α : Type u_1
x : α
cut : α → Ordering
c : RBColor
a : RBNode α
y : α
b : RBNode α
iha : ∀ (ub : Option α), find? cut a = some x → upperBound? cut a ub = some x
ihb : ∀ (ub : Option α), find? cut b = some x → upperBound? cut b ub = some x
ub : Option α
x✝ : Ordering
heq✝ : cut y = Ordering.lt
H : find? cut a = some x
⊢ upperBound? cut a (some y) = some x

case node.h_2
α : Type u_1
x : α
cut : α → Ordering
c : RBColor
a : RBNode α
y : α
b : RBNode α
iha : ∀ (ub : Option α), find? cut a = some x → upperBound? cut a ub = some x
ihb : ∀ (ub : Option α), find? cut b = some x → upperBound? cut b ub = some x
ub : Option α
x✝ : Ordering
heq✝ : cut y = Ordering.gt
H : find? cut b = some x
⊢ upperBound? cut b ub = some x

case node.h_3
α : Type u_1
x : α
cut : α → Ordering
c : RBColor
a : RBNode α
y : α
b : RBNode α
iha : ∀ (ub : Option α), find? cut a = some x → upperBound? cut a ub = some x
ihb : ∀ (ub : Option α), find? cut b = some x → upperBound? cut b ub = some x
ub : Option α
x✝ : Ordering
heq✝ : cut y = Ordering.eq
H : some y = some x
⊢ some y = some x

Proof state:
case node.h_2
α : Type u_1
x : α
cut : α → Ordering
c : RBColor
a : RBNode α
y : α
b : RBNode α
iha : ∀ (ub : Option α), find? cut a = some x → upperBound? cut a ub = some x
ihb : ∀ (ub : Option α), find? cut b = some x → upperBound? cut b ub = some x
ub : Option α
x✝ : Ordering
heq✝ : cut y = Ordering.gt
H : find? cut b = some x
⊢ upperBound? cut b ub = some x

Tactic:
apply ihb _ H

Result:
no goals

Proof state:
case node
α : Type u_1
x : α
cut : α → Ordering
c : RBColor
a : RBNode α
y : α
b : RBNode α
iha : ∀ (ub : Option α), find? cut a = some x → upperBound? cut a ub = some x
ihb : ∀ (ub : Option α), find? cut b = some x → upperBound? cut b ub = some x
ub : Option α
H :
  (match cut y with
    | Ordering.lt => find? cut a
    | Ordering.gt => find? cut b
    | Ordering.eq => some y) =
    some x
⊢ upperBound? cut (node c a y b) ub = some x

Tactic:
simp [upperBound?]

Result:
case node
α : Type u_1
x : α
cut : α → Ordering
c : RBColor
a : RBNode α
y : α
b : RBNode α
iha : ∀ (ub : Option α), find? cut a = some x → upperBound? cut a ub = some x
ihb : ∀ (ub : Option α), find? cut b = some x → upperBound? cut b ub = some x
ub : Option α
H :
  (match cut y with
    | Ordering.lt => find? cut a
    | Ordering.gt => find? cut b
    | Ordering.eq => some y) =
    some x
⊢ (match cut y with
    | Ordering.lt => upperBound? cut a (some y)
    | Ordering.gt => upperBound? cut b ub
    | Ordering.eq => some y) =
    some x

Proof state:
case node.h_3
α : Type u_1
x : α
cut : α → Ordering
c : RBColor
a : RBNode α
y : α
b : RBNode α
iha : ∀ (ub : Option α), find? cut a = some x → upperBound? cut a ub = some x
ihb : ∀ (ub : Option α), find? cut b = some x → upperBound? cut b ub = some x
ub : Option α
x✝ : Ordering
heq✝ : cut y = Ordering.eq
H : some y = some x
⊢ some y = some x

Tactic:
exact H

Result:
no goals