no goals
α : Type ?u.166374
R✝ : Type ?u.166377
k : Type ?u.166380
S✝ : Type ?u.166383
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.166392
ι : Type ?u.166395
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
F : Type u_3
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : ℤ
a : M
⊢ ↑f (↑x • a) = ↑x • ↑f a
simp only [← zsmul_eq_smul_cast, map_zsmul]