∀ {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]
  (s : CategoryTheory.Limits.Cocone (F.comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace))
  (m :
    (AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.mapCocone
          (AlgebraicGeometry.Scheme.IsLocallyDirected.cocone F)).pt ⟶
      s.pt),
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp
          ((AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.mapCocone
                  (AlgebraicGeometry.Scheme.IsLocallyDirected.cocone F)).ι.app
            j)
          m =
        s.ι.app j) →
    m =
      CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F).isoLocallyRingedSpace.hom
        (CategoryTheory.Limits.Multicoequalizer.desc
          (AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F).toLocallyRingedSpaceGlueData.diagram s.pt
          (fun i => s.ι.app ((equivShrink J).symm i)) ⋯)