no goals
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
s : { x // x ∈ S }
m : M
⊢ r • mk m s = mk (r • m) s
erw [mk_smul_mk r m 1 s, one_mul]