Also used the new simp lemmas to golf AlgebraicGeometry/ProjectiveSpectrum/*
AlgebraicGeometry/ProjectiveSpectrum/*