-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g :
  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 : (completionFunctor.obj X').α),
    Eq (α := Y.α)
      ((↑(@ConcreteCategory.hom _ category
                (fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦ { f : x1.α → x2.α // UniformContinuous f }) α _ _
                (completionFunctor.obj X') Y
                ((Equiv.symm
                      { toFun := fun (f : completionFunctor.obj X' ⟶ Y) ↦ X'.completionHom ≫ f.hom,
                        invFun :=
                          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,
                        left_inv := ⋯, right_inv := ⋯ :
                        (completionFunctor.obj X' ⟶ Y) ≃
                          (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) } :
                    (a : X' ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y) → completionFunctor.obj X' ⟶ Y)
                  (f ≫ g))) :
            (completionFunctor.obj X').α → Y.α)
          x :
        Y.α)
      ((↑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
                { f : x1.α → x2.α // UniformContinuous f }) (CC := α) (Y := Y)
                (completionFunctor.map f ≫
                  (Equiv.symm
                        { toFun := fun (f : completionFunctor.obj X ⟶ Y) ↦ X.completionHom ≫ f.hom,
                          invFun :=
                            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,
                          left_inv := ⋯, right_inv := ⋯ :
                          (completionFunctor.obj X ⟶ Y) ≃
                            (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) } :
                      (a : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y) → completionFunctor.obj X ⟶ Y)
                    g)) :
            (completionFunctor.obj X').α → Y.α)
          x :
        Y.α)
⊢ Eq (α := completionFunctor.obj X' ⟶ Y)
    ((Equiv.symm
            { toFun := fun (f : completionFunctor.obj X' ⟶ Y) ↦ X'.completionHom ≫ f.hom,
              invFun :=
                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,
              left_inv := ⋯, right_inv := ⋯ } :
          (a : X' ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y) → completionFunctor.obj X' ⟶ Y)
        (f ≫ g) :
      completionFunctor.obj X' ⟶ Y)
    (completionFunctor.map f ≫
        (Equiv.symm
              { toFun := fun (f : completionFunctor.obj X ⟶ Y) ↦ X.completionHom ≫ f.hom,
                invFun :=
                  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,
                left_inv := ⋯, right_inv := ⋯ } :
            (a : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y) → completionFunctor.obj X ⟶ Y)
          g :
      completionFunctor.obj X' ⟶ Y)

Tactic:
ext x