-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
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 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_6 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
inst_7 :
  ∀ (P : Functor.{v, v', u, u'} Cᵒᵖ A),
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J P)
      (CategoryTheory.toSheafify J P)
inst_8 :
  ∀ (P : Functor.{v, v', u, u'} Cᵒᵖ A),
    Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (G := CategoryTheory.sheafify J P)
      (CategoryTheory.toSheafify J P)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
f : P ⟶ Q
rw :
  IsIso (X := Functor.obj (presheafToSheaf J A) P) (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw₁ :
  Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ∧
      Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw₂ :
  Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ∧
      Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J Q)
        (f ≫ CategoryTheory.toSheafify J Q) ∧
      Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw₃ :
  Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ∧
      Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J Q)
        (f ≫ CategoryTheory.toSheafify J Q) ∧
      Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (G := CategoryTheory.sheafify J Q)
        (f ≫ CategoryTheory.toSheafify J Q)
rw₄ :
  Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ∧
      Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J Q)
        (CategoryTheory.toSheafify J P ≫ CategoryTheory.sheafifyMap J f) ∧
      Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (G := CategoryTheory.sheafify J Q)
        (CategoryTheory.toSheafify J P ≫ CategoryTheory.sheafifyMap J f)
rw₅ :
  Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ∧
      Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₁ := CategoryTheory.sheafify J P)
        (CategoryTheory.sheafifyMap J f) ∧
      Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (G := CategoryTheory.sheafify J Q)
        (CategoryTheory.toSheafify J P ≫ CategoryTheory.sheafifyMap J f)
rw₆ rw₇ :
  Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ∧
      Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₁ := CategoryTheory.sheafify J P)
        (CategoryTheory.sheafifyMap J f) ∧
      Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (F := CategoryTheory.sheafify J P)
        (CategoryTheory.sheafifyMap J f)
⊢ J.W f ↔ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f

Tactic:
rw [W_iff, ← Sheaf.isLocallyBijective_iff_isIso (A := A),
      ← Presheaf.isLocallyInjective_comp_iff J f (CategoryTheory.toSheafify J Q),
      ← Presheaf.isLocallySurjective_comp_iff J f (CategoryTheory.toSheafify J Q),
      CategoryTheory.toSheafify_naturality, Presheaf.comp_isLocallyInjective_iff,
      Presheaf.comp_isLocallySurjective_iff]

Premises used: CategoryTheory.toSheafify, CategoryTheory.Presheaf.comp_isLocallySurjective_iff, CategoryTheory.Presheaf.isLocallySurjective_comp_iff, CategoryTheory.Presheaf.isLocallyInjective_comp_iff, CategoryTheory.GrothendieckTopology.W_iff, CategoryTheory.Sheaf.isLocallyBijective_iff_isIso, CategoryTheory.Presheaf.comp_isLocallyInjective_iff, CategoryTheory.toSheafify_naturality