-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X : TopCat
Y : CompHaus
f :
  (↑((stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) →
    (↑(Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
hf : Continuous f
x : (↑(toTop (P := fun (x : TopCat.{u}) ↦ True) (of (fun (x : TopCat.{u}) ↦ True) (StoneCech (↑X : Type u)))) : Type u)
h :
  Set.EqOn
    (stoneCechExtend (g :=
      ContinuousMap.toFun
        (TopCat.Hom.hom
          ((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)) })
            {
              hom :=
                {
                  hom' :=
                    { toFun := f, continuous_toFun := hf :
                      C((↑((stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                        (↑(Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) } :
                  (stoneCechObj X).toTop (P := fun (x : TopCat.{u}) ↦ True).Hom
                    (Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) } :
              InducedCategory.Hom (D := TopCat) (F := toTop (P := fun (x : TopCat.{u}) ↦ True)) (stoneCechObj X) Y })))
      ⋯)
    f (Set.range stoneCechUnit)
⊢ Eq (α :=
    (x :
        (↑(toTop (P := fun (x : TopCat.{u}) ↦ True) (of (fun (x : TopCat.{u}) ↦ True) (StoneCech (↑X : Type u)))) :
          Type u)) →
      (↑(toTop (P := fun (x : TopCat.{u}) ↦ True) (of (fun (x : TopCat.{u}) ↦ True) (↑Y.1 : Type u))) : Type u))
    (⇑(@ConcreteCategory.hom _ (category fun (x : TopCat.{u}) ↦ True)
          (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)))
          (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          _ _ (of (fun (x : TopCat.{u}) ↦ True) (StoneCech (↑X : Type u)))
          (of (fun (x : TopCat.{u}) ↦ True) (↑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))))
            ((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)) })
              { hom := { hom' := { toFun := f, continuous_toFun := hf } } }))) :
      (a : (↑(of (fun (x : TopCat) ↦ True) (StoneCech (↑X : Type u))).toTop : Type u)) →
        (↑(of (fun (x : TopCat) ↦ True) (↑Y.1 : Type u)).toTop : Type u))
    (⇑(@ConcreteCategory.hom _ (category fun (x : TopCat.{u}) ↦ True)
          (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)))
          (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          _ _ (of (fun (x : TopCat.{u}) ↦ True) (StoneCech (↑X : Type u)))
          (of (fun (x : TopCat.{u}) ↦ True) (↑Y.1 : Type u))
          { hom := { hom' := { toFun := f, continuous_toFun := hf } } }) :
      (a : (↑(of (fun (x : TopCat) ↦ True) (StoneCech (↑X : Type u))).toTop : Type u)) →
        (↑(of (fun (x : TopCat) ↦ True) (↑Y.1 : Type u)).toTop : Type u))

Tactic:
apply Continuous.ext_on denseRange_stoneCechUnit (continuous_stoneCechExtend _) hf

Premises used: continuous_stoneCechExtend, Continuous.ext_on, denseRange_stoneCechUnit