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

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.