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

State before:
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ coRel r x y ↔ asymRel r x y
Tactic:
constructor
State after:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ coRel r x y → asymRel r x y

case mpr
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ asymRel r x y → coRel r x y

State before:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ coRel r x y → asymRel r x y
Tactic:
intro cxy
State after:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ asymRel r x y

State before:
case mp
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ asymRel r x y
Tactic:
constructor
State after:
case mp.left
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ r x y

case mp.right
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ coRel r x y

State before:
case mp.left
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ r x y
Tactic:
cases Total.total (r:=r) x y with
| inl hxy => exact hxy
| inr hyx => absurd cxy; exact hyx
State after:
no goals

State before:
case mp.left.inl
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
hxy : r x y
⊢ r x y
Tactic:
exact hxy
State after:
no goals

State before:
case mp.left.inr
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
hyx : r y x
⊢ r x y
Tactic:
absurd cxy
State after:
case mp.left.inr
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
hyx : r y x
⊢ r y x

State before:
case mp.left.inr
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
hyx : r y x
⊢ r y x
Tactic:
exact hyx
State after:
no goals

State before:
case mp.right
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
cxy : coRel r x y
⊢ coRel r x y
Tactic:
exact cxy
State after:
no goals

State before:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalPreorder r
x y : α
⊢ asymRel r x y → coRel r x y
Tactic:
exact And.right
State after:
no goals