-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Projective (hypothesis)
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
⊢ 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))
have 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
Tactic: have : g.hom ∘ g' = id := hg'.comp_eq_id