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

State before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ coRel r x y → coRel r y z → coRel r x z
Tactic:
repeat rw [coRel_iff_asymRel]
State after:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → asymRel r x z

State before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → asymRel r x z
Tactic:
exact Preorder.as_trans
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → coRel r x z
Tactic:
rw [coRel_iff_asymRel]
State after:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → asymRel r x z