-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.unique [@TransCmp α cmp] (ht : Ordered cmp t)
    (hx : x ∈ t) (hy : y ∈ t) (e : cmp x y = .eq) : x = y

Proof state:
case node.inr.inr.inl
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝ : TransCmp cmp
e : cmp x y = Ordering.eq
c✝ : RBColor
l r : RBNode α
ihl : Ordered cmp l → x ∈ l → y ∈ l → x = y
ihr : Ordered cmp r → x ∈ r → y ∈ r → x = y
hl : Ordered cmp l
hr : Ordered cmp r
hx : Any (fun x_1 => x = x_1) r
ht : Ordered cmp (node c✝ l y r)
lx : All (fun x => cmpLT cmp x y) l
xr : All (fun x => cmpLT cmp y x) r
⊢ x = y

Tactic:
cases e.symm.trans <| OrientedCmp.cmp_eq_gt.2 (All_def.1 xr _ hx).1

Result:
no goals

Proof state:
case node.inr.inl.inr.inl
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝ : TransCmp cmp
e : cmp x y = Ordering.eq
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → x ∈ l → y ∈ l → x = y
ihr : Ordered cmp r → x ∈ r → y ∈ r → x = y
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
hx : Any (fun x_1 => x = x_1) l
hy : Any (fun x => y = x) l
⊢ x = y

Tactic:
exact ihl hl hx hy

Result:
no goals

Proof state:
case node.inr.inl.inr.inr
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝ : TransCmp cmp
e : cmp x y = Ordering.eq
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → x ∈ l → y ∈ l → x = y
ihr : Ordered cmp r → x ∈ r → y ∈ r → x = y
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
hx : Any (fun x_1 => x = x_1) l
hy : Any (fun x => y = x) r
⊢ x = y

Tactic:
cases e.symm.trans ((All_def.1 lx _ hx).trans (All_def.1 xr _ hy)).1

Result:
no goals

Proof state:
case node.inl.inr.inl
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝ : TransCmp cmp
e : cmp x y = Ordering.eq
c✝ : RBColor
l r : RBNode α
ihl : Ordered cmp l → x ∈ l → y ∈ l → x = y
ihr : Ordered cmp r → x ∈ r → y ∈ r → x = y
hl : Ordered cmp l
hr : Ordered cmp r
ht : Ordered cmp (node c✝ l x r)
lx : All (fun x_1 => cmpLT cmp x_1 x) l
xr : All (fun x_1 => cmpLT cmp x x_1) r
hy : Any (fun x => y = x) l
⊢ x = y

Tactic:
cases e.symm.trans <| OrientedCmp.cmp_eq_gt.2 (All_def.1 lx _ hy).1

Result:
no goals

Proof state:
case node.inr.inr.inr.inr
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝ : TransCmp cmp
e : cmp x y = Ordering.eq
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → x ∈ l → y ∈ l → x = y
ihr : Ordered cmp r → x ∈ r → y ∈ r → x = y
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
hx : Any (fun x_1 => x = x_1) r
hy : Any (fun x => y = x) r
⊢ x = y

Tactic:
exact ihr hr hx hy

Result:
no goals

Proof state:
case node
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝ : TransCmp cmp
e : cmp x y = Ordering.eq
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → x ∈ l → y ∈ l → x = y
ihr : Ordered cmp r → x ∈ r → y ∈ r → x = y
ht : Ordered cmp (node c✝ l v✝ r)
hx : x ∈ node c✝ l v✝ r
hy : y ∈ node c✝ l v✝ r
⊢ x = y

Tactic:
let ⟨lx, xr, hl, hr⟩ := ht

Result:
case node
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝ : TransCmp cmp
e : cmp x y = Ordering.eq
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → x ∈ l → y ∈ l → x = y
ihr : Ordered cmp r → x ∈ r → y ∈ r → x = y
ht : Ordered cmp (node c✝ l v✝ r)
hx : x ∈ node c✝ l v✝ r
hy : y ∈ node c✝ l v✝ r
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ x = y