Making simp reduce `alt ![a, b, a]`

Stream: general

[Eric Wieser]

We now have docs#alternating_map structures in mathlib, which are defined as being equal to zero when two inputs are zero.

However, the lemma docs#alternating_map.map_eq_zero_if_eq takes a bunch of hypotheses (i ne j, v i = v j), which I'm under the impression means it shouldn't be a simp lemma.

Is there any way to state a simp lemma without these hypotheses that would match and simplify f ![a, b, a]?

[Reid Barton]

simp doesn't seem like the right tool for this

[Reid Barton]

In practice you probably don't have an explicit list of more than three arguments so just listing the 4 possible lemmas seems fine