Theorem: ENat.le_antisymm (GMLInit/Data/Nat/Extended/Order.lean)

State before:
x y : ENat
⊢ x ≤ y → y ≤ x → x = y
Tactic:
intro hxy hyx
State after:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
⊢ x = y

State before:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
⊢ x = y
Tactic:
ext n
State after:
case leNat.h
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
⊢ x.leNat n = y.leNat n

State before:
case leNat.h
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
⊢ x.leNat n = y.leNat n
Tactic:
match hx : x.leNat n, hy : y.leNat n with
| true, true => rfl
| true, false =>
  cases hyx n with
  | inl h => simp only [h] at hy
  | inr h => simp only [h] at hx
| false, true =>
  cases hxy n with
  | inl h => simp only [h] at hx
  | inr h => simp only [h] at hy
| false, false => rfl
State after:
no goals

State before:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = true
hy : y.leNat n = true
⊢ true = true
Tactic:
rfl
State after:
no goals

State before:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
⊢ true = false
Tactic:
cases hyx n with
| inl h => simp only [h] at hy
| inr h => simp only [h] at hx
State after:
no goals

State before:
case inl
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
h : y.leNat n = true
⊢ true = false
Tactic:
simp only [h] at hy
State after:
no goals

State before:
case inr
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = true
hy : y.leNat n = false
h : x.leNat n = false
⊢ true = false
Tactic:
simp only [h] at hx
State after:
no goals

State before:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = false
hy : y.leNat n = true
⊢ false = true
Tactic:
cases hxy n with
| inl h => simp only [h] at hx
| inr h => simp only [h] at hy
State after:
no goals

State before:
case inl
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = false
hy : y.leNat n = true
h : x.leNat n = true
⊢ false = true
Tactic:
simp only [h] at hx
State after:
no goals

State before:
case inr
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = false
hy : y.leNat n = true
h : y.leNat n = false
⊢ false = true
Tactic:
simp only [h] at hy
State after:
no goals

State before:
x y : ENat
hxy : x ≤ y
hyx : y ≤ x
n : Nat
hx : x.leNat n = false
hy : y.leNat n = false
⊢ false = false
Tactic:
rfl
State after:
no goals