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

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
⊢ compareOfLE x y = eq → x = y
Tactic:
unfold compareOfLE
State after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt) = eq → x = y

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt) = eq → x = y
Tactic:
intro cxy
State after:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) = eq
⊢ x = y

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
cxy : (if x ≤ y then if y ≤ x then eq else lt else gt) = eq
⊢ x = y
Tactic:
split at cxy
State after:
case isTrue
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
h✝ : x ≤ y
cxy : (if y ≤ x then eq else lt) = eq
⊢ x = y

case isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
h✝ : ¬x ≤ y
cxy : False
⊢ x = y

State before:
case isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
h✝ : ¬x ≤ y
cxy : False
⊢ x = y
Tactic:
next => contradiction
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
cxy : (if y ≤ x then eq else lt) = eq
⊢ x = y
Tactic:
split at cxy
State after:
case isTrue
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
h✝ : y ≤ x
cxy : eq = eq
⊢ x = y

case isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
h✝ : ¬y ≤ x
cxy : False
⊢ x = y

State before:
case isFalse
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
h✝ : ¬y ≤ x
cxy : False
⊢ x = y
Tactic:
next => contradiction
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
hyx : y ≤ x
cxy : eq = eq
⊢ x = y
Tactic:
antisymmetry using (.≤.)
State after:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
hyx : y ≤ x
cxy : eq = eq
⊢ x ≤ y

case a
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
hyx : y ≤ x
cxy : eq = eq
⊢ y ≤ x

State before:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
hyx : y ≤ x
cxy : eq = eq
⊢ x ≤ y
Tactic:
exact hxy
State after:
no goals

State before:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
hyx : y ≤ x
cxy : eq = eq
⊢ y ≤ x
Tactic:
exact hyx
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
hxy : x ≤ y
h✝ : ¬y ≤ x
cxy : False
⊢ x = y
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Antisymmetric fun x x_1 => x ≤ x_1
x y : α
h✝ : ¬x ≤ y
cxy : False
⊢ x = y
Tactic:
contradiction
State after:
no goals