-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_2 : HasSheafify J AddCommGrpCat
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_4 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ : Type u
M : SheafOfModules R
f : Quiver.Hom (V := SheafOfModules R) (free ι) (free σ)
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
h : cokernel f ≅ M := Iso.symm (H'.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0)))
h' : Abelian.image f ≅
  kernel (X := free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)))
    (GeneratingSections.π (generatorsOfIsCokernelFree f g H H') :
      free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)) ⟶ M) :=
  kernel.mapIso (cokernel.π f) (GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) (Iso.refl (free σ)) h ⋯
⊢ Eq (α :=
    Quiver.Hom (V := SheafOfModules R) (free ι)
      (free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections))))
    ((Abelian.factorThruImage f ≫ h'.hom) ≫ equalizer.ι (GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) 0 :
      Quiver.Hom (V := SheafOfModules R) (free ι)
        (free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections))))
    (CategoryStruct.comp (Y :=
        equalizer (X := free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)))
          (GeneratingSections.π (generatorsOfIsCokernelFree f g H H') :
            free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)) ⟶ M)
          (0 : free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)) ⟶ M))
        (kernel.lift (GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) f ⋯ :
          free ι ⟶
            kernel (X := free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)))
              (GeneratingSections.π (generatorsOfIsCokernelFree f g H H') :
                free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)) ⟶ M))
        (equalizer.ι (GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) 0 :
          equalizer (X := free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)))
              (GeneratingSections.π (generatorsOfIsCokernelFree f g H H') :
                free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)) ⟶ M)
              (0 : free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections)) ⟶ M) ⟶
            free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections))) :
      Quiver.Hom (V := SheafOfModules R) (free ι)
        (free (GeneratingSections.I (generatorsOfIsCokernelFree f g H H' : M.GeneratingSections))))

Tactic:
simp [h']