GroupTheory.OrderOfElement !4#2279

Stream: mathlib4

[Johan Commelin]

There is one error left in this file, about a fintype instance that can't be found.

[Eric Rodriguez]

the fintype instance in Lean3 is docs#subtype.fintype, as coercing to sets is afaik defeq to taking the subtype of things in the set_like. For some reason Lean4 doesn't like this - do we have to make a SetLike.fintype?

[Eric Wieser]

I think the coercion function implied by docs4#SetLike is too opaque for typeclass search to see through

[Eric Wieser]

I think we had something similar with docs4#Sym2 which was no longer picking up default quotient instances

[Johan Commelin]

So, what is the solution?

[Eric Wieser]

For Sym2 we just copied across the instance with a porting note

[Eric Wieser]

Maybe make a mathlib4 issue too, since this will probably reoccur, and it gives us something to reference in the comment

[Johan Commelin]

Ok, I will add

-- Porting note: TODO the following instance should follow from a more general principle
@[to_additive]
noncomputable instance [Fintype G] : Fintype (Submonoid.powers x) :=
  inferInstanceAs $ Fintype {y // y ∈ Submonoid.powers x}

and create an issue.

[Eric Wieser]

Oh, I meant that you should add an instance in the same form as the instance it's finding there

[Eric Wieser]

What's the term it infers?

[Johan Commelin]

  (@Subtype.fintype G
    (fun y =>
      @Membership.mem G (@Submonoid G (@Monoid.toMulOneClass G (@LeftCancelMonoid.toMonoid G inst✝²)))
        (@SetLike.instMembership (@Submonoid G (@Monoid.toMulOneClass G (@LeftCancelMonoid.toMonoid G inst✝²))) G
          (@Submonoid.instSetLikeSubmonoid G (@Monoid.toMulOneClass G (@LeftCancelMonoid.toMonoid G inst✝²))))
        y (@Submonoid.powers G (@LeftCancelMonoid.toMonoid G inst✝²) x✝))
    (fun a => @decidablePowers G x✝ inst✝² a) inst✝)

[Eric Wieser]

Can you repeat the statement of docs4#Subtype.fintype but for SetLike?

[Eric Wieser]

(or if that doesn't work, for Submonoid)