Simple quotients of indecomposable projectives

A nonzero morphism from a projective object with local endomorphism ring to a simple object kills every monic right almost-split subobject. This is the abstract form of the fact that every simple quotient of an indecomposable projective is its top.

theorem MagnitudeConjecture.CategoryTheory.rightAlmostSplit_comp_nonzero_to_simple_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {R P T : C} (r : R ⟶ P) [CategoryTheory.Mono r] [CategoryTheory.Projective P] [IsLocalRing (CategoryTheory.End P)] (hr : QuotientSubmoduleEquidistribution.IsRightAlmostSplit r) [CategoryTheory.Simple T] (p : P ⟶ T) (hp : p ≠ 0) : CategoryTheory.CategoryStruct.comp r p = 0

A nonzero map from an indecomposable projective to a simple object kills a monic right almost-split morphism into that projective.