-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k : ι
i j : (glueData hf).J
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op ((glueData hf).V (i, j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.obj (P := Presheaf.IsSheaf zariskiTopology).map ((glueData hf).f i j).op) :
          (a : (fun (X : Type u) ↦ X) (F.obj.obj (op ((glueData hf).U i)))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op ((glueData hf).V (i, j)))))
        ((fun (i : (glueData hf).J) ↦
            ((yonedaEquiv : (a : yoneda.obj ((glueData hf).U i) ⟶ F.obj) → F.obj.obj (op ((glueData hf).U i))) (f i) :
              F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op ((glueData hf).U i))))
          i) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op ((glueData hf).V (i, j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.obj (P := Presheaf.IsSheaf zariskiTopology).map (((glueData hf).f j i).op ≫ ((glueData hf).t i j).op)) :
          (a : (fun (X : Type u) ↦ X) (F.obj.obj (op ((glueData hf).U j)))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op ((glueData hf).V (i, j)))))
        ((fun (i : (glueData hf).J) ↦
            ((yonedaEquiv : (a : yoneda.obj ((glueData hf).U i) ⟶ F.obj) → F.obj.obj (op ((glueData hf).U i))) (f i) :
              F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op ((glueData hf).U i))))
          j) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op ((glueData hf).V (i, j)))))
have a : Eq (α := Functor.obj yoneda ((glueData hf).V (i, j)) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology))
  ((Equiv.symm yonedaEquiv :
        (a : F.obj.obj (op ((glueData hf).V (i, j)))) → yoneda.obj ((glueData hf).V (i, j)) ⟶ F.obj)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (F.obj (P := Presheaf.IsSheaf zariskiTopology).map ((glueData hf).f i j).op) :
            (a : (fun (X : Type u) ↦ X) (F.obj.obj (op ((glueData hf).U i)))) →
              (fun (X : Type u) ↦ X) (F.obj.obj (op ((glueData hf).V (i, j)))))
          ((fun (i : (glueData hf).J) ↦
              ((yonedaEquiv : (a : yoneda.obj ((glueData hf).U i) ⟶ F.obj) → F.obj.obj (op ((glueData hf).U i))) (f i) :
                F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op ((glueData hf).U i))))
            i) :
        (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op ((glueData hf).V (i, j))))) :
    Functor.obj yoneda ((glueData hf).V (i, j)) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology))
  ((Equiv.symm yonedaEquiv :
        (a : F.obj.obj (op ((glueData hf).V (i, j)))) → yoneda.obj ((glueData hf).V (i, j)) ⟶ F.obj)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (F.obj (P := Presheaf.IsSheaf zariskiTopology).map
                (((glueData hf).f j i).op ≫ ((glueData hf).t i j).op)) :
            (a : (fun (X : Type u) ↦ X) (F.obj.obj (op ((glueData hf).U j)))) →
              (fun (X : Type u) ↦ X) (F.obj.obj (op ((glueData hf).V (i, j)))))
          ((fun (i : (glueData hf).J) ↦
              ((yonedaEquiv : (a : yoneda.obj ((glueData hf).U i) ⟶ F.obj) → F.obj.obj (op ((glueData hf).U i))) (f i) :
                F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op ((glueData hf).U i))))
            j) :
        (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op ((glueData hf).V (i, j))))) :
    Functor.obj yoneda ((glueData hf).V (i, j)) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology))
Tactic: apply yonedaEquiv.symm.injective