no goals
α : Type ?u.172942
R✝ : Type ?u.172945
k : Type ?u.172948
S✝ : Type ?u.172951
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.172960
ι : Type ?u.172963
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : ℕ
a : M
⊢ ↑f (↑x • a) = ↑x • ↑f a
simp only [← nsmul_eq_smul_cast, AddMonoidHom.map_nsmul, map_nsmul]