∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] {i j : J}
  (k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)) {U : (F.obj i).Opens}
  (h₁ : AlgebraicGeometry.Scheme.Hom.opensRange (F.map k₁.snd.1) ≤ U)
  (h₂ : AlgebraicGeometry.Scheme.Hom.opensRange (F.map k₂.snd.1) ≤ U),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map k₁.snd.1)).inv
        (F.map k₁.snd.2)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map k₂.snd.1)).inv
        (F.map k₂.snd.2))