no goals
α : Type ?u.256535
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : NonAssocSemiring R
n : ℕ
a : R
⊢ n • a = ↑n * a
rw [nsmul_eq_mul', (n.cast_commute a).eq]