-- Module: Mathlib.Condensed.Epi
Goal:
A : Type u'
inst : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst_1 : (X Y : A) → FunLike.{u_1 + 1, v' + 1, v' + 1} (FA X Y) (CA X) (CA Y)
inst_2 : ConcreteCategory A FA (CC := CA)
inst_3 : HasFunctorialSurjectiveInjectiveFactorization A (FC := FA) (CC := CA)
X Y : Condensed.{u, v', u'} A
f : X ⟶ Y
inst_4 : PreservesFiniteProducts (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_5 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v', u'} (StructuredArrow X Stonean.toCompHaus.op) A
inst_6 : GrothendieckTopology.WEqualsLocallyBijective (extensiveTopology Stonean) A (FA := FA) (CA := CA)
inst_7 : HasSheafify.{u, v', u + 1, u'} (extensiveTopology Stonean) A
inst_8 :
  GrothendieckTopology.HasSheafCompose (extensiveTopology Stonean) (CategoryTheory.forget A (FC := FA) (CC := CA))
inst_9 : Balanced (Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
⊢ IsLocallySurjective (J := extensiveTopology Stonean) (FA := FA) (CA := CA) (F₁ :=
      (Functor.obj
          (Equivalence.functor Presheaf.coherentExtensiveEquivalence :
            Sheaf.{u, v', u + 1, u'} (coherentTopology Stonean) A ⥤
              Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
          (Functor.obj (Equivalence.inverse (StoneanCompHaus.equivalence A)) X) :
        Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A))
      (F₂ :=
      (Functor.obj
          (Equivalence.functor Presheaf.coherentExtensiveEquivalence :
            Sheaf.{u, v', u + 1, u'} (coherentTopology Stonean) A ⥤
              Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
          (Functor.obj (Equivalence.inverse (StoneanCompHaus.equivalence A)) Y) :
        Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A))
      (CategoryTheory.Functor.map (Equivalence.functor Presheaf.coherentExtensiveEquivalence)
          (CategoryTheory.Functor.map (Equivalence.inverse (StoneanCompHaus.equivalence A)) f) :
        Quiver.Hom (V := Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
          (Functor.obj
              (Equivalence.functor Presheaf.coherentExtensiveEquivalence :
                Sheaf.{u, v', u + 1, u'} (coherentTopology Stonean) A ⥤
                  Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
              (Functor.obj (Equivalence.inverse (StoneanCompHaus.equivalence A)) X) :
            Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
          (Functor.obj
              (Equivalence.functor Presheaf.coherentExtensiveEquivalence :
                Sheaf.{u, v', u + 1, u'} (coherentTopology Stonean) A ⥤
                  Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)
              (Functor.obj (Equivalence.inverse (StoneanCompHaus.equivalence A)) Y) :
            Sheaf.{u, v', u + 1, u'} (extensiveTopology Stonean) A)) ↔
    ∀ (S : Stonean.{u}),
      Function.Surjective.{v' + 1, v' + 1} (α :=
        CA (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S.compHaus))) (β :=
        CA (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S.compHaus)))
        (⇑(hom (FC := FA) (CC := CA) (f.hom.app (op S.compHaus))) :
          (a : CA (X.obj.obj (op S.compHaus))) → CA (Y.obj.obj (op S.compHaus)))

Tactic:
extensiveTopology.isLocallySurjective_iff (D := A) _

Premises used: CategoryTheory.extensiveTopology.isLocallySurjective_iff