Theorem: Relation.TotalOrder.coRel_iff_rel_and_ne (GMLInit/Logic/Ordering.lean)

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

case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
⊢ r x y ∧ x ≠ y → coRel r x y

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

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

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

State before:
case mp.left
α : Sort u_1
r : α → α → Prop
self : TotalOrder 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 : TotalOrder 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 : TotalOrder 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 : TotalOrder 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 : TotalOrder 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 : TotalOrder r
x y : α
cxy : coRel r x y
⊢ x ≠ y
Tactic:
intro | rfl => absurd cxy; exact Reflexive.rfl
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
x✝ : x = y
cxy : coRel r x x
⊢ False
Tactic:
absurd cxy
State after:
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
x✝ : x = y
cxy : coRel r x x
⊢ r x x

State before:
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
x✝ : x = y
cxy : coRel r x x
⊢ r x x
Tactic:
exact Reflexive.rfl
State after:
no goals

State before:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
⊢ r x y ∧ x ≠ y → coRel r x y
Tactic:
intro ⟨hxy, hne⟩ hyx
State after:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
hxy : r x y
hne : x ≠ y
hyx : r y x
⊢ False

State before:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
hxy : r x y
hne : x ≠ y
hyx : r y x
⊢ False
Tactic:
absurd hne
State after:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
hxy : r x y
hne : x ≠ y
hyx : r y x
⊢ x = y

State before:
case mpr
α : Sort u_1
r : α → α → Prop
self : TotalOrder r
x y : α
hxy : r x y
hne : x ≠ y
hyx : r y x
⊢ x = y
Tactic:
exact Antisymmetric.antisymm hxy hyx
State after:
no goals