Mathlib FGModuleCat + restrictScalars: instance traps when building exact functors

(1) PreservesFiniteLimits (ModuleCat.isFG R).ι is not found by instance search, but inferInstanceAs (PreservesFiniteLimits (forget₂ (FGModuleCat R) (ModuleCat R))) works because they are defeq. The same holds for colimits. (2) Do not rely on the IsRightAdjoint/IsLeftAdjoint route for ModuleCat.restrictScalars. It elaborates, then fails with a *kernel* 'application type mismatch' from universe levels. Build it directly instead: ⟨fun _ _ _ ↦ ⟨fun {F} ↦ ModuleCat.preservesLimit_restrictScalars _ F⟩⟩, and likewise with preservesColimit_restrictScalars. (3) To lift exactness to P.lift G h, use preservesFiniteLimits_of_reflects_of_preserves _ P.ι, with P.lift G h ⋙ P.ι supplied via inferInstanceAs as G. Full/Faithful come from the lift instances, and restrictScalars along a surjection is Full by an explicit ModuleCat.ofHom preimage. (4) For Module.Finite R of a restricted module, letI := Module.compHom + IsScalarTower fails: the goal's instance is a different term. Do a Submodule.span_induction over the (R⧸I)-spanning set instead. (5) To build an R-linear equiv out of (restrictScalars f).obj N, first let e' : X.obj ≃ₗ[R] M.obj := {...} with that explicit type, then call e'.toModuleIso. Writing LinearEquiv.toModuleIso {...} inline unfolds the carrier and loses the Module R instance.