-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat R
w :
  ∀
    (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)))
⊢ 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 ⟶
      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)
    (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)
    (𝟙
        (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)

Tactic:
ext