-- Lean 4 proof step from Mathlib.Condensed.EffectiveEpi (goal)
Goal:
X Y : CompHaus
f : X ⟶ Y
hf : Epi f
S : CompHaus
g : (compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
⊢ ∃ (S' : CompHaus.{u_1}) (φ : S' ⟶ S) (_ :
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
        S')
      (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
        S)
      (⇑(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 : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) S') →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) S))
    (x : (compHausToCondensed.obj X).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')),
    Eq (α :=
      (fun (X : Type (u_1 + 1)) ↦ X)
        ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((compHausToCondensed.map f).hom.app (Opposite.op S')) :
            (a : (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj X).obj.obj (Opposite.op S'))) →
              (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj Y).obj.obj (Opposite.op S')))
          x :
        (fun (X : Type (u_1 + 1)) ↦ X)
          ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
                (Opposite.op φ)) :
            (a : (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj Y).obj.obj (Opposite.op S))) →
              (fun (X : Type (u_1 + 1)) ↦ X) ((compHausToCondensed.obj Y).obj.obj (Opposite.op S')))
          g :
        (fun (X : Type (u_1 + 1)) ↦ X)
          ((compHausToCondensed.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S')))
have refine : ∀
  (y :
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      S),
  ∃ (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: refine ⟨pullback f g.down, pullback.snd _ _, fun y ↦ ?_, ⟨pullback.fst _ _⟩,
      ULift.ext _ _ <| pullback.condition _ _⟩