internlm/Lean-Github huggingface dataset:
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.le_trans
Proof 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
Proof 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
Theorem: compareOfLT.le_trans
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.eq_strict
Proof state before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
⊢ compareOfLT x y = eq → x = y
Tactic:
unfold compareOfLT
Proof state after:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
⊢ (if x < y then lt else if y < x then gt else eq) = eq → x = y
Theorem: compareOfLT.eq_strict
Proof state before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
⊢ (if x < y then lt else if y < x then gt else eq) = eq → x = y
Tactic:
intro cxy
Proof state after:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) = eq
⊢ x = y
Theorem: compareOfLT.eq_strict
Proof state before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
cxy : (if x < y then lt else if y < x then gt else eq) = eq
⊢ x = y
Tactic:
split at cxy
Proof state after:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
h✝ : x < y
cxy : False
⊢ x = y

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
h✝ : ¬x < y
cxy : (if y < x then gt else eq) = eq
⊢ x = y
Theorem: compareOfLT.eq_strict
Proof state before:
case isTrue
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
h✝ : x < y
cxy : False
⊢ x = y

case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
h✝ : ¬x < y
cxy : (if y < x then gt else eq) = eq
⊢ x = y
Tactic:
next => contradiction
Proof state after:
case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
h✝ : ¬x < y
cxy : (if y < x then gt else eq) = eq
⊢ x = y
Theorem: compareOfLT.eq_strict
Proof state before:
case isFalse
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
h✝ : ¬x < y
cxy : (if y < x then gt else eq) = eq
⊢ x = y
Tactic:
next =>
  split at cxy
  next => contradiction
  next =>
    by_contradiction
    | assuming hne =>
      cases Connex.connex (r:=(.<.)) hne with
      | inl _ => contradiction
      | inr _ => contradiction
Proof state after:
no goals
Theorem: compareOfLT.eq_strict
Proof state before:
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
h✝ : x < y
cxy : False
⊢ x = y
Tactic:
contradiction
Proof state after:
no goals