Theorem: Relation.PartialOrder.co_connex (GMLInit/Logic/Ordering.lean)

State before:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
⊢ x ≠ y → coRel r x y ∨ coRel r y x
Tactic:
intro hne
State after:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
⊢ coRel r x y ∨ coRel r y x

State before:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
⊢ coRel r x y ∨ coRel r y x
Tactic:
rw [←nand_iff_not_or_not]
State after:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
⊢ ¬(r y x ∧ r x y)

State before:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
⊢ ¬(r y x ∧ r x y)
Tactic:
intro ⟨hyx, hxy⟩
State after:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
hyx : r y x
hxy : r x y
⊢ False

State before:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
hyx : r y x
hxy : r x y
⊢ False
Tactic:
absurd hne
State after:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
hyx : r y x
hxy : r x y
⊢ x = y

State before:
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
hyx : r y x
hxy : r x y
⊢ x = y
Tactic:
exact Antisymmetric.antisymm hxy hyx
State after:
no goals