-- 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
X : D
c : (i : α) → Cocone (F i)
j : (i : α) → I i
dsimp :
  Eq (α :=
    (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj j).obj X ⟶
      piObj.{u_3, v_1, u_1} fun (i : α) ↦ (c i).pt.obj X)
    (CategoryStruct.comp (Y := Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (i : α) ↦ (c i).pt) X)
        (NatTrans.app
              (Pi.map
                (NatTrans.app
                  (NatTrans.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) fun (i : α) ↦ (c i).ι) j))
              X ≫
            𝟙 (Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (i : α) ↦ (c i).pt) X) :
          (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj j).obj X ⟶
            Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (i : α) ↦ (c i).pt) X)
        (Iso.hom (piObjIso (fun (i : α) ↦ (c i).pt) X) :
          Quiver.Hom.{v_1, u_1} (V := C) (Functor.obj.{v_2, v_1, u_2, u_1} (∏ᶜ fun (i : α) ↦ (c i).pt) X)
            (piObj.{u_3, v_1, u_1} fun (i : α) ↦ (c i).pt.obj X)) :
      (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj j).obj X ⟶
        piObj.{u_3, v_1, u_1} fun (i : α) ↦ (c i).pt.obj X)
    (CategoryStruct.comp (Y :=
        piObj.{u_3, v_1, u_1}
          (Functor.obj (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) X)
            j))
        (Iso.hom (piObjIso ((Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj j) X) :
          (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj j).obj X ⟶
            piObj.{u_3, v_1, u_1}
              (Functor.obj
                (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) X) j))
        (CategoryStruct.comp (Y :=
            piObj.{u_3, v_1, u_1}
              (Functor.obj
                (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦
                  Functor.obj (Functor.const (I i)) ((c i).pt.obj X))
                j))
            (Pi.map
              (NatTrans.app
                (NatTrans.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦
                  Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) X) (c i)))
                j))
            (𝟙 (piObj.{u_3, v_1, u_1} fun (i : α) ↦ (c i).pt.obj X)) :
          Quiver.Hom.{v_1, u_1} (V := C)
            (piObj.{u_3, v_1, u_1}
              (Functor.obj
                (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) X) j))
            (piObj.{u_3, v_1, u_1} fun (i : α) ↦ (c i).pt.obj X)) :
      (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj j).obj X ⟶
        piObj.{u_3, v_1, u_1} fun (i : α) ↦ (c i).pt.obj X)
⊢ Eq (α :=
    (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X).obj j ⟶
      Cocone.pt (F := pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)
        (Functor.obj (C :=
            Cocone (J := (i : α) → I i) (C := C)
              (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) X))
            (Cocone.precompose (Iso.hom (pointwiseProductCompEvaluation (I := I) F X)))
            (coconePointwiseProduct (I := I) fun (i : α) ↦ Functor.mapCocone (Functor.obj (evaluation D C) X) (c i)) :
          Cocone (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)))
    (CategoryStruct.comp (Y :=
        Cocone.pt (F := pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)
          (Functor.mapCocone (Functor.obj (evaluation D C) X) (coconePointwiseProduct (I := I) c)))
        (NatTrans.app
            (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) X) (coconePointwiseProduct (I := I) c))) j :
          (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X).obj j ⟶
            Functor.obj
              (Functor.obj (Functor.const ((i : α) → I i))
                (Cocone.pt (F := pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)
                  (Functor.mapCocone (Functor.obj (evaluation D C) X) (coconePointwiseProduct (I := I) c))))
              j)
        (Iso.hom (piObjIso (fun (i : α) ↦ (c i).pt) X)) :
      (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X).obj j ⟶
        Cocone.pt (F := pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)
          (Functor.obj (C :=
              Cocone (J := (i : α) → I i) (C := C)
                (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) X))
              (Cocone.precompose (Iso.hom (pointwiseProductCompEvaluation (I := I) F X)))
              (coconePointwiseProduct (I := I) fun (i : α) ↦ Functor.mapCocone (Functor.obj (evaluation D C) X) (c i)) :
            Cocone (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)))
    (NatTrans.app
        (Cocone.ι
          (Functor.obj (C :=
            Cocone (J := (i : α) → I i) (C := C)
              (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) X))
            (Cocone.precompose (Iso.hom (pointwiseProductCompEvaluation (I := I) F X)))
            (coconePointwiseProduct (I := I) fun (i : α) ↦ Functor.mapCocone (Functor.obj (evaluation D C) X) (c i))))
        j :
      (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X).obj j ⟶
        Functor.obj
          (Functor.obj (Functor.const ((i : α) → I i))
            (Cocone.pt (F := pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)
              (Functor.obj (C :=
                  Cocone (J := (i : α) → I i) (C := C)
                    (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) X))
                  (Cocone.precompose (Iso.hom (pointwiseProductCompEvaluation (I := I) F X)))
                  (coconePointwiseProduct (I := I) fun (i : α) ↦
                    Functor.mapCocone (Functor.obj (evaluation D C) X) (c i)) :
                Cocone (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X))))
          j)

Tactic:
dsimp