-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X : TopCat
Y : CompHaus
f : (↑X : Type u) → (↑(compHausToTop.obj Y) : Type u)
hf : Continuous f
w :
  ∀ (x : (↑(TopCat.of (↑X : Type u)) : Type u)),
    Eq (α := (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
      ((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
              TopCat.carrier _ _ (TopCat.of (↑X : Type u)) (TopCat.of (↑Y.1 : Type u))
              ((fun (f : stoneCechObj X ⟶ Y) ↦
                  TopCat.ofHom
                    {
                      toFun :=
                        Function.comp (β :=
                          (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
                            (stoneCechObj X))
                          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                                C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                                  (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                                (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                                (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
                            (a :
                                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u))
                                  (stoneCechObj X)) →
                              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)
                          stoneCechUnit,
                      continuous_toFun := ⋯ : C((↑X : Type u), (↑Y.1 : Type u)) })
                ((fun (f : X ⟶ compHausToTop.obj Y) ↦
                    (ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := stoneCechExtend ⋯, continuous_toFun := ⋯ } :
                      Quiver.Hom (V := CompHausLike fun (x : TopCat.{u}) ↦ True)
                        (of (fun (x : TopCat.{u}) ↦ True) (StoneCech (↑X : Type u)))
                        (of (fun (x : TopCat.{u}) ↦ True) (↑Y.1 : Type u))))
                  { hom' := { toFun := f, continuous_toFun := hf } })) :
            (a : (↑(TopCat.of (↑X : Type u)) : Type u)) → (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
          x :
        (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
      ((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
              TopCat.carrier _ _ (TopCat.of (↑X : Type u)) (TopCat.of (↑Y.1 : Type u))
              { hom' := { toFun := f, continuous_toFun := hf : C((↑X : Type u), (↑(compHausToTop.obj Y) : Type u)) } :
                X.Hom (compHausToTop.obj Y) } :
            (a : (↑(TopCat.of (↑X : Type u)) : Type u)) → (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
          x :
        (↑(TopCat.of (↑Y.1 : Type u)) : Type u))
⊢ (fun (f : stoneCechObj X ⟶ Y) ↦
        TopCat.ofHom
          {
            toFun :=
              Function.comp (β :=
                (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                    (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
                  (stoneCechObj X))
                (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                      C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                        (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                      (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                      (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
                  (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) (stoneCechObj X)) →
                    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)
                stoneCechUnit,
            continuous_toFun := ⋯ : C((↑X : Type u), (↑Y.1 : Type u)) })
      ((fun (f : X ⟶ compHausToTop.obj Y) ↦
          (ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := stoneCechExtend ⋯, continuous_toFun := ⋯ } :
            Quiver.Hom (V := CompHausLike fun (x : TopCat.{u}) ↦ True)
              (of (fun (x : TopCat.{u}) ↦ True) (StoneCech (↑X : Type u)))
              (of (fun (x : TopCat.{u}) ↦ True) (↑Y.1 : Type u))))
        { hom' := { toFun := f, continuous_toFun := hf } }) =
    { hom' := { toFun := f, continuous_toFun := hf : C((↑X : Type u), (↑(compHausToTop.obj Y) : Type u)) } :
      X.Hom (compHausToTop.obj Y) }

Tactic:
ext