∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f]
  [AlgebraicGeometry.QuasiCompact f] (y : ↥Y),
  AlgebraicGeometry.IsArtinianScheme (AlgebraicGeometry.Scheme.Hom.fiber f y)