Kernels in a split-epic map of cokernel rows

This is the elementary abelian-category calculation behind the pullback diagram in Auslander--Reiten Proposition 2.4. If a map of cokernel rows has a split-epic middle component and a monic left composite, then the kernel of the induced endpoint map is the image of the kernel of the middle component.

theorem MagnitudeConjecture.CategoryTheory.isPullback_of_splitEpi_of_kernel_restriction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {E P D Q : C} (t : E ⟶ P) (b : E ⟶ D) (q : P ⟶ Q) (h : D ⟶ Q) [CategoryTheory.IsSplitEpi t] (hsq : CategoryTheory.CategoryStruct.comp b h = CategoryTheory.CategoryStruct.comp t q) (hk : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι t) b) ⋯)) : CategoryTheory.IsPullback t b q h

A commutative square whose top map is split epic is a pullback when the restriction of its left map to the top kernel is a kernel of the bottom map.

noncomputable def MagnitudeConjecture.CategoryTheory.kernelLimit_of_splitEpi_cokernel_rows {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {U E P D Q : C} (a : U ⟶ E) (t : E ⟶ P) (b : E ⟶ D) (q : P ⟶ Q) (h : D ⟶ Q) [CategoryTheory.IsSplitEpi t] [CategoryTheory.Epi b] [CategoryTheory.Epi q] [CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp a t)] (hab : CategoryTheory.CategoryStruct.comp a b = 0) (ha : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι a hab)) (hq : {W : C} → (r : P ⟶ W) → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp a t) r = 0 → { c : Q ⟶ W // CategoryTheory.CategoryStruct.comp q c = r }) (hsq : CategoryTheory.CategoryStruct.comp b h = CategoryTheory.CategoryStruct.comp t q) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι t) b) ⋯)

In a commutative map of cokernel rows with split-epic middle map, the kernel of the endpoint map is obtained by restricting the upper cokernel map to the kernel of the middle map.