-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopCat
⊢ Eq (α :=
    (↑(toModuleCat (Functor.obj (free R) X)) : Type (max u v)) →L[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)) →L[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)) →L[R]
        (↑(toModuleCat (Functor.obj (free R) X)) : Type (max u v)))
have h : 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 := sorry },
                    naturality := sorry }
                  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 := 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)) },
                  naturality := sorry }
                (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: apply ContinuousLinearMap.coe_injective