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

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
⊢ compareOfLT x y ≠ gt → compareOfLT y z ≠ gt → compareOfLT x z ≠ gt
Tactic:
unfold compareOfLT
State after:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
⊢ (if x < y then lt else if y < x then gt else eq) ≠ gt →
    (if y < z then lt else if z < y then gt else eq) ≠ gt → (if x < z then lt else if z < x then gt else eq) ≠ gt

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
⊢ (if x < y then lt else if y < x then gt else eq) ≠ gt →
    (if y < z then lt else if z < y then gt else eq) ≠ gt → (if x < z then lt else if z < x then gt else eq) ≠ gt
Tactic:
intro cxy cyz
State after:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
⊢ (if x < z then lt else if z < x then gt else eq) ≠ gt

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
⊢ (if x < z then lt else if z < x then gt else eq) ≠ gt
Tactic:
split
State after:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
h✝ : x < z
⊢ lt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
h✝ : ¬x < z
⊢ (if z < x then gt else eq) ≠ gt

State before:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
h✝ : x < z
⊢ lt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
h✝ : ¬x < z
⊢ (if z < x then gt else eq) ≠ gt
Tactic:
next => intro; contradiction
State after:
case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
h✝ : ¬x < z
⊢ (if z < x then gt else eq) ≠ gt

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
h✝ : x < z
⊢ lt ≠ gt
Tactic:
intro
State after:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
h✝ : x < z
a✝ : lt = gt
⊢ False

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
h✝ : x < z
a✝ : lt = gt
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
⊢ (if z < x then gt else eq) ≠ gt
Tactic:
split
State after:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
h✝ : z < x
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
h✝ : ¬z < x
⊢ eq ≠ gt

State before:
case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
h✝ : ¬z < x
⊢ eq ≠ gt
Tactic:
next => intro; contradiction
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
⊢ gt ≠ gt
Tactic:
split at cxy
State after:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
h✝ : x < y
cxy : lt ≠ gt
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
h✝ : ¬x < y
cxy : (if y < x then gt else eq) ≠ gt
⊢ gt ≠ gt

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
h✝ : x < y
cxy : lt ≠ gt
⊢ gt ≠ gt
Tactic:
split at cyz
State after:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
cyz : (if z < y then gt else eq) ≠ gt
⊢ gt ≠ gt

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ gt ≠ gt
Tactic:
absurd nxz
State after:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ x < z

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ x < z
Tactic:
transitivity y
State after:
case left
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ x < y

case right
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ y < z

State before:
case left
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ x < y
Tactic:
assumption
State after:
no goals

State before:
case right
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ y < z
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
cyz : (if z < y then gt else eq) ≠ gt
⊢ gt ≠ gt
Tactic:
split at cyz
State after:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : x < y
cxy : lt ≠ gt
h✝¹ : ¬y < z
h✝ : z < y
cyz : gt ≠ gt
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : x < y
cxy : lt ≠ gt
h✝¹ : ¬y < z
h✝ : ¬z < y
cyz : eq ≠ gt
⊢ gt ≠ gt

State before:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : x < y
cxy : lt ≠ gt
h✝¹ : ¬y < z
h✝ : z < y
cyz : gt ≠ gt
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : x < y
cxy : lt ≠ gt
h✝¹ : ¬y < z
h✝ : ¬z < y
cyz : eq ≠ gt
⊢ gt ≠ gt
Tactic:
next => contradiction
State after:
case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : x < y
cxy : lt ≠ gt
h✝¹ : ¬y < z
h✝ : ¬z < y
cyz : eq ≠ gt
⊢ gt ≠ gt

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : x < y
cxy : lt ≠ gt
h✝¹ : ¬y < z
h✝ : z < y
cyz : gt ≠ gt
⊢ gt ≠ gt
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
nzy : ¬z < y
cyz : eq ≠ gt
⊢ gt ≠ gt
Tactic:
absurd nzy
State after:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
nzy : ¬z < y
cyz : eq ≠ gt
⊢ z < y

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
nzy : ¬z < y
cyz : eq ≠ gt
⊢ z < y
Tactic:
transitivity x
State after:
case left
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
nzy : ¬z < y
cyz : eq ≠ gt
⊢ z < x

case right
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
nzy : ¬z < y
cyz : eq ≠ gt
⊢ x < y

State before:
case right
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
nzy : ¬z < y
cyz : eq ≠ gt
⊢ x < y
Tactic:
. assumption
State after:
no goals

State before:
case left
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
nzy : ¬z < y
cyz : eq ≠ gt
⊢ z < x
Tactic:
assumption
State after:
no goals

State before:
case right
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
nzy : ¬z < y
cyz : eq ≠ gt
⊢ x < y
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
h✝ : ¬x < y
cxy : (if y < x then gt else eq) ≠ gt
⊢ gt ≠ gt
Tactic:
split at cxy
State after:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
h✝ : y < x
cxy : gt ≠ gt
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
h✝ : ¬y < x
cxy : eq ≠ gt
⊢ gt ≠ gt

State before:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
h✝ : y < x
cxy : gt ≠ gt
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
h✝ : ¬y < x
cxy : eq ≠ gt
⊢ gt ≠ gt
Tactic:
next => contradiction
State after:
case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
h✝ : ¬y < x
cxy : eq ≠ gt
⊢ gt ≠ gt

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
h✝ : y < x
cxy : gt ≠ gt
⊢ gt ≠ gt
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
hzx : z < x
h✝ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
⊢ gt ≠ gt
Tactic:
split at cyz
State after:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : ¬y < z
cyz : (if z < y then gt else eq) ≠ gt
⊢ gt ≠ gt

State before:
case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : ¬y < z
cyz : (if z < y then gt else eq) ≠ gt
⊢ gt ≠ gt
Tactic:
next =>
  split at cyz
  next => contradiction
  next =>
    cases Comparison.compare hzx y with
    | inl _ => contradiction
    | inr _ => contradiction
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ gt ≠ gt
Tactic:
absurd nyx
State after:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ y < x

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ y < x
Tactic:
transitivity z
State after:
case left
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ y < z

case right
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ z < x

State before:
case right
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ z < x
Tactic:
. assumption
State after:
no goals

State before:
case left
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ y < z
Tactic:
assumption
State after:
no goals

State before:
case right
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ z < x
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝¹ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝ : ¬y < z
cyz : (if z < y then gt else eq) ≠ gt
⊢ gt ≠ gt
Tactic:
split at cyz
State after:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : z < y
cyz : gt ≠ gt
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : ¬z < y
cyz : eq ≠ gt
⊢ gt ≠ gt

State before:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : z < y
cyz : gt ≠ gt
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : ¬z < y
cyz : eq ≠ gt
⊢ gt ≠ gt
Tactic:
next => contradiction
State after:
case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : ¬z < y
cyz : eq ≠ gt
⊢ gt ≠ gt

State before:
case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : ¬z < y
cyz : eq ≠ gt
⊢ gt ≠ gt
Tactic:
next =>
  cases Comparison.compare hzx y with
  | inl _ => contradiction
  | inr _ => contradiction
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : z < y
cyz : gt ≠ gt
⊢ gt ≠ gt
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝² : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : ¬z < y
cyz : eq ≠ gt
⊢ gt ≠ gt
Tactic:
cases Comparison.compare hzx y with
| inl _ => contradiction
| inr _ => contradiction
State after:
no goals

State before:
case inl
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝³ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝² : ¬y < z
h✝¹ : ¬z < y
cyz : eq ≠ gt
h✝ : z < y
⊢ gt ≠ gt
Tactic:
contradiction
State after:
no goals

State before:
case inr
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
nxz : ¬x < z
hzx : z < x
h✝³ : ¬x < y
nyx : ¬y < x
cxy : eq ≠ gt
h✝² : ¬y < z
h✝¹ : ¬z < y
cyz : eq ≠ gt
h✝ : y < x
⊢ gt ≠ gt
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
h✝ : ¬z < x
⊢ eq ≠ gt
Tactic:
intro
State after:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
h✝ : ¬z < x
a✝ : eq = gt
⊢ False

State before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y z : α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Comparison fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) ≠ gt
cyz : (if y < z then lt else if z < y then gt else eq) ≠ gt
nxz : ¬x < z
h✝ : ¬z < x
a✝ : eq = gt
⊢ False
Tactic:
contradiction
State after:
no goals