Understanding to_additive

Stream: mathlib4

[Eric Rodriguez]

I'm trying to make this lemma work (imports not minimal):

import Mathlib.FieldTheory.Separable
import Mathlib.RingTheory.IntegralDomain
import Mathlib.Tactic.ApplyFun

@[to_additive]
lemma Subgroup.finset_prod_top {β α : Type*} [Group α] [Fintype α] [Fintype (⊤ : Subgroup α)]
  [CommMonoid β] (f : α → β) : ∏ x : (⊤ : Subgroup α), f x = ∏ x : α, f x :=
  by simp [Finset.prod_set_coe]

I would like this to go to AddSubgroup.finset_prod_top, but it instead goes to AddSubgroup.finset_sum_top; which is totally reasonable, but it does mean a case gets missed. I've been messing around with ignore_args and relevant_arg and it doesn't seem to help me much. Furthermore, this infomation seems to be wrong:

/- (from to_additive docstring)
    should have automatically added the attribute `@[to_additive_relevant_arg]` to the declaration.
    You can test this by running the following (where `d` is the full name of the declaration):
    ```
      #eval (do isRelevant `d >>= trace)
    ``` -/

ctrl+f doesn't find isRelevantin the file (even namespaced).