no goals
R : Type u_2
inst✝¹⁰ : CommSemiring R
A : Type u_3
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
M : Type u_1
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type ?u.945384
inst✝³ : AddCommMonoid N
inst✝² : Module A N
inst✝¹ : Module R N
inst✝ : IsScalarTower R A N
r : R
m : M
⊢ r • m = ↑(algebraMap R A) r • m
rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]