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

State before:
x : ENat
n : Nat
⊢ x.leNat n = true → x ≤ ENat.ofNat n
Tactic:
intro h k
State after:
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
⊢ x.leNat k = true ∨ (ENat.ofNat n).leNat k = false

State before:
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
⊢ x.leNat k = true ∨ (ENat.ofNat n).leNat k = false
Tactic:
cases Nat.lt_or_ge k n with
| inl hlt => right; rw [leNat_coe_eq_false_iff_gt]; exact hlt
| inr hge => left; exact mono hge h
State after:
no goals

State before:
case inl
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ x.leNat k = true ∨ (ENat.ofNat n).leNat k = false
Tactic:
right
State after:
case inl.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ (ENat.ofNat n).leNat k = false

State before:
case inl.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ (ENat.ofNat n).leNat k = false
Tactic:
rw [leNat_coe_eq_false_iff_gt]
State after:
case inl.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ k < n

State before:
case inl.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ k < n
Tactic:
exact hlt
State after:
no goals

State before:
case inr
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hge : k ≥ n
⊢ x.leNat k = true ∨ (ENat.ofNat n).leNat k = false
Tactic:
left
State after:
case inr.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hge : k ≥ n
⊢ x.leNat k = true

State before:
case inr.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hge : k ≥ n
⊢ x.leNat k = true
Tactic:
exact mono hge h
State after:
no goals