-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyInjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_1 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v', u', u_1} D FD (CC := CD)
J : GrothendieckTopology.{v, u} C
F₁ F₂ : Functor.{v, v', u, u'} Cᵒᵖ D
φ : F₁ ⟶ F₂
h_1 : IsLocallyInjective (FD := FD) (CD := CD) J φ
X : Cᵒᵖ
x y : ToType.{w, v', u', u_1} (FC := FD) (CC := CD) (F₁.obj X)
h :
  Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
S : Sieve.{v, u} (unop X) :=
  equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (x_1 : S.arrows f) ↦
    equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₁)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) : (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
        y)
Y : C
f : Y ⟶ unop X
hf :
  Sieve.arrows
    (equalizerSieve.{w, v', v, u', u, u_1} (FD := FD) (CD := CD) (F := F₂)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) x)
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F₁.obj X)) → CD (F₂.obj X)) y))
    f
⊢ Eq (α := CD (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) :
              (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
            x :
          CD (F₁.obj (op Y))) :
      CD (F₂.obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op Y)) : (a : CD (F₁.obj (op Y))) → CD (F₂.obj (op Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₁.map f.op) :
              (a : CD (F₁.obj (op (unop X)))) → CD (F₁.obj (op Y)))
            y :
          CD (F₁.obj (op Y))) :
      CD (F₂.obj (op Y)))
have mp : Eq (α := CD (F₂.obj (op Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₂.map f.op) : (a : CD (F₂.obj (op (unop X)))) → CD (F₂.obj (op Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op (unop X))) :
            (a : CD (F₁.obj (op (unop X)))) → CD (F₂.obj (op (unop X))))
          x :
        CD (F₂.obj (op (unop X)))) :
    CD (F₂.obj (op Y)))
  ((ConcreteCategory.hom (FC := FD) (CC := CD) (F₂.map f.op) : (a : CD (F₂.obj (op (unop X)))) → CD (F₂.obj (op Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app (op (unop X))) :
            (a : CD (F₁.obj (op (unop X)))) → CD (F₂.obj (op (unop X))))
          y :
        CD (F₂.obj (op (unop X)))) :
    CD (F₂.obj (op Y)))
Tactic: rw [NatTrans.naturality_apply, NatTrans.naturality_apply]