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

State before:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
⊢ coRel r x y ∨ coRel r y x
Tactic:
by_cases r x y using Complemented with
| .isTrue hxy => left; exact Asymmetric.asymm hxy
| .isFalse nxy => right; exact nxy
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
hxy : r x y
⊢ coRel r x y ∨ coRel r y x
Tactic:
left
State after:
case h
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
hxy : r x y
⊢ coRel r x y

State before:
case h
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
hxy : r x y
⊢ coRel r x y
Tactic:
exact Asymmetric.asymm hxy
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
nxy : ¬r x y
⊢ coRel r x y ∨ coRel r y x
Tactic:
right
State after:
case h
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
nxy : ¬r x y
⊢ coRel r y x

State before:
case h
α : Sort u_1
r : α → α → Prop
self : LinearQuasiorder r
inst✝ : ComplementedRel r
x y : α
nxy : ¬r x y
⊢ coRel r y x
Tactic:
exact nxy
State after:
no goals