Theorem: compareOfLessAndEq.symm (GMLInit/Data/OrdInstances.lean)

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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]
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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]
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals