Incorrect number of universe levels parameters

Stream: maths

[Thomas Browning]

The following lemma and def each throw the cryptic error message "incorrect number of universe levels parameters for 'quotient_add_group.quotient_ker_equiv_of_right_inverse', #2 expected, #1 provided"

Seems like this is an issue with to_additive, but I'm a bit puzzled.

import group_theory.quotient_group

--incorrect number of universe levels parameters for 'quotient_add_group.quotient_ker_equiv_of_right_inverse', #2 expected, #1 provided
@[to_additive] lemma subgroup.card_quotient_bot {G : Type*} [group G] [fintype G]
  [fintype (quotient_group.quotient (⊥ : subgroup G))] :
 (fintype.card (quotient_group.quotient (⊥ : subgroup G))) = fintype.card G :=
fintype.card_congr (quotient_group.quotient_bot.to_equiv)

--incorrect number of universe levels parameters for 'quotient_add_group.quotient_ker_equiv_of_right_inverse', #2 expected, #1 provided
@[to_additive] def subgroup.quotient_bot_equiv {G : Type*} [group G] :
 quotient_group.quotient (⊥ : subgroup G) ≃ G :=
quotient_group.quotient_bot.to_equiv

[Eric Wieser]

Try putting the {G : Type*} in a variables statement?

[Thomas Browning]

Eric Wieser said:

Try putting the {G : Type*} in a variables statement?

Doesn't seem to help

[Eric Wieser]

docs#quotient_add_group.quotient_ker_equiv_of_right_inverse, docs#quotient_group.quotient_ker_equiv_of_right_inverse for reference

[Eric Wieser]

I'm curious why it's even mentioning that definition

[Eric Wieser]

Does the additive version of docs#quotient_group.quotient_bot even exist? docs#quotient_add_group.quotient_bot seems missing

[Thomas Browning]

I presume so, since docs#quotient_group.quotient_bot is marked with to_additive

[Eric Wieser]

The to-additive name is nonsense

[Eric Wieser]

It's a copy-paste error

[Eric Wieser]

The error is about universes because it checks that first, but the lemma is just not related at all

[Thomas Browning]

Great, thanks for the help!