α : Type ?u.134610
R : Type ?u.134613
k : Type ?u.134616
S : Type ?u.134619
M : Type u_1
M₂ : Type ?u.134625
M₃ : Type ?u.134628
ι : Type ?u.134631
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module ℕ M
n : ℕ
x : M
⊢ SMul.smul n x = n • x
α : Type ?u.134610
R : Type ?u.134613
k : Type ?u.134616
S : Type ?u.134619
M : Type u_1
M₂ : Type ?u.134625
M₃ : Type ?u.134628
ι : Type ?u.134631
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module ℕ M
n : ℕ
x : M
⊢ SMul.smul n x = n • x
rw [nsmul_eq_smul_cast ℕ n x, Nat.cast_id]
no goals
α : Type ?u.134610
R : Type ?u.134613
k : Type ?u.134616
S : Type ?u.134619
M : Type u_1
M₂ : Type ?u.134625
M₃ : Type ?u.134628
ι : Type ?u.134631
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module ℕ M
n : ℕ
x : M
⊢ SMul.smul n x = n • x
rfl