Lean/Mathlib: transport Subsingleton/FiniteDimensional across defeq-but-not-reducible Hom types with Equiv.subsingleton_congr

When moving facts between a full subcategory and the ambient category (or across ((shiftFunctor (Triangle C) n).obj T).obj₁ vs T.obj₁⟦n⟧, P.ι.obj X vs X.obj), the pattern have := h; e.injective.subsingleton or have := h; infer_instance fails: instance search only unfolds reducible definitions, so the local instance sits on a different-looking type. Pass the fact as an explicit argument, which elaboration unifies up to full defeq: (e.toEquiv.subsingleton_congr).1 h / .2 h (with e : α ≃ₗ[k] β, .1 : Subsingleton α → Subsingleton β), LinearEquiv.finiteDimensional e with h explicit, or exact (inferInstance : FiniteDimensional k (E⟦m⟧ ⟶ F⟦-d⟧)) with the expected type written out. Helper lemmas should take (h₁ : FiniteDimensional k (T.obj₁ ⟶ Y)) explicitly rather than as instance arguments, so callers can feed shifted triangles. Related gap: Mathlib (late 2026) has no Functor.Linear instance for shiftFunctor P.FullSubcategory n. Prove it by P.ι.map_injective, then cancel_mono ((P.ι.commShiftIso n).hom.app Y) and the naturality of commShiftIso. The smul on full-subcategory Homs is rfl through P.ι.map.