-- Lean 4 proof step from Mathlib.Condensed.Light.Epi (hypothesis)
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst_1 : Epi f
S : LightProfinite
p : Functor.obj (LightCondensed.free R) S.toCondensed ⟶ Y
this : Epi (X := Functor.obj (LightCondensed.forget R) X) (CategoryTheory.Functor.map (LightCondensed.forget R) f)
⊢ ∃ (T : LightProfinite.{u}) (π : T ⟶ S) (g : Functor.obj (LightCondensed.free R) T.toCondensed ⟶ X),
    Epi π ∧ CategoryTheory.Functor.map (lightProfiniteToLightCondSet ⋙ LightCondensed.free R) π ≫ p = g ≫ f
have this₁ : ∀ (S : LightProfinite.{u})
  (y :
    (Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
      (Opposite.op S)),
  ∃ (S' : LightProfinite.{u}) (φ : S' ⟶ S) (_ :
    Function.Surjective (α :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        S')
      (β :=
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
            Type u))
        S)
      (⇑(ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u)))
            (CC :=
            fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
            φ) :
        (a :
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                (↑X.toTop : Type u))
              S') →
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
              (↑X.toTop : Type u))
            S))
    (x :
    (Functor.obj (LightCondensed.forget R) X).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
      (Opposite.op S')),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        ((Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
          (Opposite.op S')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (LightCondensed.forget R) f))
                (Opposite.op S')) :
            (a : (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj X).obj.obj (Opposite.op S'))) →
              (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S')))
          x :
        (fun (X : Type u) ↦ X)
          ((Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
            (Opposite.op S')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Functor.obj (LightCondensed.forget R) Y).obj (P :=
                    Presheaf.IsSheaf (coherentTopology LightProfinite)).map
                (Opposite.op φ)) :
            (a : (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S))) →
              (fun (X : Type u) ↦ X) (((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S')))
          y :
        (fun (X : Type u) ↦ X)
          ((Functor.obj (LightCondensed.forget R) Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
            (Opposite.op S')))
Tactic: rw [LightCondSet.epi_iff_locallySurjective_on_lightProfinite] at this
Cleared hypotheses: this