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

State before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
⊢ reflRel r x y ∨ reflRel r y x
Tactic:
by_cases x = y using Complemented with
| .isTrue rfl => left; right; rfl
| .isFalse hne =>
  cases Connex.connex (r:=r) hne with
  | inl hxy => left; left; exact hxy
  | inr hyx => right; left; exact hyx
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x : α
⊢ reflRel r x x ∨ reflRel r x x
Tactic:
left
State after:
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x : α
⊢ reflRel r x x

State before:
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x : α
⊢ reflRel r x x
Tactic:
right
State after:
case h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x : α
⊢ x = x

State before:
case h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x : α
⊢ x = x
Tactic:
rfl
State after:
no goals

State before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
⊢ reflRel r x y ∨ reflRel r y x
Tactic:
cases Connex.connex (r:=r) hne with
| inl hxy => left; left; exact hxy
| inr hyx => right; left; exact hyx
State after:
no goals

State before:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hxy : r x y
⊢ reflRel r x y ∨ reflRel r y x
Tactic:
left
State after:
case inl.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hxy : r x y
⊢ reflRel r x y

State before:
case inl.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hxy : r x y
⊢ reflRel r x y
Tactic:
left
State after:
case inl.h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hxy : r x y
⊢ r x y

State before:
case inl.h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
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✝ : ComplementedEq α
x y : α
hne : ¬x = y
hyx : r y x
⊢ reflRel r x y ∨ reflRel r y x
Tactic:
right
State after:
case inr.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hyx : r y x
⊢ reflRel r y x

State before:
case inr.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hyx : r y x
⊢ reflRel r y x
Tactic:
left
State after:
case inr.h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hyx : r y x
⊢ r y x

State before:
case inr.h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hyx : r y x
⊢ r y x
Tactic:
exact hyx
State after:
no goals