Theorem: Relation.LinearQuasiorder.co_trans (GMLInit/Logic/Ordering.lean)

State before:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
⊢ coRel r x y → coRel r y z → coRel r x z
Tactic:
intro cxy cyz rzx
State after:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
cxy : coRel r x y
cyz : coRel r y z
rzx : r z x
⊢ False

State before:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
cxy : coRel r x y
cyz : coRel r y z
rzx : r z x
⊢ False
Tactic:
cases Comparison.compare rzx y with
| inl rzy => exact cyz rzy
| inr ryx => exact cxy ryx
State after:
no goals

State before:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
cxy : coRel r x y
cyz : coRel r y z
rzx : r z x
rzy : r z y
⊢ False
Tactic:
exact cyz rzy
State after:
no goals

State before:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
x y z : α
cxy : coRel r x y
cyz : coRel r y z
rzx : r z x
ryx : r y x
⊢ False
Tactic:
exact cxy ryx
State after:
no goals