to_additive complains about equation lemmas

Stream: mathlib4

[Eric Wieser]

This code:

import Mathlib

/-- `Finset.univ.sum` with better defeq for `Fin`. -/
@[to_additive (attr := simp) "`Finset.univ.prod` with better defeq for `Fin`."]
def prod {α} [Mul α] [One α] : ∀ {m} (_ : Fin m → α), α
  | 0, _ => 1
  | 1, v => v 0
  | _ + 2, v => prod (fun i => v (Fin.castSucc i)) * v (Fin.last _)

produces "prod and sum do not generate the same number of equation lemmas.".

[Eric Wieser]

I assume that lazy generation of these equations is to blame?

[Eric Wieser]

Is there a workaround besides defining the function twice?

[Floris van Doorn]

I believe @Joachim Breitner tried to add support for match/equation compiler in #16026 here. Does the matcher info also affect the generated equational lemmas (which are generated here)?

[Joachim Breitner]

Yes, matcherinfo is relevant, as the equations are split according to the matches on the RHS, and without the MatcherInfo they are not recognized as such