∀ (P P_1 : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (e_P : P = P_1) [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative], AlgebraicGeometry.Scheme.pretopology P = AlgebraicGeometry.Scheme.pretopology P_1