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

State before:
n : Nat
⊢ negSucc n = -ofNat (Nat.succ n)
Tactic:
unfold Neg.neg
State after:
n : Nat
⊢ negSucc n = instNegInt.1 (ofNat (Nat.succ n))

State before:
n : Nat
⊢ negSucc n = instNegInt.1 (ofNat (Nat.succ n))
Tactic:
unfold instNegInt
State after:
n : Nat
⊢ negSucc n = { neg := Int.neg }.1 (ofNat (Nat.succ n))

State before:
n : Nat
⊢ negSucc n = { neg := Int.neg }.1 (ofNat (Nat.succ n))
Tactic:
unfold Int.neg
State after:
n : Nat
⊢ negSucc n =
    {
          neg := fun n =>
            match n with
            | ofNat n => negOfNat n
            | negSucc n => ofNat (Nat.succ n) }.1
      (ofNat (Nat.succ n))

State before:
n : Nat
⊢ negSucc n =
    {
          neg := fun n =>
            match n with
            | ofNat n => negOfNat n
            | negSucc n => ofNat (Nat.succ n) }.1
      (ofNat (Nat.succ n))
Tactic:
simp only [negOfNat]
State after:
no goals