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

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

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

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

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

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

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

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

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

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

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

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