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

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.