Subgroup.toGroup instance

Stream: mathlib4

[Lingwei Peng (彭灵伟)]

The toGroup instance in Subgroup is defined as follows:

instance toGroup {G : Type*} [Group G] (H : Subgroup G) : Group H := fast_instance%
  Subtype.coe_injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl

Here, H is a Subgroup G, not a Type u, so why is Group H a valid instance? It seems like H can also be regarded as Type u.

[Ruben Van de Velde]

Indeed it can, using the CoeSort instance

[Patrick Massot]

You can read https://leanprover-community.github.io/mathematics_in_lean/C08_Groups_and_Rings.html#subgroups for more information about that.

[Lingwei Peng (彭灵伟)]

Ruben Van de Velde said:

Indeed it can, using the CoeSort instance

Are you saying that:
• The instance SetLike (Subgroup G) G allows Subgroup to be treated as a Set;
• The instance CoeSort (Set α) (Type u) enables a Set to be viewed as Type u;
• Therefore, H can also be regarded as Type u?

[Yaël Dillies]

Not quite, your middle step is wrong. Instead it's that we have an instance [SetLike A B] → CoeSort A (Type _). See docs#SetLike.instCoeSortType.

[Lingwei Peng (彭灵伟)]

Oh, now it makes complete sense. Thank you very much.