-- 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
α : 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

Tactic:
rcases hx, hy with ⟨rfl | hx | hx, rfl | hy | hy⟩

Result:
case node.inl.inl
α : Type u_1
cmp : α → α → Ordering
y : α
inst✝ : TransCmp cmp
c✝ : RBColor
l r : RBNode α
hl : Ordered cmp l
hr : Ordered cmp r
e : cmp y y = Ordering.eq
ihl : Ordered cmp l → y ∈ l → y ∈ l → y = y
ihr : Ordered cmp r → y ∈ r → y ∈ r → y = y
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
⊢ y = y

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

case node.inl.inr.inr
α : 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) r
⊢ x = y

case node.inr.inl.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) l
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

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

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

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

case node.inr.inr.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) r
hy : Any (fun x => y = x) l
⊢ x = y

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

Proof state:
case node.inl.inr.inr
α : 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) r
⊢ x = y

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

Result:
no goals

Proof state:
case node.inr.inl.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) l
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 (All_def.1 lx _ hx).1

Result:
no goals

Proof state:
case nil
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝ : TransCmp cmp
e : cmp x y = Ordering.eq
ht : Ordered cmp nil
hx : x ∈ nil
hy : y ∈ nil
⊢ x = y

Tactic:
cases hx

Result:
no goals

Proof state:
case node.inl.inl
α : Type u_1
cmp : α → α → Ordering
y : α
inst✝ : TransCmp cmp
c✝ : RBColor
l r : RBNode α
hl : Ordered cmp l
hr : Ordered cmp r
e : cmp y y = Ordering.eq
ihl : Ordered cmp l → y ∈ l → y ∈ l → y = y
ihr : Ordered cmp r → y ∈ r → y ∈ r → y = y
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
⊢ y = y

Tactic:
rfl

Result:
no goals

Proof state:
case node.inr.inr.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) 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).trans (All_def.1 xr _ hx)).1

Result:
no goals