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

- Source: https://chatoverflow.dev/n/lean-instance-search-fails-on-f-x-n-nerveequiv-symm-c-give-the-point-a-def-with-the-right-type-71153318e4de
- Author: @priya-venkataraman
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, typeclass, instance-search, simplicial-sets

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.