Theorem: Relation.Quasiorder.rc_trans (GMLInit/Logic/Ordering.lean)

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
⊢ reflRel r x y → reflRel r y z → reflRel r x z
Tactic:
intro hxy hyz
State after:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ reflRel r x z

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ reflRel r x z
Tactic:
match hxy, hyz with
| Or.inr rfl, Or.inr rfl => right; rfl
| Or.inr rfl, Or.inl hyz => left; exact hyz
| Or.inl hxy, Or.inr rfl => left; exact hxy
| Or.inl hxy, Or.inl hyz => left; exact Transitive.trans hxy hyz
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ reflRel r x x
Tactic:
right
State after:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ x = x

State before:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z : α
hxy : reflRel r x y
hyz : reflRel r y z
⊢ x = x
Tactic:
rfl
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy : reflRel r x y
hyz✝ : reflRel r y z✝
z : α
hyz : r x z
⊢ reflRel r x z
Tactic:
left
State after:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy : reflRel r x y
hyz✝ : reflRel r y z✝
z : α
hyz : r x z
⊢ r x z

State before:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy : reflRel r x y
hyz✝ : reflRel r y z✝
z : α
hyz : r x z
⊢ r x z
Tactic:
exact hyz
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy✝ : reflRel r x y
hyz : reflRel r y z✝
z : α
hxy : r x z
⊢ reflRel r x z
Tactic:
left
State after:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy✝ : reflRel r x y
hyz : reflRel r y z✝
z : α
hxy : r x z
⊢ r x z

State before:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y z✝ : α
hxy✝ : reflRel r x y
hyz : reflRel r y z✝
z : α
hxy : r x z
⊢ r x z
Tactic:
exact hxy
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y✝ z✝ : α
hxy✝ : reflRel r x y✝
hyz✝ : reflRel r y✝ z✝
z y : α
hxy : r x y
hyz : r y z
⊢ reflRel r x z
Tactic:
left
State after:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y✝ z✝ : α
hxy✝ : reflRel r x y✝
hyz✝ : reflRel r y✝ z✝
z y : α
hxy : r x y
hyz : r y z
⊢ r x z

State before:
case h
α : Sort u_1
r : α → α → Prop
self : Quasiorder r
x y✝ z✝ : α
hxy✝ : reflRel r x y✝
hyz✝ : reflRel r y✝ z✝
z y : α
hxy : r x y
hyz : r y z
⊢ r x z
Tactic:
exact Transitive.trans hxy hyz
State after:
no goals