no goals
u : Lean.Level
R✝ : Type ?u.333378
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
n : ℕ
R : Type u_1
inst✝ : Ring R
a : R
e : a = ↑(Int.negOfNat n)
⊢ a = Int.rawCast (Int.negOfNat n) + 0
simp [e]