-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat (↑cR.pt : Type w)
φ : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N
hf :
  Eq (α :=
    (↑(Functor.obj
            (forget₂ (ModuleCat (↑cR.pt : Type w)) (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
              LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w)) (CC :=
              ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
              (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
            (ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM))) :
        Type w) →+
      (↑(Functor.obj
            (forget₂ (ModuleCat (↑cR.pt : Type w)) (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
              LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w)) (CC :=
              ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
              (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
            (ModuleCat.of (↑cR.pt : Type w) (↑N : Type w))) :
        Type w))
    (AddCommGrpCat.Hom.hom
      (CategoryTheory.Functor.map
        (forget₂ (ModuleCat (↑cR.pt : Type w)) (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
          LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w)) (CC :=
          ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        ((fun (ψ : M ⟶ (constFunctor cR).obj N) ↦
            (ModuleCat.ofHom
                {
                  toFun :=
                    (⇑((AddEquiv.symm (homEquiv' hcR hcM) :
                              (a : M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1)) →
                                ModuleColimit hcR hcM →+ N.1)
                            ((toPresheaf R).map ψ) :
                          ModuleColimit hcR hcM →+ N.1) :
                      (a : ModuleColimit hcR hcM) → N.1),
                  map_add' := ⋯, map_smul' := ⋯ } :
              Quiver.Hom (V := ModuleCat (↑cR.pt : Type w)) (ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM))
                (ModuleCat.of (↑cR.pt : Type w) (↑N : Type w))))
          ((fun (φ : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) ↦
              (homMk
                  ((homEquiv' hcR hcM :
                      (a : ModuleColimit hcR hcM →+ N.1) → M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1))
                    (AddCommGrpCat.Hom.hom
                      (CategoryTheory.Functor.map
                        (forget₂ (ModuleCat (↑cR.pt : Type w)) (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
                          LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w)
                            (↑x2 : Type w))
                          (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                          (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                        φ)))
                  ⋯ :
                M ⟶ (constFunctor cR).obj N))
            φ))))
    (AddCommGrpCat.Hom.hom
      (CategoryTheory.Functor.map
        (forget₂ (ModuleCat (↑cR.pt : Type w)) (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
          LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w)) (CC :=
          ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        φ))
⊢ Eq (α :=
    Functor.obj
        (forget₂ (ModuleCat (↑cR.pt : Type w)) (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
          LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w)) (CC :=
          ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        (ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM)) ⟶
      Functor.obj
        (forget₂ (ModuleCat (↑cR.pt : Type w)) (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
          LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w)) (CC :=
          ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
          (CD := AddCommGrpCat.carrier))
        (ModuleCat.of (↑cR.pt : Type w) (↑N : Type w)))
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat (↑cR.pt : Type w)) (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
        LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w)) (CC :=
        ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      ((fun (ψ : M ⟶ (constFunctor cR).obj N) ↦
          (ModuleCat.ofHom
              {
                toFun :=
                  (⇑((AddEquiv.symm (homEquiv' hcR hcM) :
                            (a : M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1)) →
                              ModuleColimit hcR hcM →+ N.1)
                          ((toPresheaf R).map ψ) :
                        ModuleColimit hcR hcM →+ N.1) :
                    (a : ModuleColimit hcR hcM) → N.1),
                map_add' := ⋯, map_smul' := ⋯ } :
            Quiver.Hom (V := ModuleCat (↑cR.pt : Type w)) (ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM))
              (ModuleCat.of (↑cR.pt : Type w) (↑N : Type w))))
        ((fun (φ : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) ↦
            (homMk
                ((homEquiv' hcR hcM :
                    (a : ModuleColimit hcR hcM →+ N.1) → M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1))
                  (AddCommGrpCat.Hom.hom
                    (CategoryTheory.Functor.map
                      (forget₂ (ModuleCat (↑cR.pt : Type w)) (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
                        LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w))
                        (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                        (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                      φ)))
                ⋯ :
              M ⟶ (constFunctor cR).obj N))
          φ)))
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat (↑cR.pt : Type w)) (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
        LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w)) (CC :=
        ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
        (CD := AddCommGrpCat.carrier))
      φ)

Tactic:
ext : 1