Theorem: Int.toNat_of_ofNat_inj (Table/BuiltinExtensions.lean)

State before:
⊢ ∀ (z : Int), z ≥ 0 → ofNat (toNat z) = z
Tactic:
intros z h
State after:
z : Int
h : z ≥ 0
⊢ ofNat (toNat z) = z

State before:
z : Int
h : z ≥ 0
⊢ ofNat (toNat z) = z
Tactic:
cases z with
| ofNat n => simp [toNat, ofNat]
| negSucc n => contradiction
State after:
no goals

State before:
case ofNat
n : Nat
h : ofNat n ≥ 0
⊢ ofNat (toNat (ofNat n)) = ofNat n
Tactic:
simp [toNat, ofNat]
State after:
no goals

State before:
case negSucc
n : Nat
h : negSucc n ≥ 0
⊢ ofNat (toNat (negSucc n)) = negSucc n
Tactic:
contradiction
State after:
no goals