internlm/Lean-Github huggingface dataset:
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 : (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
h✝ : y < x
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
h✝ : ¬y < x
cxy : 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
h✝ : y < x
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
h✝ : ¬y < x
cxy : 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
h✝ : ¬y < x
cxy : 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
h✝ : ¬y < x
cxy : eq = eq
⊢ x = y
Tactic:
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
h✝ : y < x
cxy : False
⊢ x = y
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
h✝¹ : ¬x < y
h✝ : ¬y < x
cxy : eq = eq
⊢ x = y
Tactic:
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
h✝ : ¬y < x
cxy : eq = eq
hne : ¬x = y
⊢ False
Tactic:
cases Connex.connex (r:=(.<.)) hne with
| inl _ => contradiction
| inr _ => contradiction
Proof state after:
no goals
Theorem: compareOfLT.eq_strict
Proof state before:
case inl
α : 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
h✝¹ : ¬y < x
cxy : eq = eq
hne : ¬x = y
h✝ : x < y
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: compareOfLT.eq_strict
Proof state before:
case inr
α : 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
h✝¹ : ¬y < x
cxy : eq = eq
hne : ¬x = y
h✝ : y < x
⊢ False
Tactic:
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 : α
⊢ (compareOfLessAndEq x y).swap = compareOfLessAndEq y x
Tactic:
unfold compareOfLessAndEq
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 : α
⊢ (if x < y then lt else if x = y then eq else gt).swap = if y < x then lt else if y = x then eq else gt
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 : α
⊢ (if x < y then lt else if x = y then eq else 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
⊢ lt.swap = if y < x then lt else if y = x then eq else gt

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
⊢ (if x = y then eq else gt).swap = if y < x then lt else 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
⊢ (if x = y then eq else gt).swap = if y < x then lt else if y = x then eq else gt
Tactic:
next =>
  split
  next heq =>
    split
    next hlt =>
      absurd hlt
      rw [heq]
      exact Irreflexive.irrfl
    next =>
      split
      next => rfl
      next hne =>
        absurd hne
        symmetry
        assumption
  next hne =>
    split
    next => rfl
    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 : α
hlt : x < y
⊢ lt.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 : α
hlt : 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✝³ : 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 : α
hlt : x < y
h✝ : ¬y < x
⊢ lt.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 : α
hlt : x < y
h✝ : ¬y < x
⊢ lt.swap = if y = x then eq else gt
Tactic:
next =>
  split
  next heq =>
    absurd hlt
    rw [heq]
    exact Irreflexive.irrfl
  next => 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 : α
hlt : x < y
h✝ : y < x
⊢ lt.swap = lt
Tactic:
absurd Irreflexive.irrefl (r:=(.<.)) x
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 : α
hlt : x < y
h✝ : y < x
⊢ x < 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 : α
hlt : x < y
h✝ : y < x
⊢ x < x
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✝² : 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 : α
hlt : x < y
h✝ : y < x
⊢ x < y

case right
α : 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 : α
hlt : x < y
h✝ : y < x
⊢ y < x
Theorem: compareOfLessAndEq.symm
Proof state before:
case left
α : 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 : α
hlt : x < y
h✝ : y < x
⊢ x < y
Tactic:
assumption
Proof state after:
no goals
Theorem: compareOfLessAndEq.symm
Proof state before:
case right
α : 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 : α
hlt : x < y
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 : α
hlt : x < y
h✝ : ¬y < x
⊢ lt.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 : α
hlt : x < y
h✝¹ : ¬y < x
h✝ : y = x
⊢ lt.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 : α
hlt : x < y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ lt.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 : α
hlt : x < y
h✝¹ : ¬y < x
h✝ : y = x
⊢ lt.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 : α
hlt : x < y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ lt.swap = gt
Tactic:
next heq =>
  absurd hlt
  rw [heq]
  exact Irreflexive.irrfl
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 : α
hlt : x < y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ lt.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 : α
hlt : x < y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ lt.swap = gt
Tactic:
next => 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 : α
hlt : x < y
h✝ : ¬y < x
heq : y = x
⊢ lt.swap = eq
Tactic:
absurd hlt
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 : α
hlt : x < y
h✝ : ¬y < x
heq : 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 : α
hlt : x < y
h✝ : ¬y < x
heq : y = x
⊢ ¬x < y
Tactic:
rw [heq]
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 : α
hlt : x < y
h✝ : ¬y < x
heq : y = x
⊢ ¬x < 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 : α
hlt : x < y
h✝ : ¬y < x
heq : y = x
⊢ ¬x < x
Tactic:
exact Irreflexive.irrfl
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 : α
hlt : x < y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ lt.swap = gt
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
⊢ (if x = y then eq else 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
h✝ : x = y
⊢ eq.swap = if y < x then lt else if y = x then eq else gt

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
h✝ : ¬x = y
⊢ gt.swap = if y < x then lt else 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
h✝ : x = y
⊢ eq.swap = if y < x then lt else if y = x then eq else gt

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
h✝ : ¬x = y
⊢ gt.swap = if y < x then lt else if y = x then eq else gt
Tactic:
next heq =>
  split
  next hlt =>
    absurd hlt
    rw [heq]
    exact Irreflexive.irrfl
  next =>
    split
    next => rfl
    next hne =>
      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
h✝ : ¬x = y
⊢ gt.swap = if y < x then lt else 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
h✝ : ¬x = y
⊢ gt.swap = if y < x then lt else if y = x then eq else gt
Tactic:
next hne =>
  split
  next => rfl
  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
heq : x = y
⊢ eq.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
heq : x = y
h✝ : y < x
⊢ eq.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
heq : x = y
h✝ : ¬y < x
⊢ eq.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
heq : x = y
h✝ : y < x
⊢ eq.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
heq : x = y
h✝ : ¬y < x
⊢ eq.swap = if y = x then eq else gt
Tactic:
next hlt =>
  absurd hlt
  rw [heq]
  exact Irreflexive.irrfl
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
heq : x = y
h✝ : ¬y < x
⊢ eq.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
heq : x = y
h✝ : ¬y < x
⊢ eq.swap = if y = x then eq else gt
Tactic:
next =>
  split
  next => rfl
  next hne =>
    absurd hne
    symmetry
    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
heq : x = y
hlt : y < x
⊢ eq.swap = lt
Tactic:
absurd hlt
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
hlt : 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
hlt : y < x
⊢ ¬y < x
Tactic:
rw [heq]
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
hlt : y < x
⊢ ¬y < 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
hlt : y < x
⊢ ¬y < y
Tactic:
exact Irreflexive.irrfl
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
heq : x = y
h✝ : ¬y < x
⊢ eq.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
heq : x = y
h✝¹ : ¬y < x
h✝ : y = x
⊢ eq.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
heq : x = y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ eq.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
heq : x = y
h✝¹ : ¬y < x
h✝ : y = x
⊢ eq.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
heq : x = y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ eq.swap = 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
heq : x = y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ eq.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
heq : x = y
h✝¹ : ¬y < x
h✝ : ¬y = x
⊢ eq.swap = gt
Tactic:
next hne =>
  absurd hne
  symmetry
  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
heq : x = y
h✝¹ : ¬y < x
h✝ : y = x
⊢ eq.swap = eq
Tactic:
rfl
Proof state after:
no goals