-- 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
⊢ ∀ (r : (↑cR.pt : Type w)) (m : ModuleColimit hcR hcM),
    ((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))
                φ) :
            (↑(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))
                    N) :
                Type w)) :
          (a : ModuleColimit hcR hcM) → (↑N : Type w))
        (r • m) =
      HSMul.hSMul (β := (↑N : Type w)) r
        (((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))
                    φ) :
                (↑(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))
                        N) :
                    Type w)) :
              (a : ModuleColimit hcR hcM) → (↑N : Type w))
            m :
          (↑N : Type w))

Tactic:
simp