-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X Y : Stonean
f : X ⟶ Y
h_1 : Epi f
y : (↑(Y.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)
hy :
  ∀ (a : (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)),
    (ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
              (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)) f :
          (a : (↑X.toTop : Type u_1)) → (↑Y.toTop : Type u_1))
        a ≠
      y
C : Set
  ((fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
    Y) :=
  Set.range (ι :=
    (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
      X)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
            (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)) f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
            X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) Y)
hC : IsClosed C
U : Set
  ((fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
    Y) :=
  Cᶜ
hUy : U ∈ 𝓝 y
V : Set (↑(Y.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)
hV :
  Membership.mem (γ :=
    Set (Set (↑(Y.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))
    {s : Set (↑(Y.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1) |
      IsClopen s}
    V
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom (FC :=
    fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
    C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
      (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))
    (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
    {
      toFun :=
        (⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen (U := V) hV)) :
          (a : (↑Y.toTop : Type u_1)) → ULift.{u_1, 0} (Fin 2)),
      continuous_toFun := ⋯ }
h : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom (FC :=
    fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
    C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
      (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))
    (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
    {
      toFun :=
        fun (x : (↑(Y.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)) ↦
        { down := 1 },
      continuous_toFun := ⋯ }
H : h = g
⊢ Eq (α := Fin 2)
    (ULift.down.{u_1, 0}
      ((ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
              (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)) h :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
                Y) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
              (mkFinite (ULift.{u_1, 0} (Fin 2))))
        y))
    (ULift.down.{u_1, 0}
      ((ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
              (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)) g :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
                Y) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
              (mkFinite (ULift.{u_1, 0} (Fin 2))))
        y))

Tactic:
apply_fun fun e => (e y).down at H