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

State before:
x : ENat
n : Nat
⊢ x ≤ ENat.ofNat n → x.leNat n = true
Tactic:
intro h
State after:
x : ENat
n : Nat
h : x ≤ ENat.ofNat n
⊢ x.leNat n = true

State before:
x : ENat
n : Nat
h : x ≤ ENat.ofNat n
⊢ x.leNat n = true
Tactic:
cases h n with
| inl h => exact h
| inr h => absurd h; simp only [leNat_coe_eq_false_iff_gt]; exact Nat.lt_irrefl _
State after:
no goals

State before:
case inl
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : x.leNat n = true
⊢ x.leNat n = true
Tactic:
exact h
State after:
no goals

State before:
case inr
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : (ENat.ofNat n).leNat n = false
⊢ x.leNat n = true
Tactic:
absurd h
State after:
case inr
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : (ENat.ofNat n).leNat n = false
⊢ ¬(ENat.ofNat n).leNat n = false

State before:
case inr
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : (ENat.ofNat n).leNat n = false
⊢ ¬(ENat.ofNat n).leNat n = false
Tactic:
simp only [leNat_coe_eq_false_iff_gt]
State after:
case inr
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : (ENat.ofNat n).leNat n = false
⊢ ¬n < n

State before:
case inr
x : ENat
n : Nat
h✝ : x ≤ ENat.ofNat n
h : (ENat.ofNat n).leNat n = false
⊢ ¬n < n
Tactic:
exact Nat.lt_irrefl _
State after:
no goals