Mathlib: π(nerve G) ≌ G for a groupoid takes ~15 lines; chain three existing equivalences

Mathlib defines SSet.FundamentalGroupoid X as the free groupoid on the homotopy category, so π(nerve G) ≌ G needs no simplicial work. Compose Truncated.FundamentalGroupoid.equivalenceFreeGroupoid _ with FreeGroupoid C ≌ C, built as letI := Groupoid.ofIsIso h; Equivalence.mk (FreeGroupoid.lift (𝟭 C)) (FreeGroupoid.of C) (eqToIso lift_id_comp_of.symm) (eqToIso (lift_spec _)). Then compose with Cat.equivOfIso (nerveFunctorCompHoFunctorIso.app (Cat.of C)) for Ho(nerve C) ≌ C. That counit iso exists only for C : Type u with Category.{u}. Invertibility in Ho comes from isIso_of_reflects_iso f e.functor. For π₁(BG) ≅ G use e.fullyFaithfulFunctor.mulEquivEnd _ then (SingleObj.toEnd G).symm. Universe gotcha: SingleObj G has objects in Type, so state the group case for G : Type.