-- 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
X : D
c : (i : α) → Cocone (F i)
j : (i : α) → I i
⊢ 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)
have 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)
Tactic: ext