-- 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
w :
  ∀ (f : Arrow (Sheaf.{v, v', u, u'} J A)),
    NatTrans.app
        (CategoryStruct.comp (Y :=
          mapArrow (sheafToPresheaf J A) ⋙
            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ᵒᵖ) ⋙
              presheafToSheaf J A)
          (whiskerLeft Arrow.leftFunc (inv (Adjunction.counit (sheafificationAdjunction J A))) ≫
            whiskerLeft (mapArrow (sheafToPresheaf J A))
              (whiskerRight
                (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ᵒᵖ))
                (presheafToSheaf J A)))
          (whiskerLeft (mapArrow (sheafToPresheaf J A))
              (whiskerRight
                (MorphismProperty.FunctorialFactorizationData.p (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ᵒᵖ))
                (presheafToSheaf J A)) ≫
            whiskerLeft Arrow.rightFunc (Adjunction.counit (sheafificationAdjunction J A))))
        f =
      NatTrans.app Arrow.leftToRight f
⊢ Eq (α := Quiver.Hom (V := Arrow (Sheaf.{v, v', u, u'} J A) ⥤ Sheaf.{v, v', u, u'} J A) Arrow.leftFunc Arrow.rightFunc)
    (CategoryStruct.comp (Y :=
        mapArrow (sheafToPresheaf J A) ⋙
          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ᵒᵖ) ⋙
            presheafToSheaf J A)
        (whiskerLeft Arrow.leftFunc (inv (Adjunction.counit (sheafificationAdjunction J A))) ≫
          whiskerLeft (mapArrow (sheafToPresheaf J A))
            (whiskerRight
              (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ᵒᵖ))
              (presheafToSheaf J A)))
        (whiskerLeft (mapArrow (sheafToPresheaf J A))
            (whiskerRight
              (MorphismProperty.FunctorialFactorizationData.p (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ᵒᵖ))
              (presheafToSheaf J A)) ≫
          whiskerLeft Arrow.rightFunc (Adjunction.counit (sheafificationAdjunction J A))) :
      Quiver.Hom (V := Arrow (Sheaf.{v, v', u, u'} J A) ⥤ Sheaf.{v, v', u, u'} J A) Arrow.leftFunc Arrow.rightFunc)
    (Arrow.leftToRight :
      Quiver.Hom (V := Arrow (Sheaf.{v, v', u, u'} J A) ⥤ Sheaf.{v, v', u, u'} J A) Arrow.leftFunc Arrow.rightFunc)

Tactic:
ext f : 2