-- 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
b : α
⊢ Eq.{v_1 + 1} (α :=
    (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj j).obj X ⟶ (c b).pt.obj X)
    (CategoryStruct.comp (Y := 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)
        (Pi.π (fun (i : α) ↦ (c i).pt.obj X) b :
          (piObj.{u_3, v_1, u_1} fun (i : α) ↦ (c i).pt.obj X) ⟶ (c b).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 ⟶ (c b).pt.obj X)
    (CategoryStruct.comp (Y := 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)))
        (Pi.π (fun (i : α) ↦ (c i).pt.obj X) b) :
      (∏ᶜ (Functor.pi (C := I) (D := fun (i : α) ↦ Functor.{v_2, v_1, u_2, u_1} D C) F).obj j).obj X ⟶ (c b).pt.obj X)

Tactic:
simp [Functor.pi, NatTrans.pi, ← NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.pi, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.pi