-- Module: Mathlib.Topology.Category.CompHaus.Projective
Goal:
X : Type u_1
Y Z : CompHaus
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg :
  Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Y)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Z)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) g) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
g' :
  (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Z →
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Y
hg' :
  RightInverse g'
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) g) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
t : X → (↑(Y.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) :=
  g' ∘
    comp (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
        (of (Ultrafilter X)))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
              (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) f) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) (of (Ultrafilter X))) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Z)
      pure
h : Ultrafilter X → (↑(Y.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) := Ultrafilter.extend t
hh : Continuous h
this :
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := TopCat.carrier)
            g.hom) :
        (a : (↑Y.toTop : Type u_1)) → (↑Z.toTop : Type u_1)) ∘
      g' =
    id
h₁ :
  Eq (α := X → (↑(Z.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
    (((⇑(TopCat.Hom.hom g.hom) : (a : (↑Y.toTop : Type u_1)) → (↑Z.toTop : Type u_1)) ∘ h) ∘ pure)
    (comp (β := Ultrafilter X)
      (⇑(TopCat.Hom.hom f.hom) : (a : (↑(of (Ultrafilter X)).toTop : Type u_1)) → (↑Z.toTop : Type u_1)) pure)
⊢ Eq (α :=
    (a : (↑((of (Ultrafilter X)).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) →
      (↑(Z.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) (X := of (Ultrafilter X))
          (CompHausLike.ofHom (fun (x : TopCat.{u_1}) ↦ True) { toFun := h, continuous_toFun := hh } ≫ g)) :
      (a : (↑(of (Ultrafilter X)).toTop : Type u_1)) → (↑Z.toTop : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) f) :
      (a : (↑(of (Ultrafilter X)).toTop : Type u_1)) → (↑Z.toTop : Type u_1))

Tactic:
convert!
      denseRange_pure.equalizer (g.hom.hom.continuous.comp hh) f.hom.hom.continuous
        _

Premises used: ContinuousMap.continuous, DenseRange.equalizer, denseRange_pure, Continuous.comp, TopCat.Hom.hom, CategoryTheory.InducedCategory.Hom.hom