internlm/Lean-Github huggingface dataset:
Theorem: compareOfLessAndEq.symm
Proof state before:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
heq : x = y
h✝ : ¬y < x
hne : ¬y = x
⊢ eq.swap = gt
Tactic:
absurd hne
Proof state after:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
heq : x = y
h✝ : ¬y < x
hne : ¬y = x
⊢ y = x
Theorem: compareOfLessAndEq.symm
Proof state before:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
heq : x = y
h✝ : ¬y < x
hne : ¬y = x
⊢ y = x
Tactic:
symmetry
Proof state after:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
heq : x = y
h✝ : ¬y < x
hne : ¬y = x
⊢ x = y
Theorem: compareOfLessAndEq.symm
Proof state before:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
heq : x = y
h✝ : ¬y < x
hne : ¬y = x
⊢ x = y
Tactic:
assumption
Proof state after:
no goals
Theorem: compareOfLessAndEq.symm
Proof state before:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝ : ¬x < y
hne : ¬x = y
⊢ gt.swap = if y < x then lt else if y = x then eq else gt
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
hne : ¬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✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
hne : ¬x = y
h✝ : ¬y < x
⊢ gt.swap = if y = x then eq else gt
Theorem: compareOfLessAndEq.symm
Proof state before:
case isTrue
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
hne : ¬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✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
hne : ¬x = y
h✝ : ¬y < x
⊢ gt.swap = if y = x then eq else gt
Tactic:
next => rfl
Proof state after:
case isFalse
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
hne : ¬x = y
h✝ : ¬y < x
⊢ gt.swap = if y = x then eq else gt
Theorem: compareOfLessAndEq.symm
Proof state before:
case isFalse
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
hne : ¬x = y
h✝ : ¬y < x
⊢ gt.swap = if y = x then eq else gt
Tactic:
next =>
  split
  next =>
    absurd hne
    symmetry
    assumption
  next =>
    cases Connex.connex (r:=(.<.)) hne with
    | inl _ => contradiction
    | inr _ => contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.symm
Proof state before:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
hne : ¬x = y
h✝ : y < x
⊢ gt.swap = lt
Tactic:
rfl
Proof state after:
no goals
Theorem: compareOfLessAndEq.symm
Proof state before:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝¹ : ¬x < y
hne : ¬x = y
h✝ : ¬y < x
⊢ gt.swap = if y = x then eq else gt
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : y = x
⊢ gt.swap = eq

case isFalse
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ gt.swap = gt
Theorem: compareOfLessAndEq.symm
Proof state before:
case isTrue
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : y = x
⊢ gt.swap = eq

case isFalse
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ gt.swap = gt
Tactic:
next =>
  absurd hne
  symmetry
  assumption
Proof state after:
case isFalse
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ gt.swap = gt
Theorem: compareOfLessAndEq.symm
Proof state before:
case isFalse
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ gt.swap = gt
Tactic:
next =>
  cases Connex.connex (r:=(.<.)) hne with
  | inl _ => contradiction
  | inr _ => contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.symm
Proof state before:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : y = x
⊢ gt.swap = eq
Tactic:
absurd hne
Proof state after:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : y = x
⊢ x = y
Theorem: compareOfLessAndEq.symm
Proof state before:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : y = x
⊢ x = y
Tactic:
symmetry
Proof state after:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : y = x
⊢ y = x
Theorem: compareOfLessAndEq.symm
Proof state before:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : y = x
⊢ y = x
Tactic:
assumption
Proof state after:
no goals
Theorem: compareOfLessAndEq.symm
Proof state before:
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝² : ¬x < y
hne : ¬x = y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ gt.swap = gt
Tactic:
cases Connex.connex (r:=(.<.)) hne with
| inl _ => contradiction
| inr _ => contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.symm
Proof state before:
case inl
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝³ : ¬x < y
hne : ¬x = y
h✝² : ¬y < x
h✝¹ : ¬y = x
h✝ : x < y
⊢ gt.swap = gt
Tactic:
contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.symm
Proof state before:
case inr
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝³ : ¬x < y
hne : ¬x = y
h✝² : ¬y < x
h✝¹ : ¬y = x
h✝ : y < x
⊢ gt.swap = gt
Tactic:
contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
⊢ compareOfLessAndEq x y ≠ gt → compareOfLessAndEq y z ≠ gt → compareOfLessAndEq x z ≠ gt
Tactic:
unfold compareOfLessAndEq
Proof state after:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
⊢ (if x < y then lt else if x = y then eq else gt) ≠ gt →
    (if y < z then lt else if y = z then eq else gt) ≠ gt → (if x < z then lt else if x = z then eq else gt) ≠ gt
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
⊢ (if x < y then lt else if x = y then eq else gt) ≠ gt →
    (if y < z then lt else if y = z then eq else gt) ≠ gt → (if x < z then lt else if x = z then eq else gt) ≠ gt
Tactic:
intro cxy cyz
Proof state after:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
⊢ (if x < z then lt else if x = z then eq else gt) ≠ gt
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
⊢ (if x < z then lt else if x = z then eq else gt) ≠ gt
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
h✝ : x < z
⊢ lt ≠ gt

case isFalse
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
h✝ : ¬x < z
⊢ (if x = z then eq else gt) ≠ gt
Theorem: compareOfLessAndEq.le_trans
Proof state before:
case isTrue
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
h✝ : x < z
⊢ lt ≠ gt

case isFalse
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
h✝ : ¬x < z
⊢ (if x = z then eq else gt) ≠ gt
Tactic:
next => intro; contradiction
Proof state after:
case isFalse
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
h✝ : ¬x < z
⊢ (if x = z then eq else gt) ≠ gt
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ 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
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
h✝ : x < z
a✝ : lt = gt
⊢ False
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
h✝ : x < z
a✝ : lt = gt
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
⊢ (if x = z then eq else gt) ≠ gt
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
h✝ : x = z
⊢ eq ≠ gt

case isFalse
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
h✝ : ¬x = z
⊢ gt ≠ gt
Theorem: compareOfLessAndEq.le_trans
Proof state before:
case isTrue
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
h✝ : x = z
⊢ eq ≠ gt

case isFalse
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
h✝ : ¬x = z
⊢ gt ≠ gt
Tactic:
next => intro; contradiction
Proof state after:
case isFalse
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
h✝ : ¬x = z
⊢ gt ≠ gt
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
h✝ : x = z
⊢ eq ≠ gt
Tactic:
intro
Proof state after:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
h✝ : x = z
a✝ : eq = gt
⊢ False
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
h✝ : x = z
a✝ : eq = gt
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
hne : ¬x = z
⊢ 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
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
hne : ¬x = z
h✝ : x < y
cxy : lt ≠ gt
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
hne : ¬x = z
h✝ : ¬x < y
cxy : (if x = y then eq else gt) ≠ gt
⊢ gt ≠ gt
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
hne : ¬x = z
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
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
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
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
cyz : (if y = z then eq else gt) ≠ gt
⊢ gt ≠ gt
Theorem: compareOfLessAndEq.le_trans
Proof state before:
case isFalse
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
cyz : (if y = z then eq else gt) ≠ gt
⊢ gt ≠ gt
Tactic:
next =>
  split at cyz
  next heq =>
    absurd nxz
    rw [←heq]
    assumption
  next => contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
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
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ x < z
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
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
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
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
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ y < z
Theorem: compareOfLessAndEq.le_trans
Proof state before:
case left
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ x < y
Tactic:
assumption
Proof state after:
no goals
Theorem: compareOfLessAndEq.le_trans
Proof state before:
case right
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ y < z
Tactic:
assumption
Proof state after:
no goals
Theorem: compareOfLessAndEq.le_trans
Proof state before:
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
h✝¹ : x < y
cxy : lt ≠ gt
h✝ : ¬y < z
cyz : (if y = z then eq else gt) ≠ 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
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
h✝² : x < y
cxy : lt ≠ gt
h✝¹ : ¬y < z
h✝ : y = z
cyz : eq ≠ gt
⊢ gt ≠ gt

case isFalse
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
nxz : ¬x < z
hne : ¬x = z
h✝² : x < y
cxy : lt ≠ gt
h✝¹ : ¬y < z
h✝ : ¬y = z
cyz : gt ≠ gt
⊢ gt ≠ gt