∀ {J : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} 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]
  [inst_4 : Small.{u_1, u_3} J] {i j : J} (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (F.map f)
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom ⋯))
        ((AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F).ι ((equivShrink J) j))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom ⋯))
        ((AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F).ι ((equivShrink J) i)))
      (((CategoryTheory.Functor.const J).obj (AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F).glued).map f)