-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
α : Type u_3
I : α → Type u_4
inst_2 : (i : α) → Category.{u_5, u_4} (I i)
inst_3 : HasLimitsOfShape.{u_3, u_3, v_1, u_1} (Discrete α) C
F : (i : α) → I i ⥤ Functor.{v_2, v_1, u_2, u_1} D C
inst_4 : ∀ (i : α), HasColimitsOfShape.{u_5, u_4, v_1, u_1} (I i) C
inst_5 : HasColimitsOfShape ((i : α) → I i) C
d : D
refine :
  ∀ (s : α) (k : (i : α) → I i),
    Eq (α := (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d).obj k ⟶ (colimit (F s)).obj d)
      (CategoryStruct.comp (Y := colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d))
          (colimit.ι (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) k :
            (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d).obj k ⟶
              colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d))
          (CategoryStruct.comp (Y := piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)
              (CategoryStruct.comp (Y := (colimit (pointwiseProduct (I := I) F)).obj d)
                    (Iso.inv (colimitObjIsoColimitCompEvaluation (pointwiseProduct (I := I) F) d) :
                      colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
                        (colimit (pointwiseProduct (I := I) F)).obj d)
                    (NatTrans.app (colimitPointwiseProductToProductColimit (I := I) F) d :
                      (colimit (pointwiseProduct (I := I) F)).obj d ⟶
                        Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (s : α) ↦ colimit (F s)) d) ≫
                  Iso.hom (piObjIso (fun (x : α) ↦ colimit (F x)) d) :
                colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
                  piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)
              (Pi.π (fun (x : α) ↦ (colimit (F x)).obj d) s :
                (piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d) ⟶ (colimit (F s)).obj d) :
            colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶ (colimit (F s)).obj d) :
        (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d).obj k ⟶ (colimit (F s)).obj d)
      (CategoryStruct.comp (Y := colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d))
          (colimit.ι (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) k)
          (CategoryStruct.comp (Y := piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)
            (CategoryStruct.comp (Y :=
                piObj.{u_3, v_1, u_1} fun (s : α) ↦ colimit (F s ⋙ Functor.obj (evaluation D C) d))
                (CategoryStruct.comp (Y :=
                    colimit (J := (i : α) → I i)
                      (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d))
                    (Iso.hom (HasColimit.isoOfNatIso (pointwiseProductCompEvaluation (I := I) F d)))
                    (colimitPointwiseProductToProductColimit (I := I) fun (s : α) ↦
                      F s ⋙ Functor.obj (evaluation D C) d) :
                  colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
                    piObj.{u_3, v_1, u_1} fun (s : α) ↦ colimit (F s ⋙ Functor.obj (evaluation D C) d))
                (Iso.hom (Pi.mapIso fun (x : α) ↦ Iso.symm (colimitObjIsoColimitCompEvaluation (F x) d)) :
                  Quiver.Hom.{v_1, u_1} (V := C)
                    (piObj.{u_3, v_1, u_1} fun (x : α) ↦ colimit (F x ⋙ Functor.obj (evaluation D C) d))
                    (piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)) :
              colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
                piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)
            (Pi.π (fun (x : α) ↦ (colimit (F x)).obj d) s :
              (piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d) ⟶ (colimit (F s)).obj d)) :
        (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d).obj k ⟶ (colimit (F s)).obj d)
⊢ Eq (α :=
    colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
      piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)
    (CategoryStruct.comp (Y := (colimit (pointwiseProduct (I := I) F)).obj d)
          (Iso.inv (colimitObjIsoColimitCompEvaluation (pointwiseProduct (I := I) F) d) :
            colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
              (colimit (pointwiseProduct (I := I) F)).obj d)
          (NatTrans.app (colimitPointwiseProductToProductColimit (I := I) F) d :
            (colimit (pointwiseProduct (I := I) F)).obj d ⟶
              Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (s : α) ↦ colimit (F s)) d) ≫
        Iso.hom (piObjIso (fun (x : α) ↦ colimit (F x)) d) :
      colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
        piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)
    (CategoryStruct.comp (Y := piObj.{u_3, v_1, u_1} fun (s : α) ↦ colimit (F s ⋙ Functor.obj (evaluation D C) d))
        (CategoryStruct.comp (Y :=
            colimit (J := (i : α) → I i) (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d))
            (Iso.hom (HasColimit.isoOfNatIso (pointwiseProductCompEvaluation (I := I) F d)))
            (colimitPointwiseProductToProductColimit (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d) :
          colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
            piObj.{u_3, v_1, u_1} fun (s : α) ↦ colimit (F s ⋙ Functor.obj (evaluation D C) d))
        (Iso.hom (Pi.mapIso fun (x : α) ↦ Iso.symm (colimitObjIsoColimitCompEvaluation (F x) d)) :
          Quiver.Hom.{v_1, u_1} (V := C)
            (piObj.{u_3, v_1, u_1} fun (x : α) ↦ colimit (F x ⋙ Functor.obj (evaluation D C) d))
            (piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)) :
      colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
        piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj d)

Tactic:
refine Pi.hom_ext _ _ (fun s => colimit.hom_ext (fun k => ?_))

Premises used: CategoryTheory.Limits.Pi.hom_ext, CategoryTheory.Limits.colimit.hom_ext