to_additive type mismatch

Stream: mathlib4

[Jon Eugster]

In Algebra.BigOperators.Fin mathlib4#1848 I get the following error with to_additive:

@[simp, to_additive]
theorem prod_univ_two [CommMonoid β] (f : Fin 2 → β) : (∏ i, f i) = f 0 * f 1 := by
  simp [prod_univ_succ]
#align fin.prod_univ_two Fin.prod_univ_two

application type mismatch
  0
argument has type
  OfNat (Fin 2) 1
but function has type
  [self : OfNat (Fin 2) 0] → Fin 2

If I put the additive version in before the statement, it works fine
(theorem sum_univ_two [AddCommMonoid β] (f : Fin 2 → β) : (∑ i, f i) = f 0 + f 1 :=)

I believe it might be because 0 and 1should not be translated. I haven't kept up to date with to_additive, what's the thing to do here?

[Floris van Doorn]

to_additive has special support for numerals, and should not translate 1 to 0 in this case. I will investigate.

[Yury G. Kudryashov]

As a temporary workaround, you can use the Multiplicative trick: formulate the additive lemma and prove it by applying the multiplicative one to Multiplicative β.

[Floris van Doorn]

I found the error, and will open a PR shortly

[Floris van Doorn]

Fixed by !4#1861. It was a mistake introduced in the port of to_additive.

[Ruben Van de Velde]

(deleted)

[Jon Eugster]

Thanks!