-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
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''
m : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
m'' : ModuleColimit hcR hcM''
⊢ ∃ (U : Cᵒᵖ) (x : (↑(M.obj U) : Type w)) (x' : (↑(M'.obj U) : Type w)) (x'' : (↑(M''.obj U) : Type w)),
    (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m ∧
      (ιM : (a : (↑(M'.obj U) : Type w)) → ModuleColimit hcR hcM') x' = m' ∧
        (ιM : (a : (↑(M''.obj U) : Type w)) → ModuleColimit hcR hcM'') x'' = m''
have obtain : ∀ (U : Cᵒᵖ)
  (x :
    (M.presheaf ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.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)
  (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 AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
                      (CC := AddCommGrpCat.carrier))
                    cM)
                  (Cocone.tensor
                    (Functor.mapCocone
                      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
                        (CC := AddCommGrpCat.carrier))
                      cM')
                    (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)
                ((M.presheaf ⋙ forget AddCommGrpCat ⊗
                      M'.presheaf ⋙ forget AddCommGrpCat ⊗ M''.presheaf ⋙ forget AddCommGrpCat).obj
                  U)) →
            (fun (X : Type w) ↦ X)
              (((Functor.const Cᵒᵖ).obj
                    (((forget AddCommGrpCat).mapCocone cM).tensor
                        (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).pt).obj
                U))
        (x, x', x'') =
      (m, m', m'')),
  ∃ (U : Cᵒᵖ) (x : (↑(M.obj U) : Type w)) (x' : (↑(M'.obj U) : Type w)) (x'' : (↑(M''.obj U) : Type w)),
    (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m ∧
      (ιM : (a : (↑(M'.obj U) : Type w)) → ModuleColimit hcR hcM') x' = m' ∧
        (ιM : (a : (↑(M''.obj U) : Type w)) → ModuleColimit hcR hcM'') x'' = m''
Tactic: obtain ⟨U, ⟨x, x', x''⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
      ((isColimitOfPreserves (forget AddCommGrpCat) hcM').tensor
        (isColimitOfPreserves (forget AddCommGrpCat) hcM''))) ⟨m, m', m''⟩