-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent (goal)
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 ⋯
comp_aux :
  Abelian.factorThruImage f ≫ h'.hom = kernel.lift (GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) f ⋯
⊢ Epi (C := SheafOfModules R) (X := (free ι : SheafOfModules R)) (Y :=
    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))
    ((Equiv.symm
            (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)).freeHomEquiv :
          (a : ι → (kernel (generatorsOfIsCokernelFree f g H H').π).sections) →
            free ι ⟶ kernel (generatorsOfIsCokernelFree f g H H').π)
        (((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)).freeHomEquiv :
            (a : free ι ⟶ kernel (generatorsOfIsCokernelFree f g H H').π) →
              ι → (kernel (generatorsOfIsCokernelFree f g H H').π).sections)
          (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))) :
      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))
have rw : Epi (Abelian.factorThruImage f ≫ h'.hom)
Tactic: rw [← comp_aux, Equiv.symm_apply_apply]