Theorem: ENat.first_leNat_of (GMLInit/Data/Nat/Extended/First.lean)

State before:
p : Nat → Bool
x : Nat
h : p x = true
⊢ (first p).leNat x = true
Tactic:
match x with
| 0 => exact h
| x+1 => simp [first, first.leNat, h]
State after:
no goals

State before:
p : Nat → Bool
x : Nat
h : p 0 = true
⊢ (first p).leNat 0 = true
Tactic:
exact h
State after:
no goals

State before:
p : Nat → Bool
x✝ x : Nat
h : p (x + 1) = true
⊢ (first p).leNat (x + 1) = true
Tactic:
simp [first, first.leNat, h]
State after:
no goals