-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct (goal)
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
⊢ 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)
have 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)
Tactic: ext