∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] (U : ↑Y.affineOpens),
  (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.fromNormalization f).base).obj ↑U =
    AlgebraicGeometry.Scheme.Hom.opensRange ((AlgebraicGeometry.Scheme.Hom.normalizationOpenCover f).f U)