Theorem: Relation.Preorder.as_trans (GMLInit/Logic/Ordering.lean)

State before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
⊢ asymRel r x y → asymRel r y z → asymRel r x z
Tactic:
intro ⟨hxy, cxy⟩ ⟨hyz, _⟩
State after:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ asymRel r x z

State before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ asymRel r x z
Tactic:
constructor
State after:
case left
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ r x z

case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ coRel r x z

State before:
case left
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ r x z
Tactic:
exact Transitive.trans hxy hyz
State after:
no goals

State before:
case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
⊢ coRel r x z
Tactic:
intro hzx
State after:
case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
hzx : r z x
⊢ False

State before:
case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
hzx : r z x
⊢ False
Tactic:
absurd cxy
State after:
case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
hzx : r z x
⊢ r y x

State before:
case right
α : Sort u_1
r : α → α → Prop
self : Preorder r
x y z : α
hxy : r x y
cxy : coRel r x y
hyz : r y z
right✝ : coRel r y z
hzx : r z x
⊢ r y x
Tactic:
exact Transitive.trans hyz hzx
State after:
no goals