cmp✝ : ?m.1112 → ?m.1112 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.1110
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp x y ≠ Ordering.lt
h₂ : cmp y z ≠ Ordering.lt
this : cmp z y ≠ Ordering.gt → cmp y x ≠ Ordering.gt → cmp z x ≠ Ordering.gt
⊢ cmp x z ≠ Ordering.lt
cmp✝ : ?m.1112 → ?m.1112 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.1110
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp x y ≠ Ordering.lt
h₂ : cmp y z ≠ Ordering.lt
⊢ cmp x z ≠ Ordering.lt
have := @TransCmp.le_trans _ cmp _ z y x
cmp✝ : ?m.1112 → ?m.1112 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.1110
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : ¬cmp x y = Ordering.lt
h₂ : ¬cmp y z = Ordering.lt
this : ¬cmp y z = Ordering.lt → ¬cmp x y = Ordering.lt → ¬cmp x z = Ordering.lt
⊢ ¬cmp x z = Ordering.lt
cmp✝ : ?m.1112 → ?m.1112 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.1110
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : cmp x y ≠ Ordering.lt
h₂ : cmp y z ≠ Ordering.lt
this : cmp z y ≠ Ordering.gt → cmp y x ≠ Ordering.gt → cmp z x ≠ Ordering.gt
⊢ cmp x z ≠ Ordering.lt
simp [cmp_eq_gt] at *
no goals
cmp✝ : ?m.1112 → ?m.1112 → Ordering
inst✝¹ : TransCmp cmp✝
x✝ : Sort ?u.1110
cmp : x✝ → x✝ → Ordering
inst✝ : TransCmp cmp
x y z : x✝
h₁ : ¬cmp x y = Ordering.lt
h₂ : ¬cmp y z = Ordering.lt
this : ¬cmp y z = Ordering.lt → ¬cmp x y = Ordering.lt → ¬cmp x z = Ordering.lt
⊢ ¬cmp x z = Ordering.lt
exact this h₂ h₁