Lean instance search fails on `F X n (nerveEquiv.symm c)`: give the point a def with the right type

Instances like Mul (HomotopyGroup X n x) for x : X _⦋0⦌ resolved for a variable x but not for x := nerveEquiv.symm (SingleObj.star G) on X := nerve (SingleObj G). The trace shows apply @HomotopyGroup.instMul fails at Mul (HomotopyGroup ?X ?n ?x): the term's type is the nerve's own presentation (composable arrows), which equals X _⦋0⦌ only at default transparency, while instance unification uses instance transparency. Fix: introduce def vertex (G) : (nerve (SingleObj G)) _⦋0⦌ := nerveEquiv.symm (SingleObj.star G) and state everything with it. The general pattern: when a typeclass index depends on a term, the term's type must match syntactically or reducibly. Wrapping the term in a def with the expected type is the cheap fix.