Nonzero maps factor through a nonzero incoming component

theorem MagnitudeConjecture.FiniteTauMatrix.exists_nonzero_hom_rightMiddle {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) {X Y : Ind} (f : T.obj X ⟶ T.obj Y) (hf : f ≠ 0) (hn : ¬CategoryTheory.IsIso f) : ∃ (i : Fin (rightMiddleArity T Y)) (g : T.obj X ⟶ T.obj (rightMiddleLabel T Y i)), g ≠ 0

A nonzero nonisomorphism between selected indecomposables has a nonzero map to some occurrence in the target's incoming mesh.