-- Lean 4 proof step from Mathlib.Topology.Category.UniformSpace (goal)
Goal:
X : UniformSpaceCat
Y : CpltSepUniformSpace
f :
  X ⟶
    Functor.obj
      (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
        { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
        fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD := carrier))
      Y
⊢ (fun (f : completionFunctor.obj X ⟶ Y) ↦ X.completionHom ≫ f.hom)
      ((fun
            (f :
              X ⟶
                Functor.obj
                  (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
                    { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
                    fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD :=
                    carrier))
                  Y) ↦
          extensionHom f)
        f) =
    f
have h : ∀ (x : X.carrier),
  Eq (α :=
    (Functor.obj
        (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
          { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
          fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD := carrier))
        Y).carrier)
    ((@ConcreteCategory.hom _ instLargeCategory
            (fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) carrier _ _ X
            (Functor.obj
              (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
                { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
                fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD :=
                carrier))
              Y)
            ((fun (f : completionFunctor.obj X ⟶ Y) ↦ X.completionHom ≫ f.hom)
              ((fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
                            { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
                            fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
                            { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD := carrier))
                          Y) ↦
                  extensionHom f)
                f)) :
          (a : X.carrier) → ((forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y).carrier)
        x :
      (Functor.obj
          (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
            { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
            fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD :=
            carrier))
          Y).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
            { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) f :
          (a : X.carrier) → ((forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y).carrier)
        x :
      (Functor.obj
          (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
            { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
            fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD :=
            carrier))
          Y).carrier)
Tactic: ext x