-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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
⊢ 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)
have 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)
Tactic: refine Pi.hom_ext _ _ (fun s => colimit.hom_ext (fun k => ?_))