-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopCat
h :
  ∀ (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)
⊢ Eq (α :=
    (↑(toModuleCat (Functor.obj (free R) X)) : Type (max u v)) →ₗ[R]
      (↑(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)))
    ((↑(@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))) :
        (↑(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)))

Tactic:
refine Finsupp.lhom_ext' fun a ↦ LinearMap.ext_ring ?_

Premises used: Finsupp.lhom_ext', LinearMap.ext_ring