-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ :
  ∀ (X : Cᵒᵖ),
    Function.Injective (α := F.obj (P := Presheaf.IsSheaf J).obj X) (β := G.obj (P := Presheaf.IsSheaf J).obj X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app X)) : (a : F.obj.obj X) → G.obj.obj X)
right : IsLocallySurjective (FA := TypeCat.Fun) f
X : Cᵒᵖ
s : G.obj (P := Presheaf.IsSheaf J).obj X
H : Presieve.IsSheafFor (F.obj (P := Presheaf.IsSheaf J)) (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows
t : Presieve.FamilyOfElements (F.obj (P := Presheaf.IsSheaf J))
  (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows :=
  fun (Y : C) (g : Y ⟶ Opposite.unop X) (hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g) ↦
    Presheaf.localPreimage (FA := TypeCat.Fun) f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op W)) :
          (a : F.obj.obj (Opposite.op W)) → G.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g₁.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op Y₁))) →
                (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op W)))
            (t f₁ hf₁) :
          (fun (X : Type w) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op W)) :
          (a : F.obj.obj (Opposite.op W)) → G.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g₂.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op Y₂))) →
                (fun (X : Type w) ↦ X) (F.obj.obj (Opposite.op W)))
            (t f₂ hf₂) :
          (fun (X : Type w) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
have eq₁ : Eq (α := G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op W)) :
        (a : F.obj.obj (Opposite.op W)) → G.obj.obj (Opposite.op W))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g₁.op) :
            (a : F.obj.obj (Opposite.op Y₁)) → F.obj.obj (Opposite.op W))
          (t f₁ hf₁) :
        F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)) :
    G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map g₁.op) :
        (a : G.obj.obj (Opposite.op Y₁)) → G.obj.obj (Opposite.op W))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op Y₁)) :
            (a : F.obj.obj (Opposite.op Y₁)) → G.obj.obj (Opposite.op Y₁))
          (t f₁ hf₁) :
        G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y₁)) :
    G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
Tactic: have eq₁ := NatTrans.naturality_apply f.hom g₁.op (t f₁ hf₁)