GroupTheory.Index !4#2222

Stream: mathlib4

[Johan Commelin]

The only remaining errors seem to be about to_additive failing to translate a decl. I get errors like

application type mismatch
  Subgroup G
argument has type
  AddGroup G
but function has type
  [inst : Group G] → Type u_1

on statements like

@[to_additive (attr := simp)] -- ← error is here
theorem index_top : (⊤ : Subgroup G).index = 1 :=
  Cardinal.toNat_eq_one_iff_unique.mpr ⟨QuotientGroup.subsingleton_quotient_top, ⟨1⟩⟩

Not sure how to debug this.

[Ruben Van de Velde]

Can you try putting the type arguments that need translation first, if they aren't yet?

[Johan Commelin]

@index_top : ∀ {G : Type u_1} [inst : Group G], index ⊤ = 1

looks alright to me.

[Ruben Van de Velde]

Too bad, that was my only guess

[Eric Wieser]

Is it stuck if you replace the proof with sorry?

[Johan Commelin]

It is not

[Eric Wieser]

How much of the proof needs to be replaced with sorry for it to work?

[Eric Wieser]

Is docs4#QuotientGroup.subsingleton_quotient_top correctly additivized?

[Johan Commelin]

@[to_additive (attr := simp)]
theorem index_top : (⊤ : Subgroup G).index = 1 :=
  Cardinal.toNat_eq_one_iff_unique.mpr sorry

is broken

[Johan Commelin]

Eric Wieser said:

Is docs4#QuotientGroup.subsingleton_quotient_top correctly additivized?

Looks perfectly fine to me

[Thomas Browning]

Somehow replacing Cardinal.toNat_eq_one_iff_unique with Nat.card_eq_one_iff_unique fixes the issue, although there are some later issues in the file

[Thomas Browning]

I think I've fixed all the errors in the file, but this bug with these Cardinal lemmas is very perplexing