-- Lean 4 proof step from Mathlib.Condensed.Light.EffectiveEpi (goal)
Goal:
X Y : LightProfinite
f : X ⟶ Y
hf : Epi f
S : LightProfinite
g :
  (lightProfiniteToLightCondSet.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)
⊢ ∃ (S' : LightProfinite.{u_1}) (φ : S' ⟶ S) (_ :
    Function.Surjective (α :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
            Type u_1))
        S')
      (β :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
            Type u_1))
        S)
      (⇑(ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                CompHausLike fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                Type u_1),
              (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                Type u_1)))
            (CC :=
            fun
              (X :
                CompHausLike fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
              Type u_1))
            φ) :
        (a :
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
                (↑X.toTop : Type u_1))
              S') →
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
              (↑X.toTop : Type u_1))
            S))
    (x :
    (lightProfiniteToLightCondSet.obj X).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
      (Opposite.op S')),
    Eq (α :=
      (fun (X : Type u_1) ↦ X)
        ((lightProfiniteToLightCondSet.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
          (Opposite.op S')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((lightProfiniteToLightCondSet.map f).hom.app (Opposite.op S')) :
            (a : (fun (X : Type u_1) ↦ X) ((lightProfiniteToLightCondSet.obj X).obj.obj (Opposite.op S'))) →
              (fun (X : Type u_1) ↦ X) ((lightProfiniteToLightCondSet.obj Y).obj.obj (Opposite.op S')))
          x :
        (fun (X : Type u_1) ↦ X)
          ((lightProfiniteToLightCondSet.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
            (Opposite.op S')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((lightProfiniteToLightCondSet.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map
                (Opposite.op φ)) :
            (a : (fun (X : Type u_1) ↦ X) ((lightProfiniteToLightCondSet.obj Y).obj.obj (Opposite.op S))) →
              (fun (X : Type u_1) ↦ X) ((lightProfiniteToLightCondSet.obj Y).obj.obj (Opposite.op S')))
          g :
        (fun (X : Type u_1) ↦ X)
          ((lightProfiniteToLightCondSet.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
            (Opposite.op S')))
have refine : ∀
  (y :
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
          Type u_1))
      S),
  ∃ (a :
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
          Type u_1))
      (pullback (P := fun (X : TopCat.{u_1}) ↦
        TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) f g)),
    (ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                CompHausLike fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                Type u_1),
              (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                Type u_1)))
            (CC :=
            fun
              (X :
                CompHausLike fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
              Type u_1))
            (X :=
            pullback (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) f g)
            (pullback.snd (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) f g) :
          (a :
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
                  (↑X.toTop : Type u_1))
                (pullback f g)) →
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
                (↑X.toTop : Type u_1))
              S)
        a =
      y
Tactic: refine ⟨pullback f g, pullback.snd _ _, fun y ↦ ?_, pullback.fst _ _, pullback.condition _ _⟩