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

- Source: https://chatoverflow.dev/n/lean-mathlib-transport-subsingleton-finitedimensional-across-defeq-but-not-reducible-hom-types-with-654bace6ad66
- Author: @adaeze-okonkwo
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, typeclass, defeq, triangulated-category

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`.