-- Module: Mathlib.Condensed.Light.EffectiveEpi
Goal:
X Y : LightProfinite
f : X ⟶ Y
hf : Epi f
rw :
  ∀ (S : LightProfinite.{u_1})
    (y :
      (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')))
            y :
          (fun (X : Type u_1) ↦ X)
            ((lightProfiniteToLightCondSet.obj Y).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
              (Opposite.op S')))
⊢ Epi (lightProfiniteToLightCondSet.map f)

Tactic:
rw [LightCondSet.epi_iff_locallySurjective_on_lightProfinite]

Premises used: LightCondSet.epi_iff_locallySurjective_on_lightProfinite