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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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