-- 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
h :
  ∀ (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)
⊢ 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)

Tactic:
ext