∀ {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)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J] (i j : J) {k : J}
  (fi : k ⟶ i) (fj : k ⟶ j) {Z : AlgebraicGeometry.Scheme} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.obj i).homOfLE ⋯)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IsLocallyDirected.tAux F i j) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map fi)).inv
      (CategoryTheory.CategoryStruct.comp (F.map fj) h)