-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → Quiver.Hom.{?u.292990, max u (?u.292990 + 1)} M (X i).toModuleCat
J : Type u_2
inst_2 : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat.{u_3, u} R
c :
  Cone
    (F ⋙
      forget₂ (TopModuleCat.{u_3, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
        (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC := fun (X : TopModuleCat.{u_3, u} R) ↦
        (↑X.toModuleCat : Type u_3)) (ModuleCat.{u_3, u} R) (FD := fun (x1 x2 : ModuleCat.{u_3, u} R) ↦
        (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3)) (CD := ModuleCat.carrier))
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (ofCone c).pt
H : ∀ (j : J), m ≫ (ofCone c).π.app j = s.π.app j
⊢ m =
    ofHom
      {
        toLinearMap :=
          ModuleCat.Hom.hom
            (hc.lift
              (Functor.mapCone
                (forget₂ (TopModuleCat.{u_3, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
                  (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC :=
                  fun (X : TopModuleCat.{u_3, u} R) ↦ (↑X.toModuleCat : Type u_3)) (ModuleCat.{u_3, u} R) (FD :=
                  fun (x1 x2 : ModuleCat.{u_3, u} R) ↦ (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3)) (CD :=
                  ModuleCat.carrier))
                s)),
        cont := ⋯ }
have h : ∀ (x : (↑s.pt.toModuleCat : Type u_3)),
  Eq (α := (↑(ofCone c).pt.toModuleCat : Type u_3))
    ((hom (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
            (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC := fun (X : TopModuleCat.{u_3, u} R) ↦
            (↑X.toModuleCat : Type u_3)) m :
          (a : (↑s.pt.toModuleCat : Type u_3)) → (↑(ofCone c).pt.toModuleCat : Type u_3))
        x :
      (↑(ofCone c).pt.toModuleCat : Type u_3))
    (((hom (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
              (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC :=
              fun (X : TopModuleCat.{u_3, u} R) ↦ (↑X.toModuleCat : Type u_3)) (X := s.pt) (Y := (ofCone c).pt)
              (ofHom
                  {
                    toLinearMap :=
                      ModuleCat.Hom.hom
                        (hc.lift
                          (Functor.mapCone
                            (forget₂ (TopModuleCat.{u_3, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
                              (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC :=
                              fun (X : TopModuleCat.{u_3, u} R) ↦ (↑X.toModuleCat : Type u_3)) (ModuleCat.{u_3, u} R)
                              (FD := fun (x1 x2 : ModuleCat.{u_3, u} R) ↦ (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3))
                              (CD := ModuleCat.carrier))
                            s)),
                    cont := sorry } :
                Quiver.Hom (V := TopModuleCat.{u_3, u} R) (of R (↑s.1.1 : Type u_3))
                  (of R (↑(ofCone c).pt.toModuleCat : Type u_3))) :
            (↑s.pt.toModuleCat : Type u_3) →L[R] (↑(ofCone c).pt.toModuleCat : Type u_3)) :
          (a : (↑s.pt.toModuleCat : Type u_3)) → (↑(ofCone c).pt.toModuleCat : Type u_3))
        x :
      (↑(ofCone c).pt.toModuleCat : Type u_3))
Tactic: ext x