Refactor Category of ProfiniteGrp and ContinuousMulEquiv

Stream: mathlib4

[Nailin Guan]

When proving the Category.Iso in #16992 (probably also needed in #16993), I found the following problem:
1: The category of ProfiniteGrp need refactoring using one-field morphisms as suggested by @Christian Merten , now in PR #20740.

[Nailin Guan]

2: ContinuousMulEquiv is missing API toContinuousMonoidHom because the coe [MonoidHomClass F A B] [ContinuousMapClass F A B] F to ContinuousMonoidHom A B, this would be continued on #20628

[Edward van de Meent]

Is it just me or is there a capital missing in ContinuousMulequiv?

[Nailin Guan]

Sorry that this is a typo only for here.

[Nailin Guan]

After this two refactor we are able to prove (forget ProfiniteGrp.{u}).ReflectsIsomorphisms in a straight forward way following what in Grp did. This done in #20764 and would clear a path for ContinuousMulequiv -> Category.Iso. The ugly proof in #16992 and #16993 would be fixed after this PR is merged.