-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem upperBound?_ge' {t : RBNode α} (H : ∀ {x}, x ∈ ub → cut x ≠ .gt) :
    t.upperBound? cut ub = some x → cut x ≠ .gt

Proof state:
case node
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some x → cut x ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some x → cut x ≠ Ordering.gt
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
⊢ (match cut v✝ with
      | Ordering.lt => upperBound? cut l✝ (some v✝)
      | Ordering.gt => upperBound? cut r✝ ub
      | Ordering.eq => some v✝) =
      some x →
    ¬cut x = Ordering.gt

Tactic:
split

Result:
case node.h_1
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some x → cut x ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some x → cut x ≠ Ordering.gt
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ upperBound? cut l✝ (some v✝) = some x → ¬cut x = Ordering.gt

case node.h_2
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some x → cut x ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some x → cut x ≠ Ordering.gt
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ upperBound? cut r✝ ub = some x → ¬cut x = Ordering.gt

case node.h_3
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some x → cut x ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some x → cut x ≠ Ordering.gt
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → ¬cut x = Ordering.gt

Proof state:
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some x → cut x ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some x → cut x ≠ Ordering.gt
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
x✝ : Ordering
hv : cut v✝ = Ordering.eq
⊢ some v✝ = some x → ¬cut x = Ordering.gt

Tactic:
intro | rfl, e => cases hv.symm.trans e

Result:
no goals

Proof state:
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some x → cut x ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some x → cut x ≠ Ordering.gt
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
x✝ : Ordering
hv : cut v✝ = Ordering.lt
⊢ upperBound? cut l✝ (some v✝) = some x → ¬cut x = Ordering.gt

Tactic:
exact ihl fun | rfl, e => nomatch hv.symm.trans e

Result:
no goals

Proof state:
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
x✝² : Ordering
hv : cut v✝ = Ordering.eq
x✝¹ : some v✝ = some x
x✝ : cut x = Ordering.gt
e : cut v✝ = Ordering.gt
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some v✝ → cut v✝ ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some v✝ → cut v✝ ≠ Ordering.gt
⊢ False

Tactic:
cases hv.symm.trans e

Result:
no goals

Proof state:
case node.h_3
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some x → cut x ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some x → cut x ≠ Ordering.gt
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → ¬cut x = Ordering.gt

Tactic:
next hv => intro | rfl, e => cases hv.symm.trans e

Result:
no goals

Proof state:
case node.h_2
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some x → cut x ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some x → cut x ≠ Ordering.gt
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ upperBound? cut r✝ ub = some x → ¬cut x = Ordering.gt

Tactic:
exact ihr H

Result:
no goals

Proof state:
case nil
α : Type u_1
cut : α → Ordering
x : α
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
⊢ upperBound? cut nil ub = some x → cut x ≠ Ordering.gt

Tactic:
exact H

Result:
no goals

Proof state:
case node
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some x → cut x ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some x → cut x ≠ Ordering.gt
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
⊢ upperBound? cut (node c✝ l✝ v✝ r✝) ub = some x → cut x ≠ Ordering.gt

Tactic:
simp [upperBound?]

Result:
case node
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some x → cut x ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some x → cut x ≠ Ordering.gt
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
⊢ (match cut v✝ with
      | Ordering.lt => upperBound? cut l✝ (some v✝)
      | Ordering.gt => upperBound? cut r✝ ub
      | Ordering.eq => some v✝) =
      some x →
    ¬cut x = Ordering.gt

Proof state:
case node.h_1
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut l✝ ub = some x → cut x ≠ Ordering.gt
ihr :
  ∀ {ub : Option α}, (∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt) → upperBound? cut r✝ ub = some x → cut x ≠ Ordering.gt
ub : Option α
H : ∀ {x : α}, x ∈ ub → cut x ≠ Ordering.gt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ upperBound? cut l✝ (some v✝) = some x → ¬cut x = Ordering.gt

Tactic:
next hv => exact ihl fun | rfl, e => nomatch hv.symm.trans e

Result:
no goals