-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f : X ⟶ Y
rw :
  IsLocallySurjective (FA := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CA := ModuleCat.carrier)
      f ↔
    ∀ (S : LightProfinite.{u})
      (y : (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)),
      ∃ (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 : (↑(X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u)),
        Eq (α := (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (X :=
                  X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S'))
                  (f.hom.app (Opposite.op S')) :
                (a : (↑(X.obj.obj (Opposite.op S')) : Type u)) → (↑(Y.obj.obj (Opposite.op S')) : Type u))
              x :
            (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier)
                  (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map (Opposite.op φ)) :
                (a : (↑(Y.obj.obj (Opposite.op S)) : Type u)) → (↑(Y.obj.obj (Opposite.op S')) : Type u))
              y :
            (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
⊢ Epi f ↔
    ∀ (S : LightProfinite.{u})
      (y : (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S)) : Type u)),
      ∃ (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 : (↑(X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u)),
        Eq (α := (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (X :=
                  X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S'))
                  (f.hom.app (Opposite.op S')) :
                (a : (↑(X.obj.obj (Opposite.op S')) : Type u)) → (↑(Y.obj.obj (Opposite.op S')) : Type u))
              x :
            (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier)
                  (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map (Opposite.op φ)) :
                (a : (↑(Y.obj.obj (Opposite.op S)) : Type u)) → (↑(Y.obj.obj (Opposite.op S')) : Type u))
              y :
            (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj (Opposite.op S')) : Type u))

Tactic:
rw [← isLocallySurjective_iff_epi']

Premises used: CategoryTheory.Sheaf.isLocallySurjective_iff_epi'