[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
r : R
n : ℕ
inst✝ : Nat.AtLeastTwo n
⊢ OfNat.ofNat n * r = n • r
[PROOFSTEP]
simp only [nsmul_eq_mul, Nat.cast_eq_ofNat]
[GOAL]
R : Type u_1
inst✝¹ : NonAssocSemiring R
r : R
n : ℕ
inst✝ : Nat.AtLeastTwo n
⊢ r * OfNat.ofNat n = n • r
[PROOFSTEP]
simp only [nsmul_eq_mul', Nat.cast_eq_ofNat]
