Theorem: compareOfLT.symm (GMLInit/Data/OrdInstances.lean)

State before:
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
⊢ (compareOfLT x y).swap = compareOfLT y x
Tactic:
unfold compareOfLT
State after:
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
⊢ (if x < y then lt else if y < x then gt else eq).swap = if y < x then lt else if x < y then gt else eq

State before:
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
⊢ (if x < y then lt else if y < x then gt else eq).swap = if y < x then lt else if x < y then gt else eq
Tactic:
split
State after:
case isTrue
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝ : x < y
⊢ lt.swap = if y < x then lt else gt

case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝ : ¬x < y
⊢ (if y < x then gt else eq).swap = if y < x then lt else eq

State before:
case isTrue
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝ : x < y
⊢ lt.swap = if y < x then lt else gt

case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝ : ¬x < y
⊢ (if y < x then gt else eq).swap = if y < x then lt else eq
Tactic:
next hxy =>
  split
  next hyx  =>
    absurd hxy
    exact Asymmetric.asymm hyx
  next => rfl
State after:
case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝ : ¬x < y
⊢ (if y < x then gt else eq).swap = if y < x then lt else eq

State before:
case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝ : ¬x < y
⊢ (if y < x then gt else eq).swap = if y < x then lt else eq
Tactic:
next =>
  split
  next => rfl
  next => rfl
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
hxy : x < y
⊢ lt.swap = if y < x then lt else gt
Tactic:
split
State after:
case isTrue
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
hxy : x < y
h✝ : y < x
⊢ lt.swap = lt

case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
hxy : x < y
h✝ : ¬y < x
⊢ lt.swap = gt

State before:
case isTrue
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
hxy : x < y
h✝ : y < x
⊢ lt.swap = lt

case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
hxy : x < y
h✝ : ¬y < x
⊢ lt.swap = gt
Tactic:
next hyx  =>
  absurd hxy
  exact Asymmetric.asymm hyx
State after:
case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
hxy : x < y
h✝ : ¬y < x
⊢ lt.swap = gt

State before:
case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
hxy : x < y
h✝ : ¬y < x
⊢ lt.swap = gt
Tactic:
next => rfl
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
hxy : x < y
hyx : y < x
⊢ lt.swap = lt
Tactic:
absurd hxy
State after:
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
hxy : x < y
hyx : y < x
⊢ ¬x < y

State before:
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
hxy : x < y
hyx : y < x
⊢ ¬x < y
Tactic:
exact Asymmetric.asymm hyx
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
hxy : x < y
h✝ : ¬y < x
⊢ lt.swap = gt
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝ : ¬x < y
⊢ (if y < x then gt else eq).swap = if y < x then lt else eq
Tactic:
split
State after:
case isTrue
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
h✝ : y < x
⊢ gt.swap = lt

case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
h✝ : ¬y < x
⊢ eq.swap = eq

State before:
case isTrue
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
h✝ : y < x
⊢ gt.swap = lt

case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
h✝ : ¬y < x
⊢ eq.swap = eq
Tactic:
next => rfl
State after:
case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
h✝ : ¬y < x
⊢ eq.swap = eq

State before:
case isFalse
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
h✝ : ¬y < x
⊢ eq.swap = eq
Tactic:
next => rfl
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
h✝ : y < x
⊢ gt.swap = lt
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : Asymmetric fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
h✝ : ¬y < x
⊢ eq.swap = eq
Tactic:
rfl
State after:
no goals