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

State before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
⊢ coRel r x y → ∀ (z : α), coRel r x z ∨ coRel r z y
Tactic:
intro cxy z
State after:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
⊢ coRel r x z ∨ coRel r z y

State before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
⊢ coRel r x z ∨ coRel r z y
Tactic:
rw [←Logic.nand_iff_not_or_not]
State after:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
⊢ ¬(r z x ∧ r y z)

State before:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
⊢ ¬(r z x ∧ r y z)
Tactic:
intro ⟨hzx, hyz⟩
State after:
α : Sort u_1
r : α → α → Prop
self : Preorder r
inst✝ : WeaklyComplementedRel r
x y : α
cxy : coRel r x y
z : α
hzx : r z x
hyz : r y z
⊢ False

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

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