-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopModuleCat R
f : X ⟶ Y
h :
  ∀
    (a :
      (↑(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 v u))),
    Eq (α := (↑(Functor.obj (𝟭 (TopModuleCat R)) Y).toModuleCat : Type (max u v)))
      (((↑(hom (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)))
                  (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) ⋙
                        free R)
                      f ≫
                    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)) Y).toModuleCat : Type (max u v)) R
                                (↑Y.toModuleCat : Type (max u v)) :
                              (a :
                                  (↑Y.toModuleCat : Type (max u v)) →
                                    (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat : Type (max u v))) →
                                ((↑Y.toModuleCat : Type (max u v)) →₀ R) →ₗ[R]
                                  (↑((𝟭 (TopModuleCat R)).obj Y).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)
                                  Y)) :
                            Type (max u v)) →L[R]
                          (↑(Functor.obj (𝟭 (TopModuleCat R)) Y).toModuleCat : Type (max u v)) })) :
              (↑((forget₂ (TopModuleCat R) TopCat ⋙ free R).obj X).toModuleCat : Type (max u v)) →ₗ[R]
                (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat : Type (max u v))) ∘ₗ
            Finsupp.lsingle a :
          (a : R) → (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat : Type (max u v)))
        1)
      (((↑(hom (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)))
                  (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)) } ≫
                    CategoryTheory.Functor.map (𝟭 (TopModuleCat R)) f)) :
              (↑((forget₂ (TopModuleCat R) TopCat ⋙ free R).obj X).toModuleCat : Type (max u v)) →ₗ[R]
                (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat : Type (max u v))) ∘ₗ
            Finsupp.lsingle a :
          (a : R) → (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat : Type (max u v)))
        1)
⊢ (↑(hom (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)))
          (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) ⋙
                free R)
              f ≫
            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)) Y).toModuleCat : Type (max u v)) R
                        (↑Y.toModuleCat : Type (max u v)) :
                      (a :
                          (↑Y.toModuleCat : Type (max u v)) →
                            (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat : Type (max u v))) →
                        ((↑Y.toModuleCat : Type (max u v)) →₀ R) →ₗ[R]
                          (↑((𝟭 (TopModuleCat R)).obj Y).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)
                          Y)) :
                    Type (max u v)) →L[R]
                  (↑(Functor.obj (𝟭 (TopModuleCat R)) Y).toModuleCat : Type (max u v)) })) :
      (↑((forget₂ (TopModuleCat R) TopCat ⋙ free R).obj X).toModuleCat : Type (max u v)) →ₗ[R]
        (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat : Type (max u v))) =
    (↑(hom (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)))
          (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)) } ≫
            CategoryTheory.Functor.map (𝟭 (TopModuleCat R)) f)) :
      (↑((forget₂ (TopModuleCat R) TopCat ⋙ free R).obj X).toModuleCat : Type (max u v)) →ₗ[R]
        (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat : Type (max u v)))

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

Premises used: Finsupp.lhom_ext', LinearMap.ext_ring