no goals
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
r : R
a : A
⊢ 0 • 0 + r • a + a * 0 = r • a
rw [smul_zero, zero_add, MulZeroClass.mul_zero, add_zero]