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

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

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

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

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