α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
H : ∃ x, x ∈ t ∧ cut x ≠ Ordering.lt
⊢ ∃ x, x ∈ lowerBound? cut t none
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
⊢ (∃ x, x ∈ lowerBound? cut t none) ↔ ∃ x, x ∈ t ∧ cut x ≠ Ordering.lt
refine ⟨fun ⟨x, hx⟩ => ⟨_, lowerBound?_mem hx, lowerBound?_le hx⟩, fun H => ?_⟩
case intro.intro
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
x : α
hx : x ∈ t
e : cut x ≠ Ordering.lt
⊢ ∃ x, x ∈ lowerBound? cut t none
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp t
H : ∃ x, x ∈ t ∧ cut x ≠ Ordering.lt
⊢ ∃ x, x ∈ lowerBound? cut t none
obtain ⟨x, hx, e⟩ := H
no goals
case intro.intro.nil
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
h : Ordered cmp nil
x : α
hx : x ∈ nil
e : cut x ≠ Ordering.lt
⊢ ∃ x, x ∈ lowerBound? cut nil none
cases hx
case intro.intro.node
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.lt
⊢ ∃ x,
    (match cut v✝ with
      | Ordering.lt => lowerBound? cut l✝ none
      | Ordering.gt => lowerBound? cut r✝ (some v✝)
      | Ordering.eq => some v✝) =
      some x
case intro.intro.node
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.lt
⊢ ∃ x, x ∈ lowerBound? cut (node c✝ l✝ v✝ r✝) none
simp [lowerBound?]
case intro.intro.node.h_1
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ ∃ x, lowerBound? cut l✝ none = some x

case intro.intro.node.h_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ ∃ x, lowerBound? cut r✝ (some v✝) = some x

case intro.intro.node.h_3
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ ∃ x, some v✝ = some x
case intro.intro.node
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.lt
⊢ ∃ x,
    (match cut v✝ with
      | Ordering.lt => lowerBound? cut l✝ none
      | Ordering.gt => lowerBound? cut r✝ (some v✝)
      | Ordering.eq => some v✝) =
      some x
split
case intro.intro.node.h_1.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
x : α
e : cut x ≠ Ordering.lt
x✝ : Ordering
h : Ordered cmp (node c✝ l✝ x r✝)
heq✝ : cut x = Ordering.lt
⊢ ∃ x, lowerBound? cut l✝ none = some x

case intro.intro.node.h_1.inr.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
e : cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
hx : Any (fun x_1 => x = x_1) l✝
⊢ ∃ x, lowerBound? cut l✝ none = some x

case intro.intro.node.h_1.inr.inr
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
e : cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
hx : Any (fun x_1 => x = x_1) r✝
⊢ ∃ x, lowerBound? cut l✝ none = some x
case intro.intro.node.h_1
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ ∃ x, lowerBound? cut l✝ none = some x
rcases hx with rfl | hx | hx
no goals
case intro.intro.node.h_1.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
x : α
e : cut x ≠ Ordering.lt
x✝ : Ordering
h : Ordered cmp (node c✝ l✝ x r✝)
heq✝ : cut x = Ordering.lt
⊢ ∃ x, lowerBound? cut l✝ none = some x
contradiction
no goals
case intro.intro.node.h_1.inr.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
e : cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
hx : Any (fun x_1 => x = x_1) l✝
⊢ ∃ x, lowerBound? cut l✝ none = some x
exact ihl h.2.2.1 _ hx e
no goals
case intro.intro.node.h_1.inr.inr
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
e : cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
hx : Any (fun x_1 => x = x_1) r✝
⊢ ∃ x, lowerBound? cut l✝ none = some x
next hv => cases e <| IsCut.lt_trans (All_def.1 h.2.1 _ hx).1 hv
no goals
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
e : cut x ≠ Ordering.lt
x✝ : Ordering
hv : cut v✝ = Ordering.lt
hx : Any (fun x_1 => x = x_1) r✝
⊢ ∃ x, lowerBound? cut l✝ none = some x
cases e <| IsCut.lt_trans (All_def.1 h.2.1 _ hx).1 hv
no goals
case intro.intro.node.h_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ ∃ x, lowerBound? cut r✝ (some v✝) = some x
exact lowerBound?_of_some
no goals
case intro.intro.node.h_3
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ihl : Ordered cmp l✝ → ∀ (x : α), x ∈ l✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut l✝ none
r_ih✝ : Ordered cmp r✝ → ∀ (x : α), x ∈ r✝ → cut x ≠ Ordering.lt → ∃ x, x ∈ lowerBound? cut r✝ none
h : Ordered cmp (node c✝ l✝ v✝ r✝)
x : α
hx : x ∈ node c✝ l✝ v✝ r✝
e : cut x ≠ Ordering.lt
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ ∃ x, some v✝ = some x
exact ⟨_, rfl⟩