-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat.Limit (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
X Y : (↑s.pt : Type v)
f : X ⟶ Y
⊢ (limitConeLift F s ≫ (limitCone F).π.app j).toFunctor.map f = eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯
have dsimp : (hom (FC := TypeCat.Fun)
        (limit.π
          (homDiagram (F := F)
            ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π :=
                        { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := sorry :
                          NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                      Cone (F ⋙ objects) }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              X)
            ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π :=
                        { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := sorry :
                          NatTrans (Functor.obj (Functor.const J) (↑s.pt : Type v)) (F ⋙ objects) } :
                      Cone (F ⋙ objects) }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              Y))
          j) :
      (a :
          limit
            (homDiagram
              ((hom
                    (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)
              ((hom
                    (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))) →
        (hom (limit.π (F ⋙ objects) j) : (a : limit (F ⋙ objects)) → objects.obj (F.obj j))
            ((hom
                  (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) ⟶
          (hom (limit.π (F ⋙ objects) j) : (a : limit (F ⋙ objects)) → objects.obj (F.obj j))
            ((hom
                  (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))
    (Types.Limit.mk
      (homDiagram (F := F)
        ((@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)
        ((@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))
      (fun (j : J) ↦ eqToHom sorry ≫ (s.π.app j).toFunctor.map f ≫ eqToHom sorry) sorry) =
  eqToHom sorry ≫ (s.π.app j).toFunctor.map f ≫ eqToHom sorry
Tactic: dsimp [limitConeLift]