-- 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 (α :=
    (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X).obj j ⟶
      Cocone.pt (F := pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)
        (Functor.obj (C :=
            Cocone (J := (i : α) → I i) (C := C)
              (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) X))
            (Cocone.precompose (Iso.hom (pointwiseProductCompEvaluation (I := I) F X)))
            (coconePointwiseProduct (I := I) fun (i : α) ↦ Functor.mapCocone (Functor.obj (evaluation D C) X) (c i)) :
          Cocone (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)))
    (CategoryStruct.comp (Y :=
        Cocone.pt (F := pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)
          (Functor.mapCocone (Functor.obj (evaluation D C) X) (coconePointwiseProduct (I := I) c)))
        (NatTrans.app
            (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation D C) X) (coconePointwiseProduct (I := I) c))) j :
          (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X).obj j ⟶
            Functor.obj
              (Functor.obj (Functor.const ((i : α) → I i))
                (Cocone.pt (F := pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)
                  (Functor.mapCocone (Functor.obj (evaluation D C) X) (coconePointwiseProduct (I := I) c))))
              j)
        (Iso.hom (piObjIso (fun (i : α) ↦ (c i).pt) X)) :
      (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X).obj j ⟶
        Cocone.pt (F := pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)
          (Functor.obj (C :=
              Cocone (J := (i : α) → I i) (C := C)
                (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) X))
              (Cocone.precompose (Iso.hom (pointwiseProductCompEvaluation (I := I) F X)))
              (coconePointwiseProduct (I := I) fun (i : α) ↦ Functor.mapCocone (Functor.obj (evaluation D C) X) (c i)) :
            Cocone (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)))
    (NatTrans.app
        (Cocone.ι
          (Functor.obj (C :=
            Cocone (J := (i : α) → I i) (C := C)
              (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) X))
            (Cocone.precompose (Iso.hom (pointwiseProductCompEvaluation (I := I) F X)))
            (coconePointwiseProduct (I := I) fun (i : α) ↦ Functor.mapCocone (Functor.obj (evaluation D C) X) (c i))))
        j :
      (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X).obj j ⟶
        Functor.obj
          (Functor.obj (Functor.const ((i : α) → I i))
            (Cocone.pt (F := pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X)
              (Functor.obj (C :=
                  Cocone (J := (i : α) → I i) (C := C)
                    (pointwiseProduct (I := I) fun (s : α) ↦ F s ⋙ Functor.obj (evaluation D C) X))
                  (Cocone.precompose (Iso.hom (pointwiseProductCompEvaluation (I := I) F X)))
                  (coconePointwiseProduct (I := I) fun (i : α) ↦
                    Functor.mapCocone (Functor.obj (evaluation D C) X) (c i)) :
                Cocone (pointwiseProduct (I := I) F ⋙ Functor.obj (evaluation D C) X))))
          j)
have dsimp : 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: dsimp