-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : UniformSpaceCat
Y : CpltSepUniformSpace
x : X.carrier
val :
  X.carrier →
    (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
property : UniformContinuous val
⊢ 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)
                {
                  hom' :=
                    Subtype.mk (p :=
                      fun
                        (f :
                          X.carrier →
                            (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) ↦
                      UniformContinuous f) val property })) :
          (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 _ 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)
            {
              hom' :=
                Subtype.mk (p :=
                  fun
                    (f :
                      X.carrier →
                        (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) ↦
                  UniformContinuous f) val property :
              X.Hom
                (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.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:
@Completion.extension_coe _ _ _ _ _ (CpltSepUniformSpace.t0Space _)
              ‹_› _

Premises used: UniformSpace.Completion.coe', UniformSpace.Completion.extension_coe, SeparationQuotient.mk, UniformSpace.Completion.extension, AbstractCompletion.extend, ite