-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EpiMono (goal)
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)
⊢ IsLocallyInjective (FD := FA) (CD := CA) (F₁ :=
    obj (presheafToSheaf J A)
      (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)))
    (map (presheafToSheaf J A)
        (NatTrans.app
          (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ᵒᵖ))
          (Arrow.mk x.hom.hom)) ≫
      NatTrans.app (Adjunction.counit (sheafificationAdjunction J A)) x.right)
have rw : Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
  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.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ᵒᵖ))
    (Arrow.mk x.hom.hom))
Tactic: rw [← isLocallyInjective_sheafToPresheaf_map_iff, Functor.map_comp,
      Presheaf.isLocallyInjective_comp_iff, isLocallyInjective_sheafToPresheaf_map_iff,
      Presheaf.isLocallyInjective_presheafToSheaf_map_iff]