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

State before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
⊢ coRel r x y ↔ reflRel r x y
Tactic:
constructor
State after:
case mp
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
⊢ coRel r x y → reflRel r x y

case mpr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
⊢ reflRel r x y → coRel r x y

State before:
case mp
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
⊢ coRel r x y → reflRel r x y
Tactic:
intro cxy
State after:
case mp
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
⊢ reflRel r x y

State before:
case mp
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
⊢ reflRel r x y
Tactic:
by_cases r x y using Complemented with
| .isTrue hxy => left; exact hxy
| .isFalse cyx =>
  right
  by_contradiction
  | assuming hne =>
    cases Connex.connex (r:=r) hne with
    | inl hxy => absurd cyx; exact hxy
    | inr hyx => absurd cxy; exact hyx
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
hxy : r x y
⊢ reflRel r x y
Tactic:
left
State after:
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
hxy : r x y
⊢ r x y

State before:
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
hxy : r x y
⊢ r x y
Tactic:
exact hxy
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
⊢ reflRel r x y
Tactic:
right
State after:
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
cxy : coRel r x y
cyx : ¬r x y
⊢ x = y

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

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

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

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

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

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

State before:
case mpr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
⊢ reflRel r x y → coRel r x y
Tactic:
intro
| .inr rfl => exact Quasiorder.co_refl x
| .inl hxy => exact Asymmetric.asymm hxy
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
x✝ : reflRel r x y
⊢ coRel r x x
Tactic:
exact Quasiorder.co_refl x
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y✝ : α
x✝ : reflRel r x y✝
y : α
hxy : r x y
⊢ coRel r x y
Tactic:
exact Asymmetric.asymm hxy
State after:
no goals