-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst : Epi f
this : ExtremallyDisconnected.{u_1} (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)
hf :
  Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      B)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      C)
    (⇑(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)) B) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) C)
f' :
  (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) →
    (↑(B.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)
h :
  Continuous f' ∧
    Eq (α :=
      (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) →
        (↑(C.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      ((⇑(TopCat.Hom.hom f.hom) : (a : (↑B.toTop : Type u_1)) → (↑C.toTop : Type u_1)) ∘ f')
      (⇑(TopCat.Hom.hom φ.hom) : (a : (↑(toCompHaus.obj X).toTop : Type u_1)) → (↑C.toTop : Type u_1))
h₁ :
  ∀ (a : (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)),
    Eq (α := (↑(C.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 := toCompHaus.obj X)
                (ofHom (fun (x : TopCat.{u_1}) ↦ True) { toFun := f', continuous_toFun := ⋯ } ≫ f :
                  toCompHaus.obj X ⟶ C) :
              C((↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
                (↑(C.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))) :
            (a : (↑(toCompHaus.obj X).toTop : Type u_1)) → (↑C.toTop : Type u_1))
          a :
        (↑(C.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)) φ :
            (a : (↑(toCompHaus.obj X).toTop : Type u_1)) → (↑C.toTop : Type u_1))
          a :
        (↑(C.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
⊢ ofHom (fun (x : TopCat.{u_1}) ↦ True) { toFun := f', continuous_toFun := ⋯ } ≫ f = φ

Tactic:
ext