-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat R
e_2 :
  (↑(Functor.obj (𝟭 (TopModuleCat R)) X).toModuleCat : 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 v u))
⊢ 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 v u)) →
      (↑(Functor.obj (𝟭 (TopModuleCat R)) X).toModuleCat : Type (max u v)))
    (Function.comp (β :=
      (↑(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)) →₀
        R)
      (AddHom.toFun
        (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
          ((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)))
      fun
        (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 v u))) ↦
      Finsupp.single x 1)
    id
have h : ∀
  (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 v u))),
  Function.comp (β :=
      (↑(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)) →₀
        R)
      (AddHom.toFun
        (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
          ((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)))
      (fun
          (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 v u))) ↦
        Finsupp.single x 1)
      x =
    id x
Tactic: ext