-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (𝟭 TopCat) X ⟶
      Functor.obj
        (free R ⋙
          forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
            C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
        Y)
    (CategoryTheory.Functor.map (𝟭 TopCat) f ≫
      TopCat.ofHom { toFun := fun (x : (↑Y : Type (max u v))) ↦ Finsupp.single x 1, continuous_toFun := ⋯ })
    (CategoryStruct.comp (Y :=
      Functor.obj
        (free R ⋙
          forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
            C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
        X)
      (TopCat.ofHom { toFun := fun (x : (↑X : Type (max u v))) ↦ Finsupp.single x 1, continuous_toFun := ⋯ })
      (CategoryTheory.Functor.map
        (free R ⋙
          forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
            C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
        f))
have w : ∀ (x : (↑(Functor.obj (𝟭 TopCat) X) : Type (max u v))),
  Eq (α :=
    (↑(Functor.obj
          (free R ⋙
            forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
              (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
              fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
              C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
          Y) :
      Type (max u v)))
    ((hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := TopCat.carrier) (X :=
            Functor.obj (𝟭 TopCat) X) (Y :=
            Functor.obj
              (free R ⋙
                forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
                  (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
                  fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
                  C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
              Y)
            (CategoryTheory.Functor.map (𝟭 TopCat) f ≫
              TopCat.ofHom { toFun := fun (x : (↑Y : Type (max u v))) ↦ Finsupp.single x 1, continuous_toFun := sorry }) :
          (a : (↑((𝟭 TopCat).obj X) : Type (max u v))) →
            (↑((free R ⋙ forget₂ (TopModuleCat R) TopCat).obj Y) : Type (max u v)))
        x :
      (↑(Functor.obj
            (free R ⋙
              forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
                (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
                fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
                C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
            Y) :
        Type (max u v)))
    ((hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := TopCat.carrier) (X :=
            Functor.obj (𝟭 TopCat) X) (Y :=
            Functor.obj
              (free R ⋙
                forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
                  (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
                  fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
                  C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
              Y)
            (CategoryStruct.comp (Y :=
              Functor.obj
                (free R ⋙
                  forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
                    (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
                    fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
                    C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
                X)
              (TopCat.ofHom { toFun := fun (x : (↑X : Type (max u v))) ↦ Finsupp.single x 1, continuous_toFun := sorry })
              (CategoryTheory.Functor.map
                (free R ⋙
                  forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
                    (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
                    fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
                    C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
                f)) :
          (a : (↑((𝟭 TopCat).obj X) : Type (max u v))) →
            (↑((free R ⋙ forget₂ (TopModuleCat R) TopCat).obj Y) : Type (max u v)))
        x :
      (↑(Functor.obj
            (free R ⋙
              forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
                (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
                fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
                C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
            Y) :
        Type (max u v)))
Tactic: ext x