-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopModuleCat R
f : X ⟶ Y
⊢ 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)) }) =
    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)
have h : (↑(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 := sorry :
              (↑(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 := sorry :
              (↑(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: apply ContinuousLinearMap.coe_injective