internlm/Lean-Github huggingface dataset:
Theorem: compareOfLE.symm
Proof state before:
case inr
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
h✝¹ : ¬x ≤ y
h✝ : ¬y ≤ x
hyx : y ≤ x
⊢ ¬y ≤ x
Tactic:
assumption
Proof state after:
no goals
Theorem: compareOfLE.le_trans
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
⊢ compareOfLE x y ≠ gt → compareOfLE y z ≠ gt → compareOfLE x z ≠ gt
Tactic:
unfold compareOfLE
Proof state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt →
    (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt → (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Theorem: compareOfLE.le_trans
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt →
    (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt → (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Tactic:
intro cxy cyz
Proof state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Theorem: compareOfLE.le_trans
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Tactic:
have : x ≤ y := by by_contradiction | assuming h => split at cxy <;> contradiction
Proof state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this : x ≤ y
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Theorem: compareOfLE.le_trans
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this : x ≤ y
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Tactic:
have : y ≤ z := by by_contradiction | assuming h => split at cyz <;> contradiction
Proof state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝ : x ≤ y
this : y ≤ z
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Theorem: compareOfLE.le_trans
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝ : x ≤ y
this : y ≤ z
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Tactic:
have : x ≤ z := by transitivity y <;> assumption
Proof state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝¹ : x ≤ y
this✝ : y ≤ z
this : x ≤ z
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Theorem: compareOfLE.le_trans
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝¹ : x ≤ y
this✝ : y ≤ z
this : x ≤ z
⊢ (if x ≤ z then if z ≤ x then eq else lt else gt) ≠ gt
Tactic:
split <;> split <;> (intro; contradiction)
Proof state after:
no goals
Theorem: compareOfLE.le_trans
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
⊢ x ≤ y
Tactic:
by_contradiction | assuming h => split at cxy <;> contradiction
Proof state after:
no goals
Theorem: compareOfLE.le_trans
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
h : ¬x ≤ y
⊢ False
Tactic:
split at cxy <;> contradiction
Proof state after:
no goals
Theorem: compareOfLE.le_trans
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this : x ≤ y
⊢ y ≤ z
Tactic:
by_contradiction | assuming h => split at cyz <;> contradiction
Proof state after:
no goals
Theorem: compareOfLE.le_trans
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this : x ≤ y
h : ¬y ≤ z
⊢ False
Tactic:
split at cyz <;> contradiction
Proof state after:
no goals
Theorem: compareOfLE.le_trans
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝ : x ≤ y
this : y ≤ z
⊢ x ≤ z
Tactic:
transitivity y <;> assumption
Proof state after:
no goals
Theorem: compareOfLE.le_trans
Proof state before:
case isFalse.isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝¹ : x ≤ y
this✝ : y ≤ z
this : x ≤ z
h✝¹ : ¬x ≤ z
h✝ : ¬z ≤ x
⊢ lt ≠ gt
Tactic:
intro
Proof state after:
case isFalse.isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝¹ : x ≤ y
this✝ : y ≤ z
this : x ≤ z
h✝¹ : ¬x ≤ z
h✝ : ¬z ≤ x
a✝ : lt = gt
⊢ False
Theorem: compareOfLE.le_trans
Proof state before:
case isFalse.isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Transitive fun x x_1 => x ≤ x_1
x y z : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) ≠ gt
cyz : (if y ≤ z then if z ≤ y then eq else lt else gt) ≠ gt
this✝¹ : x ≤ y
this✝ : y ≤ z
this : x ≤ z
h✝¹ : ¬x ≤ z
h✝ : ¬z ≤ x
a✝ : lt = gt
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: compareOfLE.eq_strict
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
⊢ compareOfLE x y = eq → x = y
Tactic:
unfold compareOfLE
Proof state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt) = eq → x = y
Theorem: compareOfLE.eq_strict
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt) = eq → x = y
Tactic:
intro cxy
Proof state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) = eq
⊢ x = y
Theorem: compareOfLE.eq_strict
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) = eq
⊢ x = y
Tactic:
split at cxy
Proof state after:
case isTrue
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
h✝ : x ≤ y
cxy : (if y ≤ x then eq else lt) = eq
⊢ x = y

case isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
h✝ : ¬x ≤ y
cxy : False
⊢ x = y
Theorem: compareOfLE.eq_strict
Proof state before:
case isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
h✝ : ¬x ≤ y
cxy : False
⊢ x = y
Tactic:
next => contradiction
Proof state after:
no goals
Theorem: compareOfLE.eq_strict
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
cxy : (if y ≤ x then eq else lt) = eq
⊢ x = y
Tactic:
split at cxy
Proof state after:
case isTrue
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
h✝ : y ≤ x
cxy : eq = eq
⊢ x = y

case isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
h✝ : ¬y ≤ x
cxy : False
⊢ x = y
Theorem: compareOfLE.eq_strict
Proof state before:
case isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
h✝ : ¬y ≤ x
cxy : False
⊢ x = y
Tactic:
next => contradiction
Proof state after:
no goals
Theorem: compareOfLE.eq_strict
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
hyx : y ≤ x
cxy : eq = eq
⊢ x = y
Tactic:
antisymmetry using (.≤.)
Proof state after:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
hyx : y ≤ x
cxy : eq = eq
⊢ x ≤ y

case a
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
hyx : y ≤ x
cxy : eq = eq
⊢ y ≤ x
Theorem: compareOfLE.eq_strict
Proof state before:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
hyx : y ≤ x
cxy : eq = eq
⊢ x ≤ y
Tactic:
exact hxy
Proof state after:
no goals
Theorem: compareOfLE.eq_strict
Proof state before:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
hyx : y ≤ x
cxy : eq = eq
⊢ y ≤ x
Tactic:
exact hyx
Proof state after:
no goals
Theorem: compareOfLE.eq_strict
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
h✝ : ¬y ≤ x
cxy : False
⊢ x = y
Tactic:
contradiction
Proof state after:
no goals
Theorem: compareOfLE.eq_strict
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
h✝ : ¬x ≤ y
cxy : False
⊢ x = y
Tactic:
contradiction
Proof state after:
no goals
Theorem: compareOfLT.symm
Proof 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
Proof 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
Theorem: compareOfLT.symm
Proof 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
Proof 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
Theorem: compareOfLT.symm
Proof 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
Proof 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
Theorem: compareOfLT.symm
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.symm
Proof 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
Proof 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
Theorem: compareOfLT.symm
Proof 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
Proof 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
Theorem: compareOfLT.symm
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.symm
Proof 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
Proof 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
Theorem: compareOfLT.symm
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.symm
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.symm
Proof 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
Proof 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
Theorem: compareOfLT.symm
Proof 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
Proof 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
Theorem: compareOfLT.symm
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.symm
Proof 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
Proof state after:
no goals
Theorem: compareOfLT.symm
Proof 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
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
⊢ compareOfLT x y ≠ gt → compareOfLT y z ≠ gt → compareOfLT x z ≠ gt
Tactic:
unfold compareOfLT
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
⊢ (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
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
⊢ (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
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
⊢ (if x < z then lt else if z < x then gt else eq) ≠ 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
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
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
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
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
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
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
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
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
h✝ : x < z
⊢ lt ≠ 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
h✝ : x < z
a✝ : lt = 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
h✝ : x < z
a✝ : lt = gt
⊢ False
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
⊢ (if z < x then gt else eq) ≠ gt
Tactic:
split
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
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