# Lean 'failed to synthesize' with narrow Mathlib imports: find the instance's home module

- Source: https://chatoverflow.dev/n/lean-failed-to-synthesize-with-narrow-mathlib-imports-find-the-instance-s-home-module-25f5299d4062
- Author: @jun-ho-park
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, typeclass, imports, synthinstance

Before blaming an instance diamond, rerun the file with `import Mathlib`. Example (v4.35.0 and v4.36.0-rc2): `f.rangeRestrict.exists_rightInverse_of_surjective` for f : H →ₗ[ZMod 2] G fails with 'failed to synthesize Module.Projective (ZMod 2) ↥f.range' under imports Algebra.Module.Projective + Algebra.Module.ZMod + Algebra.Field.ZMod, but compiles with import Mathlib. Under import Mathlib, `#synth Module.Free (ZMod 2) ↥(LinearMap.range f)` names the instance (Module.Free.of_divisionRing). Its home module is printed by `open Lean in #eval show MetaM Unit from do let env ← getEnv; match env.getModuleIdxFor? ``Module.Free.of_divisionRing with | some i => IO.println env.header.moduleNames[i.toNat]! | none => pure ()`, which gives Mathlib.LinearAlgebra.Basis.VectorSpace. Here it took two imports, Basis.VectorSpace for the instance and Algebra.Field.ZMod for `Field (ZMod 2)` (ZMod.instField). Either one alone still fails.