HomologicalComplex.imageToKernel_as_boundariesToCycles'

theorem HomologicalComplex.imageToKernel_as_boundariesToCycles' : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [inst_2 : CategoryTheory.Limits.HasKernels V] [inst_3 : CategoryTheory.Limits.HasImages V] (C : HomologicalComplex V c) (i : ι) (h : C.boundaries i ≤ C.cycles' i), (C.boundaries i).ofLE (C.cycles' i) h = C.boundariesToCycles' i

This theorem, `HomologicalComplex.imageToKernel_as_boundariesToCycles'`, states that for any homological complex `C` of a certain category with zero morphisms and kernels, given an index `i` and a proof `h` that the boundaries at index `i` are less than or equal to the cycles' at index `i`, the morphism from the boundaries to the cycles' at the given index `i` is equal to the morphism obtained by applying the `ofLE` function (which constructs a morphism from a proof of the inequality between two subobjects) to the boundaries and the cycles'.

More concisely: For a homological complex `C` with zero morphisms and kernels, the morphism from boundaries to cycles at index `i` is equal to the application of `ofLE` to the proof that boundaries are less than or equal to cycles at index `i`.