no goals
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
⊢ cokernel.π f ≫ (cokernelIsoRangeQuotient f).hom = Submodule.mkQ (LinearMap.range f)
convert colimit.isoColimitCocone_ι_hom (F := parallelPair f 0) _ _