Theorem: Relation.LinearOrder.co_antisymm (GMLInit/Logic/Ordering.lean)

State before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
⊢ coRel r x y → coRel r y x → x = y
Tactic:
intro cxy cyx
State after:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
⊢ x = y

State before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
⊢ x = y
Tactic:
by_contradiction
| assuming hne =>
  cases Connex.connex (r:=r) hne with
  | inl hxy => absurd hxy; exact cyx
  | inr hyx => absurd hyx; exact cxy
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
⊢ False
Tactic:
cases Connex.connex (r:=r) hne with
| inl hxy => absurd hxy; exact cyx
| inr hyx => absurd hyx; exact cxy
State after:
no goals

State before:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hxy : r x y
⊢ False
Tactic:
absurd hxy
State after:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hxy : r x y
⊢ ¬r x y

State before:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hxy : r x y
⊢ ¬r x y
Tactic:
exact cyx
State after:
no goals

State before:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hyx : r y x
⊢ False
Tactic:
absurd hyx
State after:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hyx : r y x
⊢ ¬r y x

State before:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : StableEq α
x y : α
cxy : coRel r x y
cyx : coRel r y x
hne : ¬x = y
hyx : r y x
⊢ ¬r y x
Tactic:
exact cxy
State after:
no goals