-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.memP_iff_lowerBound? [@TransCmp α cmp] [IsCut cmp cut] (ht : Ordered cmp t) :
    t.MemP cut ↔ ∃ x, t.lowerBound? cut = some x ∧ cut x = .eq

Proof state:
case eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.eq
⊢ Ordering.eq = Ordering.eq

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
⊢ ∃ x, lowerBound? cut t = some x ∧ cut x = Ordering.eq

Tactic:
refine ⟨x, hx, ?_⟩

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
⊢ cut x = Ordering.eq

Proof state:
case lt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.lt
⊢ Ordering.lt = Ordering.eq

Tactic:
cases lowerBound?_le hx ex

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
⊢ MemP cut t ↔ ∃ x, lowerBound? cut t = some x ∧ cut x = Ordering.eq

Tactic:
refine memP_def.trans ⟨fun ⟨y, hy, ey⟩ => ?_, fun ⟨x, hx, e⟩ => ⟨_, lowerBound?_mem hx, e⟩⟩

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
⊢ ∃ x, lowerBound? cut t = some x ∧ cut x = Ordering.eq

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
⊢ cut x = Ordering.eq

Tactic:
cases ex : cut x

Result:
case lt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.lt
⊢ Ordering.lt = Ordering.eq

case eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.eq
⊢ Ordering.eq = Ordering.eq

case gt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.gt
⊢ Ordering.gt = Ordering.eq

Proof state:
case gt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.gt
⊢ Ordering.gt = Ordering.eq

Tactic:
cases e : cmp x y

Result:
case gt.lt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.gt
e : cmp x y = Ordering.lt
⊢ Ordering.gt = Ordering.eq

case gt.eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.gt
e : cmp x y = Ordering.eq
⊢ Ordering.gt = Ordering.eq

case gt.gt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.gt
e : cmp x y = Ordering.gt
⊢ Ordering.gt = Ordering.eq

Proof state:
case gt.gt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.gt
e : cmp x y = Ordering.gt
⊢ Ordering.gt = Ordering.eq

Tactic:
cases ey.symm.trans <| IsCut.gt_trans (OrientedCmp.cmp_eq_gt.1 e) ex

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
⊢ ∃ x, lowerBound? cut t = some x ∧ cut x = Ordering.eq

Tactic:
have ⟨x, hx⟩ := ht.lowerBound?_exists.2 ⟨_, hy, fun h => nomatch ey.symm.trans h⟩

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
⊢ ∃ x, lowerBound? cut t = some x ∧ cut x = Ordering.eq

Proof state:
case gt.lt
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.gt
e : cmp x y = Ordering.lt
⊢ Ordering.gt = Ordering.eq

Tactic:
cases ey.symm.trans <| ht.lowerBound?_greatest hx hy e ex

Result:
no goals

Proof state:
case gt.eq
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
x✝ : ∃ x, x ∈ t ∧ cut x = Ordering.eq
y : α
hy : y ∈ t
ey : cut y = Ordering.eq
x : α
hx : lowerBound? cut t = some x
ex : cut x = Ordering.gt
e : cmp x y = Ordering.eq
⊢ Ordering.gt = Ordering.eq

Tactic:
cases ey.symm.trans <| IsCut.congr e |>.symm.trans ex

Result:
no goals