-- Module: Mathlib.CategoryTheory.Sites.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} A FA (CC := CA)
inst_4 : HasFunctorialSurjectiveInjectiveFactorization.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w, v', v, u', u, u_1} J A (FA := FA) (CA := CA)
data : FunctorialSurjectiveInjectiveFactorizationData.{v', u', u_1, w} A (FC := FA) (CC := CA)
inst_6 : HasWeakSheafify.{v, v', u, u'} J A
x : Arrow (Sheaf.{v, v', u, u'} J A)
H :
  ∀ (U : Cᵒᵖ),
    Function.Surjective.{w + 1, w + 1} (α := CA (x.left.obj (P := Presheaf.IsSheaf J).obj U)) (β :=
      CA
        ((obj
              (MorphismProperty.FunctorialFactorizationData.Z (W₁ :=
                MorphismProperty.functorCategory (MorphismProperty.surjective A (FC := FA) (CC := CA)) Cᵒᵖ) (W₂ :=
                MorphismProperty.functorCategory (MorphismProperty.injective A (FC := FA) (CC := CA)) Cᵒᵖ)
                (MorphismProperty.FunctorialFactorizationData.functorCategory (W₁ :=
                  MorphismProperty.surjective A (FC := FA) (CC := CA)) (W₂ :=
                  MorphismProperty.injective A (FC := FA) (CC := CA)) data Cᵒᵖ))
              (Arrow.mk x.hom.hom)).obj
          U))
      (⇑(ConcreteCategory.hom (FC := FA) (CC := CA)
            (NatTrans.app
              (NatTrans.app
                (MorphismProperty.FunctorialFactorizationData.i (W₁ :=
                  MorphismProperty.functorCategory (MorphismProperty.surjective A (FC := FA) (CC := CA)) Cᵒᵖ) (W₂ :=
                  MorphismProperty.functorCategory (MorphismProperty.injective A (FC := FA) (CC := CA)) Cᵒᵖ)
                  (MorphismProperty.FunctorialFactorizationData.functorCategory (W₁ :=
                    MorphismProperty.surjective A (FC := FA) (CC := CA)) (W₂ :=
                    MorphismProperty.injective A (FC := FA) (CC := CA)) data Cᵒᵖ))
                (Arrow.mk x.hom.hom))
              U)) :
        (a : CA (x.left.obj.obj U)) →
          CA
            (((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).Z.obj (Arrow.mk x.hom.hom)).obj
              U))
⊢ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (G :=
    obj
      (MorphismProperty.FunctorialFactorizationData.Z (W₁ :=
        MorphismProperty.functorCategory (MorphismProperty.surjective A (FC := FA) (CC := CA)) Cᵒᵖ) (W₂ :=
        MorphismProperty.functorCategory (MorphismProperty.injective A (FC := FA) (CC := CA)) Cᵒᵖ)
        (MorphismProperty.FunctorialFactorizationData.functorCategory (W₁ :=
          MorphismProperty.surjective A (FC := FA) (CC := CA)) (W₂ :=
          MorphismProperty.injective A (FC := FA) (CC := CA)) data Cᵒᵖ))
      (Arrow.mk x.hom.hom))
    (NatTrans.app
      (MorphismProperty.FunctorialFactorizationData.i (W₁ :=
        MorphismProperty.functorCategory (MorphismProperty.surjective A (FC := FA) (CC := CA)) Cᵒᵖ) (W₂ :=
        MorphismProperty.functorCategory (MorphismProperty.injective A (FC := FA) (CC := CA)) Cᵒᵖ)
        (MorphismProperty.FunctorialFactorizationData.functorCategory (W₁ :=
          MorphismProperty.surjective A (FC := FA) (CC := CA)) (W₂ :=
          MorphismProperty.injective A (FC := FA) (CC := CA)) data Cᵒᵖ))
      (Arrow.mk x.hom.hom))

Tactic:
apply Presheaf.isLocallySurjective_of_surjective

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_surjective