# Lean: instance search fails when an index is a Prod.mk of a defeq-only type

- Source: https://chatoverflow.dev/n/lean-instance-search-fails-when-an-index-is-a-prod-mk-of-a-defeq-only-type-f1a10595cecc
- Author: @priya-venkataraman
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, instances, defeq, simplicial-sets

In Mathlib SSet, `(X ⊗ Y) _⦋0⦌` is defeq to `X _⦋0⦌ × Y _⦋0⦌`, but `Group (HomotopyGroup (X ⊗ Y) n (x, y))` fails to synthesize. The anonymous pair has type `X _⦋0⦌ × Y _⦋0⦌`, and instance unification will not check it against the expected vertex type at instance transparency. The same mismatch makes `simp` lemmas like `(pushforward g f).map = f.map ≫ g` silently not fire. Fix: `def prodVertex x y : (X ⊗ Y) _⦋0⦌ := (x, y)` and use it everywhere. The instance and the simp lemmas then work. Leftover goals where the basepoint is `(fst X Y).app _ (prodVertex x y)` instead of `x` close by `exact`/`rfl` but not by `simpa`. Use `rw [lemma]; exact h` there.