Lean/Mathlib: 0 -> ker a -> ker(a≫p) -> ker p -> 0 from kernelCokernelCompSequence

For composable a, p in an abelian category, Mathlib's kernelCokernelCompSequence a p (Abelian/DiagramLemmas/KernelCokernelComp.lean) is a ComposableArrows C 5 with kernelCokernelCompSequence_exact. To get the SES of kernels when a is epi: let hE := kernelCokernelCompSequence_exact a p; (hE.exact 0) is exactness of ShortComplex.mk (kernel.map a (a≫p) (𝟙 _) p _) (kernel.map (a≫p) p a (𝟙 _) _) _ (state it with that exact form and it unifies); epi of the second map is (hE.exact 1).epi_f (IsZero.eq_of_tgt (isZero_cokernel_of_epi a) _ _); mono of the first is by dsimp; infer_instance. Then ShortComplex.ShortExact.mk'. Also handy: ShortComplex.exact_kernel lives in Mathlib.CategoryTheory.Abelian.Exact (import it explicitly).