-- Module: Mathlib.CategoryTheory.Sites.LocallySurjective
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)
F₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
X : Cᵒᵖ
x₁ x₂ : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj X)
h :
  Eq (α := CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₁ : CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₂ : CA (F₃.obj X))
S : Sieve.{v, u} (unop X) := imageSieve (FA := FA) (CA := CA) f₁ x₁ ⊓ imageSieve (FA := FA) (CA := CA) f₁ x₂
hS : Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) S
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (hf : S.arrows f) ↦
    equalizerSieve (FD := FA) (CD := CA) (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯)
      (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯)
Y : C
f : Y ⟶ unop X
hf : S.arrows f
refine_2 :
  Eq (α := CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
            (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯) :
          CA (F₂.obj (op Y))) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y) ≫ f₂.app (op Y)) :
          (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯) :
      CA (F₃.obj (op Y)))
refine_2₁ :
  Eq (α := CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
            (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯) :
          CA (F₂.obj (op Y))) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
            (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯) :
          CA (F₂.obj (op Y))) :
      CA (F₃.obj (op Y)))
refine_2₂ :
  Eq (α := CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) :
              (a : CA (F₂.obj (op (unop X)))) → CA (F₂.obj (op Y)))
            x₁ :
          CA (F₂.obj (op Y))) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
            (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯) :
          CA (F₂.obj (op Y))) :
      CA (F₃.obj (op Y)))
refine_2₃ :
  Eq (α := CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) :
              (a : CA (F₂.obj (op (unop X)))) → CA (F₂.obj (op Y)))
            x₁ :
          CA (F₂.obj (op Y))) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) :
              (a : CA (F₂.obj (op (unop X)))) → CA (F₂.obj (op Y)))
            x₂ :
          CA (F₂.obj (op Y))) :
      CA (F₃.obj (op Y)))
refine_2₄ :
  Eq (α := CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map f.op) : (a : CA (F₃.obj (op (unop X)))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op (unop X))) :
              (a : CA (F₂.obj (op (unop X)))) → CA (F₃.obj (op (unop X))))
            x₁ :
          CA (F₃.obj (op (unop X)))) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) :
              (a : CA (F₂.obj (op (unop X)))) → CA (F₂.obj (op Y)))
            x₂ :
          CA (F₂.obj (op Y))) :
      CA (F₃.obj (op Y)))
refine_2₅ :
  Eq (α := CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map f.op) : (a : CA (F₃.obj (op (unop X)))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op (unop X))) :
              (a : CA (F₂.obj (op (unop X)))) → CA (F₃.obj (op (unop X))))
            x₁ :
          CA (F₃.obj (op (unop X)))) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map f.op) : (a : CA (F₃.obj (op (unop X)))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op (unop X))) :
              (a : CA (F₂.obj (op (unop X)))) → CA (F₃.obj (op (unop X))))
            x₂ :
          CA (F₃.obj (op (unop X)))) :
      CA (F₃.obj (op Y)))
refine_2₆ refine_2₇ :
  Eq (α := CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map f.op) : (a : CA (F₃.obj (op (unop X)))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₂ :
          CA (F₃.obj X)) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₃.map f.op) : (a : CA (F₃.obj (op (unop X)))) → CA (F₃.obj (op Y)))
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op (unop X))) :
              (a : CA (F₂.obj (op (unop X)))) → CA (F₃.obj (op (unop X))))
            x₂ :
          CA (F₃.obj (op (unop X)))) :
      CA (F₃.obj (op Y)))
⊢ Eq (α := CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y) ≫ f₂.app (op Y)) :
          (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y) ≫ f₂.app (op Y)) :
          (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯) :
      CA (F₃.obj (op Y)))

Tactic:
rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, app_localPreimage,
        app_localPreimage, NatTrans.naturality_apply, NatTrans.naturality_apply, h]

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Presheaf.app_localPreimage