-- Module: Mathlib.Topology.Category.UniformSpace
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
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)
⊢ (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

Tactic:
ext x