Theorem: ENat.mono (GMLInit/Data/Nat/Extended/Basic.lean)

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

State before:
n m : Nat
x : ENat
h : n ≤ m
hx : x.leNat n = true
⊢ x.leNat m = true
Tactic:
match Nat.le.dest h with
| ⟨_, h⟩ => cases h; exact mono_add hx
State after:
no goals

State before:
n m : Nat
x : ENat
h✝ : n ≤ m
hx : x.leNat n = true
w✝ : Nat
h : n + w✝ = m
⊢ x.leNat m = true
Tactic:
cases h
State after:
case refl
n : Nat
x : ENat
hx : x.leNat n = true
w✝ : Nat
h : n ≤ n + w✝
⊢ x.leNat (n + w✝) = true

State before:
case refl
n : Nat
x : ENat
hx : x.leNat n = true
w✝ : Nat
h : n ≤ n + w✝
⊢ x.leNat (n + w✝) = true
Tactic:
exact mono_add hx
State after:
no goals