Factorization across an irreducible kernel

If an epimorphism has irreducible kernel, a morphism into its target which does not lift through the epimorphism must instead contain that epimorphism. This is the pullback argument used in Auslander--Reiten IV, Proposition 2.7.

theorem MagnitudeConjecture.CategoryTheory.exists_factor_thru_of_not_exists_lift_of_irreducible_kernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {A B D X : C} (g : A ⟶ B) [CategoryTheory.Mono g] (q : B ⟶ D) [CategoryTheory.Epi q] (hzero : CategoryTheory.CategoryStruct.comp g q = 0) (hgKernel : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι g hzero)) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism g) (h : X ⟶ D) (hnot : ¬∃ (l : X ⟶ B), CategoryTheory.CategoryStruct.comp l q = h) : ∃ (r : B ⟶ X), CategoryTheory.CategoryStruct.comp r h = q

Let g be the kernel of an epimorphism q. If g is irreducible, then every morphism into the target of q which does not lift through q admits q as a factor.