∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ D} {φ : F₁ ⟶ F₂} {ψ : F₂ ⟶ F₃} {φψ : F₁ ⟶ F₃},
  CategoryTheory.CategoryStruct.comp φ ψ = φψ →
    ∀ [CategoryTheory.Presheaf.IsLocallyInjective J ψ],
      CategoryTheory.Presheaf.IsLocallyInjective J φψ ↔ CategoryTheory.Presheaf.IsLocallyInjective J φ