-- 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
r₁ r₂ : (↑cR.pt : Type w)
m : ModuleColimit hcR hcM
obtain :
  ∀ (U : Cᵒᵖ)
    (a₁ a₂ :
      (R ⋙ forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)).obj
        U)
    (x :
      (M.presheaf ⋙
            forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier)).obj
        U)
    (h :
      (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Cocone.tensor
                    (Functor.mapCocone
                      (forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                        RingCat.carrier))
                      cR)
                    (Cocone.tensor
                      (Functor.mapCocone
                        (forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                          RingCat.carrier))
                        cR)
                      (Functor.mapCocone
                        (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
                          (CC := AddCommGrpCat.carrier))
                        cM))))
                U) :
            (a :
                (fun (X : Type w) ↦ X)
                  ((R ⋙ forget RingCat ⊗ R ⋙ forget RingCat ⊗ M.presheaf ⋙ forget AddCommGrpCat).obj U)) →
              (fun (X : Type w) ↦ X)
                (((Functor.const Cᵒᵖ).obj
                      (((forget RingCat).mapCocone cR).tensor
                          (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).pt).obj
                  U))
          (a₁, a₂, x) =
        (r₁, r₂, m)),
    ∃ (U : Cᵒᵖ) (a₁ : (↑(R.obj U) : Type w)) (a₂ : (↑(R.obj U) : Type w)) (x : (↑(M.obj U) : Type w)),
      (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a₁ = r₁ ∧
        (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a₂ = r₂ ∧
          (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m
⊢ ∃ (U : Cᵒᵖ) (a₁ : (↑(R.obj U) : Type w)) (a₂ : (↑(R.obj U) : Type w)) (x : (↑(M.obj U) : Type w)),
    (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a₁ = r₁ ∧
      (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a₂ = r₂ ∧
        (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m

Tactic:
obtain ⟨U, ⟨a₁, a₂, x⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget RingCat) hcR).tensor
      ((isColimitOfPreserves (forget RingCat) hcR).tensor
        (isColimitOfPreserves (forget AddCommGrpCat) hcM))) ⟨r₁, r₂, m⟩

Premises used: CategoryTheory.Limits.IsColimit.tensor, Prod.mk, RingCat, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, AddCommGrpCat, CategoryTheory.forget, CategoryTheory.Limits.isColimitOfPreserves