bug in rw tactic?

Stream: mathlib4

[Joël Riou]

While attempting to port RingTheory.WittVector.WittPolynomial !4#3355, I found a strange behaviour of rw. If we have to prove something like a * (b - Finset.sum ...) = 0, we should be able to do rw [sum_eq_zero], which should create two goals, firstly that a * (b - 0) = 0 and secondly the unspecified assumption tosum_eq_zero which is that all the terms in the Finset.sum are zero. This is not what is happening if we do that at https://github.com/leanprover-community/mathlib4/pull/3355/files#diff-f33593ea969bf958e5cb05e696cc502c949d9abfd4241a1f4be934e01466c818R236-R239
The second goal is created, but the sum is not replaced by zero in the original goal!?
(In this particular case, I could circumvent the problem though.)