∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  [inst_2 : Small.{u, u_1} 𝒰.I₀] [inst_3 : Quiver.IsThin 𝒰.I₀] (i : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι d.functor i)
      (CategoryTheory.CategoryStruct.comp d.toBase h) =
    CategoryTheory.CategoryStruct.comp (d.natTrans.app i) (CategoryTheory.CategoryStruct.comp (𝒰.f i) h)