-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat R
x :
  (↑(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))
        X) :
    Type (max u v))
⊢ Eq (α :=
    (↑(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))
          X) :
      Type (max u v)))
    (((@hom _ TopCat.instCategory (fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) TopCat.carrier
              (fun (X Y : TopCat) ↦
                (ContinuousMap.instFunLike :
                  FunLike C((↑X : Type (max u v)), (↑Y : Type (max u v))) (↑X : Type (max u v)) (↑Y : Type (max u v))))
              _ _ _
              (CategoryStruct.comp (Y :=
                  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)
                      (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))
                        X)))
                  (NatTrans.app
                    {
                      app := fun (X : TopCat) ↦
                        TopCat.ofHom
                          { toFun := fun (x : (↑X : Type (max u v))) ↦ Finsupp.single x 1, continuous_toFun := ⋯ },
                      naturality := ⋯ }
                    (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))
                      X))
                  (CategoryTheory.Functor.map
                    (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))
                    (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 := ⋯ }
                      X)) :
                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))
                    X ⟶
                  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))
                    X) :
            C((↑(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))
                    X) :
                Type (max u v)),
              (↑(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))
                    X) :
                Type (max u v)))) :
          (a : (↑((forget₂ (TopModuleCat R) TopCat).obj X) : Type (max u v))) →
            (↑((forget₂ (TopModuleCat R) TopCat).obj X) : Type (max u v)))
        x :
      (↑(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))
            X) :
        Type (max u v)))
    ((@hom _ TopCat.instCategory (fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) TopCat.carrier
            (fun (X Y : TopCat) ↦
              (ContinuousMap.instFunLike :
                FunLike C((↑X : Type (max u v)), (↑Y : Type (max u v))) (↑X : Type (max u v)) (↑Y : Type (max u v))))
            _ _ _
            (𝟙
                (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))
                  X) :
              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))
                  X ⟶
                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))
                  X) :
          (a : (↑((forget₂ (TopModuleCat R) TopCat).obj X) : Type (max u v))) →
            (↑((forget₂ (TopModuleCat R) TopCat).obj X) : Type (max u v)))
        x :
      (↑(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))
            X) :
        Type (max u v)))

Tactic:
simp [freeObj]

Premises used: TopModuleCat.freeObj