-- 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))
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))

Tactic:
congr_fun h.right _

Premises used: And.right, congr_fun