-- 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
h :
  ∀
    (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))
⊢ Eq (α :=
    (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)) U)
    ((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))
    ((↾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)

Tactic:
ext ⟨r, m⟩