internlm/Lean-Github huggingface dataset:
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 : α
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
Tactic:
next heq =>
  absurd nxz
  rw [←heq]
  assumption
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 : α
nxz : ¬x < z
hne : ¬x = z
h✝² : x < y
cxy : lt ≠ gt
h✝¹ : ¬y < z
h✝ : ¬y = z
cyz : 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
h✝ : ¬y = z
cyz : gt ≠ gt
⊢ gt ≠ gt
Tactic:
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
heq : y = z
cyz : eq ≠ 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
heq : y = z
cyz : eq ≠ 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
heq : y = z
cyz : eq ≠ gt
⊢ x < z
Tactic:
rw [←heq]
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
heq : y = z
cyz : eq ≠ gt
⊢ x < y
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
heq : y = z
cyz : eq ≠ gt
⊢ x < y
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
h✝ : ¬y = z
cyz : gt ≠ gt
⊢ gt ≠ 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 : α
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
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
h✝ : x = y
cxy : 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 : α
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
hne : ¬x = z
h✝¹ : ¬x < y
h✝ : ¬x = y
cxy : 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 : α
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
hne : ¬x = z
h✝¹ : ¬x < y
h✝ : ¬x = y
cxy : gt ≠ gt
⊢ gt ≠ gt
Tactic:
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 : α
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
hne : ¬x = z
h✝ : ¬x < y
heq : x = y
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
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
heq : x = y
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
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
heq : x = y
cxy : eq ≠ gt
h✝ : ¬y < z
cyz : (if y = z then eq else gt) ≠ gt
⊢ 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 : α
nxz : ¬x < z
hne : ¬x = z
h✝¹ : ¬x < y
heq : x = y
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
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
heq : x = y
cxy : eq ≠ gt
h✝ : ¬y < z
cyz : (if y = z then eq else gt) ≠ gt
⊢ gt ≠ gt
Tactic:
next =>
  absurd nxz
  rw [heq]
  assumption
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 : α
nxz : ¬x < z
hne : ¬x = z
h✝¹ : ¬x < y
heq : x = y
cxy : eq ≠ gt
h✝ : ¬y < z
cyz : (if y = z 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 : α
nxz : ¬x < z
hne : ¬x = z
h✝¹ : ¬x < y
heq : x = y
cxy : eq ≠ 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
heq : x = y
cxy : eq ≠ 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
heq : x = y
cxy : eq ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ x < z
Tactic:
rw [heq]
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
heq : x = y
cxy : eq ≠ gt
h✝ : y < z
cyz : lt ≠ gt
⊢ y < 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
heq : x = y
cxy : eq ≠ 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
heq : x = y
cxy : eq ≠ 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
heq : x = y
cxy : eq ≠ 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
heq : x = y
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : ¬y = z
cyz : 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
heq : x = y
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : ¬y = z
cyz : gt ≠ gt
⊢ gt ≠ gt
Tactic:
next =>
  cases Connex.connex (r:=(.<.)) hne with
  | inl _ => contradiction
  | inr _ => 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
heq : x = y
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : y = z
cyz : eq ≠ gt
⊢ gt ≠ gt
Tactic:
absurd hne
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
heq : x = y
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : y = z
cyz : eq ≠ 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
heq : x = y
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : y = z
cyz : eq ≠ 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
heq : x = y
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : y = z
cyz : eq ≠ 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
heq : x = y
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : y = z
cyz : eq ≠ 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
heq : x = y
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : y = z
cyz : eq ≠ 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
heq : x = y
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : y = z
cyz : eq ≠ 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
heq : x = y
cxy : eq ≠ gt
h✝¹ : ¬y < z
h✝ : ¬y = z
cyz : gt ≠ gt
⊢ gt ≠ gt
Tactic:
cases Connex.connex (r:=(.<.)) hne with
| inl _ => contradiction
| inr _ => contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.le_trans
Proof state before:
case inl
α : 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
heq : x = y
cxy : eq ≠ gt
h✝² : ¬y < z
h✝¹ : ¬y = z
cyz : gt ≠ gt
h✝ : x < z
⊢ gt ≠ gt
Tactic:
contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.le_trans
Proof state before:
case inr
α : 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
heq : x = y
cxy : eq ≠ gt
h✝² : ¬y < z
h✝¹ : ¬y = z
cyz : gt ≠ gt
h✝ : z < x
⊢ gt ≠ 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 : α
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
hne : ¬x = z
h✝¹ : ¬x < y
h✝ : ¬x = y
cxy : gt ≠ gt
⊢ gt ≠ gt
Tactic:
contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.eq_strict
Proof state before:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
⊢ compareOfLessAndEq x y = eq → x = y
Tactic:
unfold compareOfLessAndEq
Proof state after:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
⊢ (if x < y then lt else if x = y then eq else gt) = eq → x = y
Theorem: compareOfLessAndEq.eq_strict
Proof state before:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
⊢ (if x < y then lt else if x = y then eq else gt) = eq → x = y
Tactic:
intro cxy
Proof state after:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
cxy : (if x < y then lt else if x = y then eq else gt) = eq
⊢ x = y
Theorem: compareOfLessAndEq.eq_strict
Proof state before:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
cxy : (if x < y then lt else if x = y then eq else gt) = 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
inst✝ : DecidableEq α
x y : α
h✝ : x < y
cxy : False
⊢ x = y

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

case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝ : ¬x < y
cxy : (if x = y then eq else gt) = 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
inst✝ : DecidableEq α
x y : α
h✝ : ¬x < y
cxy : (if x = y then eq else gt) = eq
⊢ x = y
Theorem: compareOfLessAndEq.eq_strict
Proof state before:
case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝ : ¬x < y
cxy : (if x = y then eq else gt) = eq
⊢ x = y
Tactic:
next =>
  split at cxy
  next => assumption
  next => contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.eq_strict
Proof state before:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝ : x < y
cxy : False
⊢ x = y
Tactic:
contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.eq_strict
Proof state before:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝ : ¬x < y
cxy : (if x = y then eq else gt) = 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
inst✝ : DecidableEq α
x y : α
h✝¹ : ¬x < y
h✝ : x = y
cxy : eq = eq
⊢ x = y

case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝¹ : ¬x < y
h✝ : ¬x = y
cxy : False
⊢ x = y
Theorem: compareOfLessAndEq.eq_strict
Proof state before:
case isTrue
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝¹ : ¬x < y
h✝ : x = y
cxy : eq = eq
⊢ x = y

case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝¹ : ¬x < y
h✝ : ¬x = y
cxy : False
⊢ x = y
Tactic:
next => assumption
Proof state after:
case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝¹ : ¬x < y
h✝ : ¬x = y
cxy : False
⊢ x = y
Theorem: compareOfLessAndEq.eq_strict
Proof state before:
case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝¹ : ¬x < y
h✝ : ¬x = y
cxy : False
⊢ x = y
Tactic:
next => contradiction
Proof state after:
no goals
Theorem: compareOfLessAndEq.eq_strict
Proof state before:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝¹ : ¬x < y
h✝ : x = y
cxy : eq = eq
⊢ x = y
Tactic:
assumption
Proof state after:
no goals
Theorem: compareOfLessAndEq.eq_strict
Proof state before:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝¹ : ¬x < y
h✝ : ¬x = y
cxy : False
⊢ x = y
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.add_sub_comm
Proof state before:
x y : Nat
⊢ x + (y - x) = y + (x - y)
Tactic:
rw [Nat.add_comm x, Nat.add_comm y, Nat.sub_add_eq_max, Nat.sub_add_eq_max, Nat.max_comm]
Proof state after:
no goals
Theorem: Nat.sub_sub_comm
Proof state before:
x y : Nat
⊢ x - (x - y) = y - (y - x)
Tactic:
rw [Nat.sub_sub_eq_min, Nat.sub_sub_eq_min, Nat.min_comm]
Proof state after:
no goals
Theorem: Nat.sub_lt_iff_lt_add_of_pos
Proof state before:
case zero_right
z : Nat
hz : z > 0
x : Nat
⊢ x - 0 < z ↔ x < 0 + z
Tactic:
rw [Nat.sub_zero, Nat.zero_add]
Proof state after:
no goals
Theorem: Nat.sub_lt_iff_lt_add_of_pos
Proof state before:
case zero_left
z : Nat
hz : z > 0
y : Nat
⊢ 0 - y < z ↔ 0 < y + z
Tactic:
rw [Nat.zero_sub]
Proof state after:
case zero_left
z : Nat
hz : z > 0
y : Nat
⊢ 0 < z ↔ 0 < y + z
Theorem: Nat.sub_lt_iff_lt_add_of_pos
Proof state before:
case zero_left
z : Nat
hz : z > 0
y : Nat
⊢ 0 < z ↔ 0 < y + z
Tactic:
constructor
Proof state after:
case zero_left.mp
z : Nat
hz : z > 0
y : Nat
⊢ 0 < z → 0 < y + z

case zero_left.mpr
z : Nat
hz : z > 0
y : Nat
⊢ 0 < y + z → 0 < z
Theorem: Nat.sub_lt_iff_lt_add_of_pos
Proof state before:
case zero_left.mp
z : Nat
hz : z > 0
y : Nat
⊢ 0 < z → 0 < y + z
Tactic:
intro
Proof state after:
case zero_left.mp
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ 0 < y + z
Theorem: Nat.sub_lt_iff_lt_add_of_pos
Proof state before:
case zero_left.mp
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ 0 < y + z
Tactic:
transitivity z using LT.lt, LE.le
Proof state after:
case zero_left.mp.left
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ 0 < z

case zero_left.mp.right
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ z ≤ y + z
Theorem: Nat.sub_lt_iff_lt_add_of_pos
Proof state before:
case zero_left.mp.left
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ 0 < z
Tactic:
exact hz
Proof state after:
no goals
Theorem: Nat.sub_lt_iff_lt_add_of_pos
Proof state before:
case zero_left.mp.right
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ z ≤ y + z
Tactic:
exact Nat.le_add_left ..
Proof state after:
no goals
Theorem: Nat.sub_lt_iff_lt_add_of_pos
Proof state before:
case zero_left.mpr
z : Nat
hz : z > 0
y : Nat
⊢ 0 < y + z → 0 < z
Tactic:
intro
Proof state after:
case zero_left.mpr
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < y + z
⊢ 0 < z
Theorem: Nat.sub_lt_iff_lt_add_of_pos
Proof state before:
case zero_left.mpr
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < y + z
⊢ 0 < z
Tactic:
exact hz
Proof state after:
no goals
Theorem: Nat.sub_lt_iff_lt_add_of_pos
Proof state before:
case succ_succ
z : Nat
hz : z > 0
x y : Nat
H : x - y < z ↔ x < y + z
⊢ x + 1 - (y + 1) < z ↔ x + 1 < y + 1 + z
Tactic:
rw [Nat.succ_sub_succ, Nat.succ_add, Nat.succ_eq, Nat.succ_lt_succ_iff]
Proof state after:
case succ_succ
z : Nat
hz : z > 0
x y : Nat
H : x - y < z ↔ x < y + z
⊢ x - y < z ↔ x < y + z
Theorem: Nat.sub_lt_iff_lt_add_of_pos
Proof state before:
case succ_succ
z : Nat
hz : z > 0
x y : Nat
H : x - y < z ↔ x < y + z
⊢ x - y < z ↔ x < y + z
Tactic:
apply H
Proof state after:
no goals
Theorem: Nat.sub_lt_of_pos_of_lt_add
Proof state before:
x y z : Nat
hpos : y > 0
⊢ x < y + z → x - z < y
Tactic:
intro h
Proof state after:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x - z < y
Theorem: Nat.sub_lt_of_pos_of_lt_add
Proof state before:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x - z < y
Tactic:
rw [Nat.sub_lt_iff_lt_add_of_pos]
Proof state after:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x < z + y

case hz
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ y > 0
Theorem: Nat.sub_lt_of_pos_of_lt_add
Proof state before:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x < z + y
Tactic:
rw [Nat.add_comm]
Proof state after:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x < y + z
Theorem: Nat.sub_lt_of_pos_of_lt_add
Proof state before:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x < y + z
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.sub_lt_of_pos_of_lt_add
Proof state before:
case hz
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ y > 0
Tactic:
exact hpos
Proof state after:
no goals
Theorem: Nat.lt_add_of_sub_lt
Proof state before:
case zero
x y : Nat
⊢ x - y < 0 → x < y + 0
Tactic:
intro
Proof state after:
case zero
x y : Nat
a✝ : x - y < 0
⊢ x < y + 0
Theorem: Nat.lt_add_of_sub_lt
Proof state before:
case zero
x y : Nat
a✝ : x - y < 0
⊢ x < y + 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.lt_add_of_sub_lt
Proof state before:
case succ
x y z : Nat
⊢ x - y < z + 1 → x < y + (z + 1)
Tactic:
intro h
Proof state after:
case succ
x y z : Nat
h : x - y < z + 1
⊢ x < y + (z + 1)
Theorem: Nat.lt_add_of_sub_lt
Proof state before:
case succ
x y z : Nat
h : x - y < z + 1
⊢ x < y + (z + 1)
Tactic:
rw [←Nat.sub_lt_iff_lt_add_of_pos]
Proof state after:
case succ
x y z : Nat
h : x - y < z + 1
⊢ x - y < z + 1

case succ.hz
x y z : Nat
h : x - y < z + 1
⊢ z + 1 > 0
Theorem: Nat.lt_add_of_sub_lt
Proof state before:
case succ
x y z : Nat
h : x - y < z + 1
⊢ x - y < z + 1
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.lt_add_of_sub_lt
Proof state before:
case succ.hz
x y z : Nat
h : x - y < z + 1
⊢ z + 1 > 0
Tactic:
exact Nat.zero_lt_succ ..
Proof state after:
no goals