-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
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
a :
  Eq (α := Functor.obj yoneda (⋯.pullback (f j)) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology))
    ((Equiv.symm yonedaEquiv : (a : F.obj.obj (op (⋯.pullback (f j)))) → yoneda.obj (⋯.pullback (f j)) ⟶ F.obj)
        ((yonedaEquiv : (a : yoneda.obj (⋯.pullback (f j)) ⟶ F.obj) → F.obj.obj (op (⋯.pullback (f j))))
            (CategoryTheory.Functor.map yoneda (⋯.fst' (f j)) ≫ f i) :
          F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (⋯.pullback (f j)))) :
      Functor.obj yoneda (⋯.pullback (f j)) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology))
    ((Equiv.symm yonedaEquiv : (a : F.obj.obj (op (⋯.pullback (f j)))) → yoneda.obj (⋯.pullback (f j)) ⟶ F.obj)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.obj (P := Presheaf.IsSheaf zariskiTopology).map ((⋯.fst' (f i)).op ≫ (⋯.symmetry ⋯).op)) :
              (a : F.obj.obj (op (X j))) → F.obj.obj (op (⋯.pullback (f j))))
            ((yonedaEquiv : (a : yoneda.obj (X j) ⟶ F.obj) → F.obj.obj (op (X j))) (f j) :
              F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X j))) :
          F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (⋯.pullback (f j)))) :
      Functor.obj yoneda (⋯.pullback (f j)) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology))
a₁ :
  CategoryTheory.Functor.map yoneda (⋯.fst' (f j)) ≫ f i =
    (Equiv.symm yonedaEquiv : (a : F.obj.obj (op (⋯.pullback (f j)))) → yoneda.obj (⋯.pullback (f j)) ⟶ F.obj)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (F.obj (P := Presheaf.IsSheaf zariskiTopology).map ((⋯.fst' (f i)).op ≫ (⋯.symmetry ⋯).op)) :
            (a : F.obj.obj (op (X j))) → F.obj.obj (op (⋯.pullback (f j))))
          ((yonedaEquiv : (a : yoneda.obj (X j) ⟶ F.obj) → F.obj.obj (op (X j))) (f j) :
            F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X j))) :
        F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (⋯.pullback (f j))))
a₂ :
  CategoryTheory.Functor.map yoneda (⋯.fst' (f j)) ≫ f i =
    (Equiv.symm yonedaEquiv : (a : F.obj.obj (op (⋯.pullback (f j)))) → yoneda.obj (⋯.pullback (f j)) ⟶ F.obj)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf zariskiTopology).map (⋯.symmetry ⋯).op) :
            (a : F.obj.obj (op (⋯.pullback (f i)))) → F.obj.obj (op (⋯.pullback (f j))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (F.obj (P := Presheaf.IsSheaf zariskiTopology).map (⋯.fst' (f i)).op) :
                (a : F.obj.obj (op (X j))) → F.obj.obj (op (⋯.pullback (f i))))
              ((yonedaEquiv : (a : yoneda.obj (X j) ⟶ F.obj) → F.obj.obj (op (X j))) (f j) :
                F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X j))) :
            F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (⋯.pullback (f i)))) :
        F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (⋯.pullback (f j))))
a₃ :
  CategoryTheory.Functor.map yoneda (⋯.fst' (f j)) ≫ f i =
    (Equiv.symm yonedaEquiv : (a : F.obj.obj (op (⋯.pullback (f j)))) → yoneda.obj (⋯.pullback (f j)) ⟶ F.obj)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf zariskiTopology).map (⋯.symmetry ⋯).op) :
            (a : F.obj.obj (op (⋯.pullback (f i)))) → F.obj.obj (op (⋯.pullback (f j))))
          ((yonedaEquiv : (a : yoneda.obj (⋯.pullback (f i)) ⟶ F.obj) → F.obj.obj (op (⋯.pullback (f i))))
              (CategoryTheory.Functor.map yoneda (⋯.fst' (f i)) ≫ f j) :
            F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (⋯.pullback (f i)))) :
        F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (⋯.pullback (f j))))
a₄ :
  CategoryTheory.Functor.map yoneda (⋯.fst' (f j)) ≫ f i =
    (Equiv.symm yonedaEquiv : (a : F.obj.obj (op (⋯.pullback (f j)))) → yoneda.obj (⋯.pullback (f j)) ⟶ F.obj)
      ((yonedaEquiv : (a : yoneda.obj (⋯.pullback (f j)) ⟶ F.obj) → F.obj.obj (op (⋯.pullback (f j))))
          (CategoryTheory.Functor.map yoneda (⋯.symmetry ⋯) ≫ CategoryTheory.Functor.map yoneda (⋯.fst' (f i)) ≫ f j) :
        F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (⋯.pullback (f j))))
a₅ :
  CategoryTheory.Functor.map yoneda (⋯.fst' (f j)) ≫ f i =
    CategoryTheory.Functor.map yoneda (⋯.symmetry ⋯) ≫ CategoryTheory.Functor.map yoneda (⋯.fst' (f i)) ≫ f j
a₆ :
  CategoryTheory.Functor.map yoneda (⋯.fst' (f j)) ≫ f i =
    CategoryTheory.Functor.map yoneda (⋯.symmetry ⋯ ≫ ⋯.fst' (f i)) ≫ f j
a₇ : CategoryTheory.Functor.map yoneda (⋯.fst' (f j)) ≫ f i = CategoryTheory.Functor.map yoneda (⋯.snd (f j)) ≫ f j
a₈ a₉ : CategoryTheory.Functor.map yoneda (⋯.snd (f j)) ≫ f j = CategoryTheory.Functor.map yoneda (⋯.snd (f j)) ≫ f j
⊢ Eq (α := Functor.obj yoneda (⋯.pullback (f j)) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology))
    ((Equiv.symm yonedaEquiv : (a : F.obj.obj (op (⋯.pullback (f j)))) → yoneda.obj (⋯.pullback (f j)) ⟶ F.obj)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.obj (P := Presheaf.IsSheaf zariskiTopology).map (⋯.fst' (f j)).op) :
              (a : F.obj.obj (op (X i))) → F.obj.obj (op (⋯.pullback (f j))))
            ((yonedaEquiv : (a : yoneda.obj (X i) ⟶ F.obj) → F.obj.obj (op (X i))) (f i) :
              F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i))) :
          F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (⋯.pullback (f j)))) :
      Functor.obj yoneda (⋯.pullback (f j)) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology))
    ((Equiv.symm yonedaEquiv : (a : F.obj.obj (op (⋯.pullback (f j)))) → yoneda.obj (⋯.pullback (f j)) ⟶ F.obj)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.obj (P := Presheaf.IsSheaf zariskiTopology).map ((⋯.fst' (f i)).op ≫ (⋯.symmetry ⋯).op)) :
              (a : F.obj.obj (op (X j))) → F.obj.obj (op (⋯.pullback (f j))))
            ((yonedaEquiv : (a : yoneda.obj (X j) ⟶ F.obj) → F.obj.obj (op (X j))) (f j) :
              F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X j))) :
          F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (⋯.pullback (f j)))) :
      Functor.obj yoneda (⋯.pullback (f j)) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology))

Tactic:
rw [yonedaEquiv_naturality, Equiv.symm_apply_apply,
        Functor.map_comp_apply, yonedaEquiv_naturality, yonedaEquiv_naturality,
        Equiv.symm_apply_apply, ← Functor.map_comp_assoc,
        Functor.relativelyRepresentable.symmetry_fst, ((hf i).rep.isPullback' (f j)).w]

Premises used: Equiv.symm_apply_apply, CategoryTheory.Functor.map_comp_apply, CategoryTheory.Functor.relativelyRepresentable.symmetry_fst, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.yonedaEquiv_naturality, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, CategoryTheory.Functor.relativelyRepresentable.isPullback', CategoryTheory.MorphismProperty.relative.rep