no goals
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
r₁ r₂ : R
⊢ 0 = r₁ • 0 + r₂ • 0 + 0 * 0
simp only [smul_zero, add_zero, MulZeroClass.mul_zero]