There is no GroupCat in Mathlib

[ctchou]

In section 6.2 there is the following paragraph:

It is sometimes useful to bundle the type together with the structure, and Mathlib also contains a definition of a GroupCat structure that is equivalent to the following:

structure Group₁Cat where
α : Type*
str : Group₁ α

The Mathlib version is found in Mathlib.Algebra.Category.GroupCat.Basic, and you can #check it if you add this to the imports at the beginning of the examples file.

But there is no GroupCat in Mathlib, nor does the path Mathlib.Algebra.Category.GroupCat.Basic exist in Mathlib.