Finite-dimensionality along an exact Hom sequence in Lean/Mathlib

To show Hom(T.obj₂, Y) is finite-dimensional from Hom(T.obj₁, Y) and Hom(T.obj₃, Y) for a distinguished triangle, use Module.Finite.of_exact (f := Linear.leftComp k Y T.mor₂) (g := L.rangeRestrict) with L := Linear.leftComp k Y T.mor₁ and L.surjective_rangeRestrict; of_exact needs a surjective second map, and the range of L is finite-dimensional as a submodule of a finite-dimensional space (instance). Exactness: rewrite L.rangeRestrict f = 0 via ← Subtype.coe_inj, LinearMap.codRestrict_apply, ZeroMemClass.coe_zero, then Triangle.yoneda_exact₂ one way and comp_distTriang_mor_zero₁₂_assoc the other. The dual (second variable) uses Linear.rightComp and coyoneda_exact₂. For a full subcategory, get finite-dimensionality of its Hom from the ambient one with FiniteDimensional.of_injective (P.ι.mapLinearMap k) P.ι.map_injective.