-- 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
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)
have h : Eq (α := (↑Y.toModuleCat : Type (max u v)))
  (Finsupp.sum
    (Finsupp.mapDomain (⇑(Hom.hom f) : (a : (↑X.toModuleCat : Type (max u v))) → (↑Y.toModuleCat : Type (max u v)))
      (Finsupp.single a 1))
    fun (x : (↑Y.toModuleCat : Type (max u v))) (r : R) ↦ r • x)
  ((Hom.hom f : (a : (↑X.toModuleCat : Type (max u v))) → (↑Y.toModuleCat : Type (max u v)))
    (Finsupp.sum (Finsupp.single a 1) fun (x : (↑X.toModuleCat : Type (max u v))) (r : R) ↦ r • x))
Tactic: dsimp [freeObj, freeMap]