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

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

case node.h_3
α : Type u_1
p : α → Prop
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, All p l✝ → (∀ {x : α}, x ∈ lb → p x) → x ∈ lowerBound? cut l✝ lb → p x
ihr : ∀ {lb : Option α}, All p r✝ → (∀ {x : α}, x ∈ lb → p x) → x ∈ lowerBound? cut r✝ lb → p x
lb : Option α
hp : All p (node c✝ l✝ v✝ r✝)
H : ∀ {x : α}, x ∈ lb → p x
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → p x
case node
α : Type u_1
p : α → Prop
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, All p l✝ → (∀ {x : α}, x ∈ lb → p x) → x ∈ lowerBound? cut l✝ lb → p x
ihr : ∀ {lb : Option α}, All p r✝ → (∀ {x : α}, x ∈ lb → p x) → x ∈ lowerBound? cut r✝ lb → p x
lb : Option α
hp : All p (node c✝ l✝ v✝ r✝)
H : ∀ {x : α}, x ∈ lb → p x
⊢ (match cut v✝ with
      | Ordering.lt => lowerBound? cut l✝ lb
      | Ordering.gt => lowerBound? cut r✝ (some v✝)
      | Ordering.eq => some v✝) =
      some x →
    p x
split
no goals
case node.h_1
α : Type u_1
p : α → Prop
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, All p l✝ → (∀ {x : α}, x ∈ lb → p x) → x ∈ lowerBound? cut l✝ lb → p x
ihr : ∀ {lb : Option α}, All p r✝ → (∀ {x : α}, x ∈ lb → p x) → x ∈ lowerBound? cut r✝ lb → p x
lb : Option α
hp : All p (node c✝ l✝ v✝ r✝)
H : ∀ {x : α}, x ∈ lb → p x
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ lowerBound? cut l✝ lb = some x → p x
exact ihl hp.2.1 H
no goals
case node.h_2
α : Type u_1
p : α → Prop
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, All p l✝ → (∀ {x : α}, x ∈ lb → p x) → x ∈ lowerBound? cut l✝ lb → p x
ihr : ∀ {lb : Option α}, All p r✝ → (∀ {x : α}, x ∈ lb → p x) → x ∈ lowerBound? cut r✝ lb → p x
lb : Option α
hp : All p (node c✝ l✝ v✝ r✝)
H : ∀ {x : α}, x ∈ lb → p x
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ lowerBound? cut r✝ (some v✝) = some x → p x
exact ihr hp.2.2 fun | rfl => hp.1
no goals
case node.h_3
α : Type u_1
p : α → Prop
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : ∀ {lb : Option α}, All p l✝ → (∀ {x : α}, x ∈ lb → p x) → x ∈ lowerBound? cut l✝ lb → p x
ihr : ∀ {lb : Option α}, All p r✝ → (∀ {x : α}, x ∈ lb → p x) → x ∈ lowerBound? cut r✝ lb → p x
lb : Option α
hp : All p (node c✝ l✝ v✝ r✝)
H : ∀ {x : α}, x ∈ lb → p x
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → p x
exact fun | rfl => hp.1