-- 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) ⟶
      Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (s : α) ↦ colimit (F s)) 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) :
      colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
        Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (s : α) ↦ colimit (F s)) 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)))
        (CategoryStruct.comp (Y := piObj.{u_3, v_1, u_1} fun (s : α) ↦ colimit (F s ⋙ Functor.obj (evaluation D C) d))
          (colimitPointwiseProductToProductColimit (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) d)
          (CategoryStruct.comp (Y := piObj.{u_3, v_1, u_1} fun (x : α) ↦ (colimit (F x)).obj 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))
            (Iso.inv (piObjIso (fun (x : α) ↦ colimit (F x)) d) :
              Quiver.Hom.{v_1, u_1} (V := C) (piObj.{u_3, v_1, u_1} fun (s : α) ↦ (colimit (F s)).obj d)
                (Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (x : α) ↦ colimit (F x)) d)))) :
      colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
        Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (x : α) ↦ colimit (F x)) d)
have simp : Eq (α :=
  colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
    Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (s : α) ↦ colimit (F s)) 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) :
    colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
      Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (s : α) ↦ colimit (F s)) d)
  (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)
      (Iso.inv (piObjIso (fun (x : α) ↦ colimit (F x)) d) :
        Quiver.Hom.{v_1, u_1} (V := C) (piObj.{u_3, v_1, u_1} fun (s : α) ↦ (colimit (F s)).obj d)
          (Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (x : α) ↦ colimit (F x)) d)) :
    colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d) ⟶
      Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (x : α) ↦ colimit (F x)) d)
Tactic: simp only [← Category.assoc]