simp_rw not working as expected

Stream: mathlib4

[Moritz Firsching]

@Eric Wieser suggested to discuss the following from the port of Data.Fin.Tuple.NatAntidiagonal
https://github.com/leanprover-community/mathlib4/pull/2170/files/b8e08c51d0dfce0856f1e5092db6811b9cdf68c9#r1100852830
simp_rw doesn't use the equation lemma properly and it is unclear why