-- Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u_1
I : α → Type u_2
inst_1 : (i : α) → Category.{v_1, u_2} (I i)
inst_2 : HasProductsOfShape.{u_1, u, v} α C
F : (i : α) → Functor.{v_1, v, u_2, u} (I i) C
c c' : (i : α) → Cocone (F i)
e : (i : α) → c i ≅ c' i
i : (i : α) → I i
h :
  ∀ (b : α),
    Eq.{v + 1} (α := piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶ (c' b).pt)
      (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
          (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
              (CategoryStruct.comp (Y :=
                  piObj.{u_1, v, u}
                    (Functor.obj
                      (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦
                        Functor.obj (Functor.const (I i)) (c i).pt)
                      i))
                  (Pi.map (NatTrans.app (NatTrans.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ (c i).ι) i))
                  (𝟙 (piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)) :
                piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
                  piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
              (Iso.hom (Pi.mapIso fun (i : α) ↦ (Cocone.forget (F i)).mapIso (e i)) :
                Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
                  (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)) :
            piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
              piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
          (Pi.π (fun (i : α) ↦ (c' i).pt) b : (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt) ⟶ (c' b).pt) :
        piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶ (c' b).pt)
      (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
          (CategoryStruct.comp (Y :=
              piObj.{u_1, v, u}
                (Functor.obj
                  (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ Functor.obj (Functor.const (I i)) (c' i).pt)
                  i))
              (Pi.map (NatTrans.app (NatTrans.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ (c' i).ι) i))
              (𝟙 (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)) :
            piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
              piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
          (Pi.π (fun (i : α) ↦ (c' i).pt) b : (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt) ⟶ (c' b).pt) :
        piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶ (c' b).pt)
⊢ Eq.{v + 1} (α :=
    piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
      piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
    (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
        (CategoryStruct.comp (Y :=
            piObj.{u_1, v, u}
              (Functor.obj
                (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ Functor.obj (Functor.const (I i)) (c i).pt)
                i))
            (Pi.map (NatTrans.app (NatTrans.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ (c i).ι) i))
            (𝟙 (piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)) :
          piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
            piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
        (Iso.hom (Pi.mapIso fun (i : α) ↦ (Cocone.forget (F i)).mapIso (e i)) :
          Quiver.Hom.{v, u} (V := C) (piObj.{u_1, v, u} fun (i : α) ↦ (c i).pt)
            (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)) :
      piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
        piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)
    (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u}
          (Functor.obj
            (Functor.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ Functor.obj (Functor.const (I i)) (c' i).pt) i))
        (Pi.map (NatTrans.app (NatTrans.pi (C := I) (D := fun (i : α) ↦ C) fun (i : α) ↦ (c' i).ι) i))
        (𝟙 (piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)) :
      piObj.{u_1, v, u} ((Functor.pi (C := I) (D := fun (i : α) ↦ C) F).obj i) ⟶
        piObj.{u_1, v, u} fun (i : α) ↦ (c' i).pt)

Tactic:
ext