no goals
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : { x // x ∈ S }
⊢ 1 • 1 • 0 = 1 • s • 0
rw [one_smul, smul_zero, smul_zero, one_smul]