∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} 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_2, u_1} J] (x : J),
  x = (equivShrink J).symm (((equivShrink J).trans (Equiv.uniqueSigma fun x => Shrink.{u_2, u_1} J).symm) x).snd