-- Module: Mathlib.Condensed.EffectiveEpi
Goal:
X Y : CompHaus
f : X ⟶ Y
hf :
  Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      X)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      Y)
    (⇑(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)) X) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y)
S : CompHaus
g : (compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
y : (↑(S.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)
obtain :
  ∀ (x : (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
    (hx :
      Eq (α :=
        (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
          Y)
        ((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)) X) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) Y)
            x :
          (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
            Y)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) g.down.hom :
              (a : (↑(Opposite.unop (Opposite.op S)).toTop : Type u_1)) → (↑Y.toTop : Type u_1))
            y :
          (↑(Y.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))),
    ∃ (a :
      (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
        (pullback (P := fun (x : TopCat.{u_1}) ↦ True) f g.down)),
      (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 :=
              pullback (P := fun (x : TopCat.{u_1}) ↦ True) f g.down)
              (pullback.snd (P := fun (x : TopCat.{u_1}) ↦ True) f g.down) :
            (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) (pullback f g.down)) →
              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) S)
          a =
        y
⊢ ∃ (a :
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      (pullback (P := fun (x : TopCat.{u_1}) ↦ True) f g.down)),
    (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 :=
            pullback (P := fun (x : TopCat.{u_1}) ↦ True) f g.down)
            (pullback.snd (P := fun (x : TopCat.{u_1}) ↦ True) f g.down) :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) (pullback f g.down)) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) S)
        a =
      y

Tactic:
obtain ⟨x, hx⟩ := hf (g.down.hom y)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.InducedCategory.Hom.hom, DFunLike.coe, ULift.down