-- 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
rw :
  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)
⊢ Eq (α :=
    (colimit (pointwiseProduct (I := I) F)).obj d ⟶ Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (s : α) ↦ colimit (F s)) 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)
    (CategoryStruct.comp (Y := colimit (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) d))
        (Iso.hom (colimitObjIsoColimitCompEvaluation (pointwiseProduct (I := I) F) d) :
          (colimit (pointwiseProduct (I := I) F)).obj d ⟶
            colimit (pointwiseProduct (I := I) F ⋙ 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)))
            (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) :
      (colimit (pointwiseProduct (I := I) F)).obj d ⟶
        Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (x : α) ↦ colimit (F x)) d)

Tactic:
rw [← Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq