-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
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 := ⋯ }) :
          (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 := ⋯ })
              (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:
simp [freeMap_map]

Premises used: TopModuleCat.freeMap_map