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

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
⊢ compareOfLT x y = eq → x = y
Tactic:
unfold compareOfLT
State after:
α : 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
⊢ (if x < y then lt else if y < x then gt else eq) = eq → x = y

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
⊢ (if x < y then lt else if y < x then gt else eq) = eq → x = y
Tactic:
intro cxy
State after:
α : 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
cxy : (if x < y then lt else if y < x then gt else eq) = eq
⊢ x = y

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
cxy : (if x < y then lt else if y < x then gt else eq) = 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
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
h✝ : x < y
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
cxy : (if y < x then gt else eq) = eq
⊢ x = y

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
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
cxy : (if y < x then gt else eq) = eq
⊢ x = y
Tactic:
next => contradiction
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
cxy : (if y < x then gt else eq) = eq
⊢ x = y

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
cxy : (if y < x then gt else eq) = eq
⊢ x = y
Tactic:
next =>
  split at cxy
  next => contradiction
  next =>
    by_contradiction
    | assuming hne =>
      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
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
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
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
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

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

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

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

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

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

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

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