-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat.Limit (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
X Y : (↑s.1 : Type v)
f : X ⟶ Y
j j' : J
h : j ⟶ j'
⊢ Eq (α :=
    (fun (X : Type v) ↦ X)
      (Functor.obj
        (homDiagram (F := F)
          ((hom (FC := TypeCat.Fun)
                (limit.lift (F ⋙ objects)
                  { pt := (↑s.pt : Type v),
                    π :=
                      { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                    Cone (F ⋙ objects) }) :
              (a :
                  (fun (X : Type v) ↦ X)
                    { pt := (↑s.pt : Type v),
                        π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
            X)
          ((hom (FC := TypeCat.Fun)
                (limit.lift (F ⋙ objects)
                  { pt := (↑s.pt : Type v),
                    π :=
                      { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                    Cone (F ⋙ objects) }) :
              (a :
                  (fun (X : Type v) ↦ X)
                    { pt := (↑s.pt : Type v),
                        π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
            Y))
        j'))
    ((hom (FC := TypeCat.Fun)
            (Functor.map
              (homDiagram (F := F)
                ((hom (FC := TypeCat.Fun)
                      (limit.lift (F ⋙ objects)
                        { pt := (↑s.pt : Type v),
                          π :=
                            { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ :
                              NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                          Cone (F ⋙ objects) }) :
                    (a :
                        (fun (X : Type v) ↦ X)
                          { pt := (↑s.pt : Type v),
                              π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                      (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
                  X)
                ((hom (FC := TypeCat.Fun)
                      (limit.lift (F ⋙ objects)
                        { pt := (↑s.pt : Type v),
                          π :=
                            { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ :
                              NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                          Cone (F ⋙ objects) }) :
                    (a :
                        (fun (X : Type v) ↦ X)
                          { pt := (↑s.pt : Type v),
                              π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                      (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
                  Y))
              h) :
          (a :
              (fun (X : Type v) ↦ X)
                ((homDiagram
                      ((hom
                            (limit.lift (F ⋙ objects)
                              { pt := (↑s.pt : Type v),
                                π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                          (a :
                              (fun (X : Type v) ↦ X)
                                { pt := (↑s.pt : Type v),
                                    π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                            (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
                        X)
                      ((hom
                            (limit.lift (F ⋙ objects)
                              { pt := (↑s.pt : Type v),
                                π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                          (a :
                              (fun (X : Type v) ↦ X)
                                { pt := (↑s.pt : Type v),
                                    π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                            (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
                        Y)).obj
                  j)) →
            (fun (X : Type v) ↦ X)
              ((homDiagram
                    ((hom
                          (limit.lift (F ⋙ objects)
                            { pt := (↑s.pt : Type v),
                              π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                        (a :
                            (fun (X : Type v) ↦ X)
                              { pt := (↑s.pt : Type v),
                                  π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                          (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
                      X)
                    ((hom
                          (limit.lift (F ⋙ objects)
                            { pt := (↑s.pt : Type v),
                              π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                        (a :
                            (fun (X : Type v) ↦ X)
                              { pt := (↑s.pt : Type v),
                                  π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                          (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
                      Y)).obj
                j'))
        (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) :
      (fun (X : Type v) ↦ X)
        (Functor.obj
          (homDiagram (F := F)
            ((hom (FC := TypeCat.Fun)
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π :=
                        { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ :
                          NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                      Cone (F ⋙ objects) }) :
                (a :
                    (fun (X : Type v) ↦ X)
                      { pt := (↑s.pt : Type v),
                          π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                  (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
              X)
            ((hom (FC := TypeCat.Fun)
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π :=
                        { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ :
                          NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                      Cone (F ⋙ objects) }) :
                (a :
                    (fun (X : Type v) ↦ X)
                      { pt := (↑s.pt : Type v),
                          π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                  (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
              Y))
          j'))
    (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯ :
      Quiver.Hom (V := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j'))
        ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') :
              (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j'))
            ((hom (FC := TypeCat.Fun)
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π :=
                        { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ :
                          NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                      Cone (F ⋙ objects) }) :
                (a :
                    (fun (X : Type v) ↦ X)
                      { pt := (↑s.pt : Type v),
                          π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                  (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
              X) :
          (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j'))
        ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') :
              (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j'))
            ((hom (FC := TypeCat.Fun)
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π :=
                        { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ :
                          NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                      Cone (F ⋙ objects) }) :
                (a :
                    (fun (X : Type v) ↦ X)
                      { pt := (↑s.pt : Type v),
                          π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }.pt) →
                  (fun (X : Type v) ↦ X) (limit (F ⋙ objects)))
              Y) :
          (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j')))
have h₁ : Eq (α :=
  Quiver.Hom (V := objects.obj (F.obj j'))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
        ((@hom _ types TypeCat.Fun _ _ _ _ _
                (limit.lift (F ⋙ objects)
                  { pt := (↑s.pt : Type v),
                    π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := sorry } }) :
              (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
            X :
          limit (F ⋙ objects)) :
      objects.obj (F.obj j'))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
        ((@hom _ types TypeCat.Fun _ _ _ _ _
                (limit.lift (F ⋙ objects)
                  { pt := (↑s.pt : Type v),
                    π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := sorry } }) :
              (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
            Y :
          limit (F ⋙ objects)) :
      objects.obj (F.obj j')))
  (eqToHom sorry ≫ (F.map h).toFunctor.map (eqToHom sorry ≫ (s.π.app j).toFunctor.map f ≫ eqToHom sorry) ≫ eqToHom sorry)
  (eqToHom sorry ≫ (s.π.app j').toFunctor.map f ≫ eqToHom sorry)
Tactic: dsimp [Functor.comp_obj, homDiagram_obj]