∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {ι : Sort u_1}
  (s : ι → X.Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (⨆ i, s i) =
    ⨆ i, (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (s i)