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
α✝ : 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
cases ey : cut y
no goals
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
exact IsCut.le_lt_trans (fun h => nomatch H.symm.trans <| OrientedCmp.cmp_eq_gt.1 h) ey
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
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
cases ex : cut x
no goals
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
exact IsCut.le_lt_trans (fun h => nomatch H.symm.trans h) ex |>.symm.trans ey
no goals
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
rfl
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
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
refine IsCut.le_gt_trans (cmp := cmp) (fun h => ?_) ex |>.symm.trans ey
no goals
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
cases H.symm.trans <| OrientedCmp.cmp_eq_gt.1 h
no goals
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
exact IsCut.le_gt_trans (fun h => nomatch H.symm.trans h) ey