-- 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 := 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)
have rw : 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: rw [Iso.eq_comp_inv]