no goals
α : Type ?u.208296
R✝ : Type ?u.208299
k : Type ?u.208302
S✝ : Type ?u.208305
M : Type u_1
M₂ : Type u_2
M₃ : Type ?u.208314
ι : Type ?u.208317
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✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ
x : M
⊢ ↑f (↑c • x) = ↑c • ↑f x
rw [Rat.cast_def, Rat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
  map_int_cast_smul f R S, map_inv_nat_cast_smul f R S]