-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopCat
a : (↑X : Type (max v u))
⊢ Eq (α := (↑(toModuleCat (Functor.obj (free R) X)) : Type (max u v)))
    ((((↑(@hom _ (instCategory R)
                  (fun (x1 x2 : TopModuleCat R) ↦
                    (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v)))
                  (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v)))
                  (fun (X Y : TopModuleCat R) ↦
                    (ContinuousLinearMap.funLike :
                      FunLike ((↑X.toModuleCat : Type (max u v)) →L[R] (↑Y.toModuleCat : Type (max u v)))
                        (↑X.toModuleCat : Type (max u v)) (↑Y.toModuleCat : Type (max u v))))
                  _ _ _
                  (CategoryStruct.comp (Y :=
                      Functor.obj (free R)
                        (Functor.obj
                          (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))
                          (Functor.obj (free R) X)))
                      (CategoryTheory.Functor.map (free R)
                        (NatTrans.app
                          {
                            app := fun (X : TopCat) ↦
                              TopCat.ofHom
                                { toFun := fun (x : (↑X : Type (max u v))) ↦ Finsupp.single x 1,
                                  continuous_toFun := ⋯ },
                            naturality := ⋯ }
                          X))
                      (NatTrans.app
                        {
                          app := fun (X : TopModuleCat R) ↦
                            ConcreteCategory.ofHom (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)))
                              {
                                toLinearMap :=
                                  (Finsupp.lift (↑(Functor.obj (𝟭 (TopModuleCat R)) X).toModuleCat : Type (max u v)) R
                                        (↑X.toModuleCat : Type (max u v)) :
                                      (a :
                                          (↑X.toModuleCat : Type (max u v)) →
                                            (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat : Type (max u v))) →
                                        ((↑X.toModuleCat : Type (max u v)) →₀ R) →ₗ[R]
                                          (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat : Type (max u v)))
                                    id,
                                cont := ⋯ :
                                (↑(toModuleCat
                                        (Functor.obj
                                          (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) ⋙
                                            free R)
                                          X)) :
                                    Type (max u v)) →L[R]
                                  (↑(Functor.obj (𝟭 (TopModuleCat R)) X).toModuleCat : Type (max u v)) },
                          naturality := ⋯ }
                        (Functor.obj (free R) X)) :
                    Quiver.Hom (V := TopModuleCat R) (Functor.obj (free R) X) (Functor.obj (free R) X))) :
              (↑(toModuleCat (Functor.obj (free R) X)) : Type (max u v)) →ₗ[R]
                (↑(toModuleCat (Functor.obj (free R) X)) : Type (max u v))) :
            (↑(toModuleCat (Functor.obj (free R) X)) : Type (max u v)) →ₗ[R]
              (↑(toModuleCat (Functor.obj (free R) X)) : Type (max u v))) ∘ₗ
          (Finsupp.lsingle a : R →ₗ[R] (↑X : Type (max v u)) →₀ R) :
        (a : R) → (↑((free R).obj X).toModuleCat : Type (max u v)))
      1)
    (((↑(@hom _ (instCategory R)
                (fun (x1 x2 : TopModuleCat R) ↦
                  (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v)))
                (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v)))
                (fun (X Y : TopModuleCat R) ↦
                  (ContinuousLinearMap.funLike :
                    FunLike ((↑X.toModuleCat : Type (max u v)) →L[R] (↑Y.toModuleCat : Type (max u v)))
                      (↑X.toModuleCat : Type (max u v)) (↑Y.toModuleCat : Type (max u v))))
                _ _ _
                (𝟙 (Functor.obj (free R) X) :
                  Quiver.Hom (V := TopModuleCat R) (Functor.obj (free R) X) (Functor.obj (free R) X))) :
            (↑((free R).obj X).toModuleCat : Type (max u v)) →ₗ[R] (↑((free R).obj X).toModuleCat : Type (max u v))) ∘ₗ
          Finsupp.lsingle a :
        (a : R) → (↑((free R).obj X).toModuleCat : Type (max u v)))
      1)

Tactic:
simp [freeMap, freeObj]

Premises used: TopModuleCat.freeObj, TopModuleCat.freeMap