α : Type u_1
cut : α → Ordering
y : α
t : RBNode α
⊢ ∃ x, lowerBound? cut t (some y) = some x
α : Type u_1
cut : α → Ordering
y : α
t : RBNode α
⊢ ∃ x, x ∈ lowerBound? cut t (some y)
simp
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : ∀ {y : α}, ∃ x, lowerBound? cut l✝ (some y) = some x
r_ih✝ : ∀ {y : α}, ∃ x, lowerBound? cut r✝ (some y) = some x
y : α
⊢ ∃ x,
    (match cut v✝ with
      | Ordering.lt => lowerBound? cut l✝ (some y)
      | Ordering.gt => lowerBound? cut r✝ (some v✝)
      | Ordering.eq => some v✝) =
      some x
α : Type u_1
cut : α → Ordering
y : α
t : RBNode α
⊢ ∃ x, lowerBound? cut t (some y) = some x
induction t generalizing y <;> simp [lowerBound?]
no goals
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : ∀ {y : α}, ∃ x, lowerBound? cut l✝ (some y) = some x
r_ih✝ : ∀ {y : α}, ∃ x, lowerBound? cut r✝ (some y) = some x
y : α
⊢ ∃ x,
    (match cut v✝ with
      | Ordering.lt => lowerBound? cut l✝ (some y)
      | Ordering.gt => lowerBound? cut r✝ (some v✝)
      | Ordering.eq => some v✝) =
      some x
split <;> simp [*]