no goals
case nil
α : Type u_1
cut : α → Ordering
x : α
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
⊢ x ∈ lowerBound? cut nil lb → cut x ≠ Ordering.lt
exact H
case node
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut l✝ lb → cut x ≠ Ordering.lt
ihr : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut r✝ lb → cut x ≠ Ordering.lt
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
⊢ (match cut v✝ with
      | Ordering.lt => lowerBound? cut l✝ lb
      | Ordering.gt => lowerBound? cut r✝ (some v✝)
      | Ordering.eq => some v✝) =
      some x →
    ¬cut x = Ordering.lt
case node
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut l✝ lb → cut x ≠ Ordering.lt
ihr : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut r✝ lb → cut x ≠ Ordering.lt
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
⊢ x ∈ lowerBound? cut (node c✝ l✝ v✝ r✝) lb → cut x ≠ Ordering.lt
simp [lowerBound?]
case node.h_1
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut l✝ lb → cut x ≠ Ordering.lt
ihr : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut r✝ lb → cut x ≠ Ordering.lt
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ lowerBound? cut l✝ lb = some x → ¬cut x = Ordering.lt

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

case node.h_3
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut l✝ lb → cut x ≠ Ordering.lt
ihr : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut r✝ lb → cut x ≠ Ordering.lt
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → ¬cut x = Ordering.lt
case node
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut l✝ lb → cut x ≠ Ordering.lt
ihr : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut r✝ lb → cut x ≠ Ordering.lt
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
⊢ (match cut v✝ with
      | Ordering.lt => lowerBound? cut l✝ lb
      | Ordering.gt => lowerBound? cut r✝ (some v✝)
      | Ordering.eq => some v✝) =
      some x →
    ¬cut x = Ordering.lt
split
no goals
case node.h_1
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut l✝ lb → cut x ≠ Ordering.lt
ihr : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut r✝ lb → cut x ≠ Ordering.lt
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ lowerBound? cut l✝ lb = some x → ¬cut x = Ordering.lt
exact ihl H
no goals
case node.h_2
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut l✝ lb → cut x ≠ Ordering.lt
ihr : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut r✝ lb → cut x ≠ Ordering.lt
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ lowerBound? cut r✝ (some v✝) = some x → ¬cut x = Ordering.lt
next hv => exact ihr fun | rfl, e => nomatch hv.symm.trans e
no goals
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut l✝ lb → cut x ≠ Ordering.lt
ihr : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut r✝ lb → cut x ≠ Ordering.lt
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
x✝ : Ordering
hv : cut v✝ = Ordering.gt
⊢ lowerBound? cut r✝ (some v✝) = some x → ¬cut x = Ordering.lt
exact ihr fun | rfl, e => nomatch hv.symm.trans e
no goals
case node.h_3
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut l✝ lb → cut x ≠ Ordering.lt
ihr : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut r✝ lb → cut x ≠ Ordering.lt
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → ¬cut x = Ordering.lt
next hv => intro | rfl, e => cases hv.symm.trans e
no goals
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut l✝ lb → cut x ≠ Ordering.lt
ihr : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → x ∈ lowerBound? cut r✝ lb → cut x ≠ Ordering.lt
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
x✝ : Ordering
hv : cut v✝ = Ordering.eq
⊢ some v✝ = some x → ¬cut x = Ordering.lt
intro | rfl, e => cases hv.symm.trans e
no goals
α : Type u_1
cut : α → Ordering
x : α
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
lb : Option α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
x✝² : Ordering
hv : cut v✝ = Ordering.eq
x✝¹ : some v✝ = some x
x✝ : cut x = Ordering.lt
e : cut v✝ = Ordering.lt
ihl : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → v✝ ∈ lowerBound? cut l✝ lb → cut v✝ ≠ Ordering.lt
ihr : ∀ {lb : Option α}, (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → v✝ ∈ lowerBound? cut r✝ lb → cut v✝ ≠ Ordering.lt
⊢ False
cases hv.symm.trans e