-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
m : S.pt ⟶ (limitCone.{v, u, w} F).pt
h : ∀ (j : J), m ≫ (limitCone.{v, u, w} F).π.app j = S.π.app j
a : (↑S.pt : Type (max u v))
⊢ Eq (α := (↑(limitCone.{v, u, w} F).pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            m :
          (a : (↑S.pt : Type (max u v))) → (↑(limitCone F).pt : Type (max u v)))
        a :
      (↑(limitCone.{v, u, w} F).pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (X := S.pt) (Y := (limitCone.{v, u, w} F).pt)
            (ofHom
              {
                toFun := fun (x : (↑S.1 : Type (max u v))) ↦
                  Subtype.mk (p := fun (x : (j : J) → (↑(F.obj j) : Type (max u v))) ↦
                    Membership.mem (γ := Set ((j : J) → (↑(F.obj j) : Type (max u v))))
                      {u : (j : J) → (↑(F.obj j) : Type (max u v)) |
                        ∀ {i j : J} (f : i ⟶ j),
                          (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦
                                  C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier) (F.map f) :
                                (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                              (u i) =
                            u j}
                      x)
                    (fun (x_1 : J) ↦
                      (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                            (CC := carrier) (S.π.app x_1) :
                          (a : (↑(((Functor.const J).obj S.pt).obj x_1) : Type (max u v))) →
                            (↑(F.obj x_1) : Type (max u v)))
                        x)
                    ⋯,
                continuous_toFun := ⋯ }) :
          (a : (↑S.pt : Type (max u v))) → (↑(limitCone F).pt : Type (max u v)))
        a :
      (↑(limitCone.{v, u, w} F).pt : Type (max u v)))
have w : Eq (α := (↑(limitCone.{v, u, w} F).pt : Type (max u v)))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
          m :
        (a : (↑S.pt : Type (max u v))) → (↑(limitCone F).pt : Type (max u v)))
      a :
    (↑(limitCone.{v, u, w} F).pt : Type (max u v)))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
          (X := S.pt) (Y := (limitCone.{v, u, w} F).pt)
          (ofHom
            {
              toFun := fun (x : (↑S.1 : Type (max u v))) ↦
                Subtype.mk (p := fun (x : (j : J) → (↑(F.obj j) : Type (max u v))) ↦
                  ∀ {i j : J} (f : i ⟶ j),
                    (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                            (CC := carrier) (F.map f) :
                          (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
                        (x i) =
                      x j)
                  (fun (x_1 : J) ↦
                    ((Hom.hom ((limitCone.{v, u, w} F).π.app x_1)).comp (Hom.hom m) :
                        (a : (↑S.pt : Type (max u v))) → (↑(F.obj x_1) : Type (max u v)))
                      x)
                  sorry,
              continuous_toFun := sorry }) :
        (a : (↑S.pt : Type (max u v))) → (↑(limitCone F).pt : Type (max u v)))
      a :
    (↑(limitCone.{v, u, w} F).pt : Type (max u v)))
Tactic: simp [← h]