-- 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''
V U : Cᵒᵖ
f : V ⟶ U
r : (R ⋙ forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)).obj V
m :
  (M.presheaf ⋙
        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier)).obj
    V
⊢ Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) U)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((tensorObj (𝒞 := Functor.category)
                (R ⋙
                  forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                    RingCat.carrier))
                (M.presheaf ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                    AddCommGrpCat.carrier))).map
            f ≫
          ↾fun
              (x :
                (tensorObj (𝒞 := Functor.category)
                      (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                          RingCat.carrier))
                      (M.presheaf ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                          AddCommGrpCat.carrier))).obj
                  U) ↦
            match (motive :=
              (tensorObj (𝒞 := Functor.category)
                      (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                          RingCat.carrier))
                      (M.presheaf ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                          AddCommGrpCat.carrier))).obj
                  U →
                Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) U)
              x with
            | (r, m) =>
              (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                    AddCommGrpCat.carrier) (cM.ι.app U) :
                  (a : (↑(M.presheaf.obj U) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cM.pt).obj U) : Type w))
                (r • m)))
      (r, m))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun
              (x :
                (tensorObj (𝒞 := Functor.category)
                      (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                          RingCat.carrier))
                      (M.presheaf ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                          AddCommGrpCat.carrier))).obj
                  V) ↦
            match (motive :=
              (tensorObj (𝒞 := Functor.category)
                      (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                          RingCat.carrier))
                      (M.presheaf ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                          AddCommGrpCat.carrier))).obj
                  V →
                Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) V)
              x with
            | (r, m) =>
              (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                    AddCommGrpCat.carrier) (cM.ι.app V) :
                  (a : (↑(M.presheaf.obj V) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cM.pt).obj V) : Type w))
                (r • m)) ≫
          CategoryTheory.Functor.map (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) f))
      (r, m))

Tactic:
exact (ConcreteCategory.congr_arg (cM.ι.app U)
      (M.map_smul f r m).symm).trans (ConcreteCategory.congr_hom (cM.w f) _)

Premises used: CategoryTheory.ConcreteCategory.congr_arg, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.Cocone.w, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.NatTrans.app, Eq.trans