-- 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))
    (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)
    (comp (β := Ultrafilter X)
      (⇑(TopCat.Hom.hom f.hom) : (a : (↑(of (Ultrafilter X)).toTop : Type u_1)) → (↑Z.toTop : Type u_1)) pure)
⊢ 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)

Tactic:
rw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp]

Premises used: ultrafilter_extend_extends, Function.comp_assoc, Function.id_comp