-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem IsCut.congr [IsCut cmp cut] [TransCmp cmp] (H : cmp x y = .eq) : cut x = cut y

Proof state:
case eq.gt
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.eq
ex : cut x = Ordering.gt
h : cmp y x = Ordering.gt
⊢ False

Tactic:
cases H.symm.trans <| OrientedCmp.cmp_eq_gt.1 h

Result:
no goals

Proof state:
case gt
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.gt
⊢ cut x = Ordering.gt

Tactic:
exact IsCut.le_gt_trans (fun h => nomatch H.symm.trans h) ey

Result:
no goals

Proof state:
case eq.gt
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.eq
ex : cut x = Ordering.gt
⊢ Ordering.gt = Ordering.eq

Tactic:
refine IsCut.le_gt_trans (cmp := cmp) (fun h => ?_) ex |>.symm.trans ey

Result:
case eq.gt
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.eq
ex : cut x = Ordering.gt
h : cmp y x = Ordering.gt
⊢ False

Proof state:
case eq
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.eq
⊢ cut x = Ordering.eq

Tactic:
cases ex : cut x

Result:
case eq.lt
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.eq
ex : cut x = Ordering.lt
⊢ Ordering.lt = Ordering.eq

case eq.eq
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.eq
ex : cut x = Ordering.eq
⊢ Ordering.eq = Ordering.eq

case eq.gt
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.eq
ex : cut x = Ordering.gt
⊢ Ordering.gt = Ordering.eq

Proof state:
case eq.lt
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.eq
ex : cut x = Ordering.lt
⊢ Ordering.lt = Ordering.eq

Tactic:
exact IsCut.le_lt_trans (fun h => nomatch H.symm.trans h) ex |>.symm.trans ey

Result:
no goals

Proof state:
case eq.eq
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.eq
ex : cut x = Ordering.eq
⊢ Ordering.eq = Ordering.eq

Tactic:
rfl

Result:
no goals

Proof state:
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
⊢ cut x = cut y

Tactic:
cases ey : cut y

Result:
case lt
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.lt
⊢ cut x = Ordering.lt

case eq
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.eq
⊢ cut x = Ordering.eq

case gt
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.gt
⊢ cut x = Ordering.gt

Proof state:
case lt
α✝ : Sort u_1
cmp : α✝ → α✝ → Ordering
cut : α✝ → Ordering
x y : α✝
inst✝¹ : IsCut cmp cut
inst✝ : TransCmp cmp
H : cmp x y = Ordering.eq
ey : cut y = Ordering.lt
⊢ cut x = Ordering.lt

Tactic:
exact IsCut.le_lt_trans (fun h => nomatch H.symm.trans <| OrientedCmp.cmp_eq_gt.1 h) ey

Result:
no goals