chore(AlgebraicGeometry): Fix wrong names (#14021)

`PrimeSpectrum.IsPrime` -> `PrimeSpectrum.isPrime`
`PrimeSpectrum.vanishingIdeal_univ` -> `PrimeSpectrum.vanishingIdeal_empty`
`isAffineAffineScheme` -> `isAffine_affineScheme`
`SpecIsAffine` -> `isAffine_Spec`
`isAffineOfIso` -> `isAffine_of_isIso`
`rangeIsAffineOpenOfOpenImmersion` -> `isAffineOpen_opensRange`
`topIsAffineOpen` -> `isAffineOpen_top`
`Scheme.affineCoverIsAffine` -> `Scheme.isAffine_affineCover`
`Scheme.affineBasisCoverIsAffine` -> `Scheme.isAffine_affineBasisCover`
`IsAffineOpen.fromSpec_range` -> `IsAffineOpen.range_fromSpec`
`IsAffineOpen.imageIsOpenImmersion` -> `IsAffineOpen.image_of_isOpenImmersion`
`Scheme.quasi_compact_of_affine` -> `Scheme.compactSpace_of_isAffine`
`IsAffineOpen.fromSpec_base_preimage` -> `IsAffineOpen.fromSpec_preimage_self`
`IsAffineOpen.fromSpec_map_basicOpen'` -> `IsAffineOpen.fromSpec_preimage_basicOpen'`
`IsAffineOpen.fromSpec_map_basicOpen` -> `IsAffineOpen.fromSpec_preimage_basicOpen`
`IsAffineOpen.opensFunctor_map_basicOpen` -> `IsAffineOpen.fromSpec_image_basicOpen`
`IsAffineOpen.basicOpenIsAffine` -> `IsAffineOpen.basicOpen`
`IsAffineOpen.mapRestrictBasicOpen` -> `IsAffineOpen.ιOpens_preimage`
`AffineTargetMorphismProperty.IsLocal.targetAffineLocallyIsLocal` -> `AffineTargetMorphismProperty.IsLocal.targetAffineLocally_isLocal`
`AffineTargetMorphismProperty.IsLocal.targetAffineLocallyPullbackFstOfRightOfStableUnderBaseChange` -> `AffineTargetMorphismProperty.IsLocal.targetAffineLocally_pullback_fst_of_right_of_stableUnderBaseChange`
`diagonalTargetAffineLocallyOfOpenCover` -> `diagonal_targetAffineLocally_of_openCover`
`AffineTargetMorphismProperty.diagonalOfTargetAffineLocally` -> `AffineTargetMorphismProperty.diagonal_of_targetAffineLocally`
`universallyIsLocalAtTarget` -> `universally_isLocalAtTarget`
`universallyIsLocalAtTargetOfMorphismRestrict` -> `universally_isLocalAtTarget_of_morphismRestrict`
`bot_isAffineOpen` -> `isAffineOpen_bot`
`isOpenImmersion_is_local_at_target` -> `isOpenImmersion_isLocalAtTarget`
`QuasiCompact.is_local_at_target` -> `QuasiCompact.isLocalAtTarget`
`QuasiSeparated.is_local_at_target` -> `QuasiSeparated.isLocalAtTarget`
`universallyClosed_is_local_at_target` -> `universallyClosed_isLocalAtTarget`
`isReducedOfStalkIsReduced` -> `isReduced_of_isReduced_stalk`
`stalk_isReduced_of_reduced` -> `isReduced_stalk_of_isReduced`
`isReducedOfOpenImmersion` -> `isReduced_of_isOpenImmersion`
`isReducedOfIsAffineIsReduced` -> `isReduced_of_isAffine_isReduced`
`isReducedOfIsIntegral` -> `isReduced_of_isIntegral`
`is_irreducible_of_isIntegral` -> `irreducibleSpace_of_isIntegral`
`isIntegralOfIsIrreducibleIsReduced` -> `isIntegral_of_irreducibleSpace_of_isReduced`
`isIntegral_iff_is_irreducible_and_isReduced` -> `isIntegral_iff_irreducibleSpace_and_isReduced`
`isIntegralOfOpenImmersion` -> `isIntegral_of_isOpenImmersion`
`isIntegralOfIsAffineIsDomain` -> `isIntegral_of_isAffine_of_isDomain`

Author: erdOne

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -136,7 +136,7 @@ instance functionField_isFractionRing_of_affine (R : CommRingCat.{u}) [IsDomain
 instance {X : Scheme} [IsIntegral X] {U : Opens X.carrier} [hU : Nonempty U] :
     IsIntegral (X.restrict U.openEmbedding) :=
   haveI : Nonempty (X.restrict U.openEmbedding).carrier := hU
-  isIntegralOfOpenImmersion (X.ofRestrict U.openEmbedding)
+  isIntegral_of_isOpenImmersion (X.ofRestrict U.openEmbedding)
 
 theorem IsAffineOpen.primeIdealOf_genericPoint {X : Scheme} [IsIntegral X] {U : Opens X.carrier}
     (hU : IsAffineOpen U) [h : Nonempty U] :
@@ -161,7 +161,7 @@ theorem functionField_isFractionRing_of_isAffineOpen [IsIntegral X] (U : Opens X
   haveI : IsAffine _ := hU
   haveI : Nonempty (X.restrict U.openEmbedding).carrier := hU'
   haveI : IsIntegral (X.restrict U.openEmbedding) :=
-    @isIntegralOfIsAffineIsDomain _ _ _
+    @isIntegral_of_isAffine_of_isDomain _ _ _
       (by dsimp; rw [Opens.openEmbedding_obj_top]; infer_instance)
   delta IsFractionRing Scheme.functionField
   convert hU.isLocalization_stalk ⟨genericPoint X.carrier, _⟩ using 1
@@ -170,14 +170,14 @@ theorem functionField_isFractionRing_of_isAffineOpen [IsIntegral X] (U : Opens X
 #align algebraic_geometry.function_field_is_fraction_ring_of_is_affine_open AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen
 
 instance (x : X.carrier) : IsAffine (X.affineCover.obj x) :=
-  AlgebraicGeometry.SpecIsAffine _
+  AlgebraicGeometry.isAffine_Spec _
 
 instance [IsIntegral X] (x : X.carrier) :
     IsFractionRing (X.presheaf.stalk x) X.functionField :=
   let U : Opens X.carrier :=
     ⟨Set.range (X.affineCover.map x).1.base,
       PresheafedSpace.IsOpenImmersion.base_open.isOpen_range⟩
-  have hU : IsAffineOpen U := rangeIsAffineOpenOfOpenImmersion (X.affineCover.map x)
+  have hU : IsAffineOpen U := isAffineOpen_opensRange (X.affineCover.map x)
   let x : U := ⟨x, X.affineCover.Covers x⟩
   have : Nonempty U := ⟨x⟩
   let M := (hU.primeIdealOf x).asIdeal.primeCompl

Mathlib/AlgebraicGeometry/FunctionField.lean

@@ -44,7 +44,7 @@ instance : HasTerminal Scheme :=
   hasTerminal_of_hasTerminal_of_preservesLimit Scheme.Spec
 
 instance : IsAffine (⊤_ Scheme.{u}) :=
-  isAffineOfIso (PreservesTerminal.iso Scheme.Spec).inv
+  isAffine_of_isIso (PreservesTerminal.iso Scheme.Spec).inv
 
 instance : HasFiniteLimits Scheme :=
   hasFiniteLimits_of_hasTerminal_and_pullbacks
@@ -117,7 +117,7 @@ noncomputable def specPunitIsInitial : IsInitial (Scheme.Spec.obj (op <| CommRin
 #align algebraic_geometry.Spec_punit_is_initial AlgebraicGeometry.specPunitIsInitial
 
 instance (priority := 100) isAffine_of_isEmpty {X : Scheme} [IsEmpty X.carrier] : IsAffine X :=
-  isAffineOfIso
+  isAffine_of_isIso
     (inv (emptyIsInitial.to X) ≫ emptyIsInitial.to (Scheme.Spec.obj (op <| CommRingCat.of PUnit)))
 #align algebraic_geometry.is_affine_of_is_empty AlgebraicGeometry.isAffine_of_isEmpty
 
@@ -130,14 +130,14 @@ instance initial_isEmpty : IsEmpty (⊥_ Scheme).carrier :=
   ⟨fun x => ((initial.to Scheme.empty : _).1.base x).elim⟩
 #align algebraic_geometry.initial_is_empty AlgebraicGeometry.initial_isEmpty
 
-theorem bot_isAffineOpen (X : Scheme) : IsAffineOpen (⊥ : Opens X.carrier) := by
-  convert rangeIsAffineOpenOfOpenImmersion (initial.to X)
+theorem isAffineOpen_bot (X : Scheme) : IsAffineOpen (⊥ : Opens X.carrier) := by
+  convert isAffineOpen_opensRange (initial.to X)
   ext
   -- Porting note: added this `erw` to turn LHS to `False`
   erw [Set.mem_empty_iff_false]
   rw [false_iff_iff]
   exact fun x => isEmptyElim (show (⊥_ Scheme).carrier from x.choose)
-#align algebraic_geometry.bot_is_affine_open AlgebraicGeometry.bot_isAffineOpen
+#align algebraic_geometry.bot_is_affine_open AlgebraicGeometry.isAffineOpen_bot
 
 instance : HasStrictInitialObjects Scheme :=
   hasStrictInitialObjects_of_initial_is_strict fun A f => by infer_instance

Mathlib/AlgebraicGeometry/Limits.lean

@@ -50,7 +50,7 @@ theorem isOpenImmersion_respectsIso : MorphismProperty.RespectsIso @IsOpenImmers
   infer_instance
 #align algebraic_geometry.is_open_immersion_respects_iso AlgebraicGeometry.isOpenImmersion_respectsIso
 
-theorem isOpenImmersion_is_local_at_target : PropertyIsLocalAtTarget @IsOpenImmersion := by
+theorem isOpenImmersion_isLocalAtTarget : PropertyIsLocalAtTarget @IsOpenImmersion := by
   constructor
   · exact isOpenImmersion_respectsIso
   · intros; infer_instance
@@ -72,7 +72,7 @@ theorem isOpenImmersion_is_local_at_target : PropertyIsLocalAtTarget @IsOpenImme
         (isOpenImmersion_respectsIso.arrow_iso_iff
           (morphismRestrictOpensRange f (𝒰.map _))).mpr (H _)
       infer_instance
-#align algebraic_geometry.is_open_immersion_is_local_at_target AlgebraicGeometry.isOpenImmersion_is_local_at_target
+#align algebraic_geometry.is_open_immersion_is_local_at_target AlgebraicGeometry.isOpenImmersion_isLocalAtTarget
 
 theorem IsOpenImmersion.openCover_TFAE {X Y : Scheme.{u}} (f : X ⟶ Y) : List.TFAE
     [IsOpenImmersion f,
@@ -85,13 +85,13 @@ theorem IsOpenImmersion.openCover_TFAE {X Y : Scheme.{u}} (f : X ⟶ Y) : List.T
       IsOpenImmersion (pullback.snd : pullback f g ⟶ _),
     ∃ (ι : Type u) (U : ι → Opens Y.carrier) (_ : iSup U = ⊤),
       ∀ i, IsOpenImmersion (f ∣_ U i)] :=
-  isOpenImmersion_is_local_at_target.openCover_TFAE f
+  isOpenImmersion_isLocalAtTarget.openCover_TFAE f
 #align algebraic_geometry.is_open_immersion.open_cover_tfae AlgebraicGeometry.IsOpenImmersion.openCover_TFAE
 
 theorem IsOpenImmersion.openCover_iff {X Y : Scheme.{u}} (𝒰 : Scheme.OpenCover.{u} Y)
     (f : X ⟶ Y) :
     IsOpenImmersion f ↔ ∀ i, IsOpenImmersion (pullback.snd : pullback f (𝒰.map i) ⟶ _) :=
-  isOpenImmersion_is_local_at_target.openCover_iff f 𝒰
+  isOpenImmersion_isLocalAtTarget.openCover_iff f 𝒰
 #align algebraic_geometry.is_open_immersion.open_cover_iff AlgebraicGeometry.IsOpenImmersion.openCover_iff
 
 theorem isOpenImmersion_stableUnderBaseChange :

Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

@@ -88,7 +88,7 @@ theorem isCompact_open_iff_eq_basicOpen_union {X : Scheme} [IsAffine X] (U : Set
       ∃ s : Set (X.presheaf.obj (op ⊤)),
         s.Finite ∧ U = ⋃ (i : X.presheaf.obj (op ⊤)) (_ : i ∈ s), X.basicOpen i :=
   (isBasis_basicOpen X).isCompact_open_iff_eq_finite_iUnion _
-    (fun _ => ((topIsAffineOpen _).basicOpenIsAffine _).isCompact) _
+    (fun _ => ((isAffineOpen_top _).basicOpen _).isCompact) _
 #align algebraic_geometry.is_compact_open_iff_eq_basic_open_union AlgebraicGeometry.isCompact_open_iff_eq_basicOpen_union
 
 theorem quasiCompact_iff_forall_affine :
@@ -136,7 +136,7 @@ theorem isCompact_basicOpen (X : Scheme) {U : Opens X.carrier} (hU : IsCompact (
       convert Set.subset_iUnion₂ (s := fun (U : X.affineOpens) (_ : U ∈ s) => (U : Set X.carrier))
         V V.prop using 1
     erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op]
-    exact IsAffineOpen.basicOpenIsAffine V.1.prop _
+    exact IsAffineOpen.basicOpen V.1.prop _
   haveI : Finite s := hs.to_subtype
   refine ⟨Set.range g, Set.finite_range g, ?_⟩
   refine (Set.inter_eq_right.mpr
@@ -176,7 +176,7 @@ theorem QuasiCompact.affineProperty_isLocal : (QuasiCompact.affineProperty : _).
       dsimp [Opens.map]
       simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk, Set.preimage_iUnion]
       exact isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i)
-    · exact topIsAffineOpen _
+    · exact isAffineOpen_top _
 #align algebraic_geometry.quasi_compact.affine_property_is_local AlgebraicGeometry.QuasiCompact.affineProperty_isLocal
 
 theorem QuasiCompact.affine_openCover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) :
@@ -193,10 +193,10 @@ theorem QuasiCompact.affine_openCover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) :
   quasiCompact_eq_affineProperty.symm ▸ QuasiCompact.affineProperty_isLocal.affine_openCover_TFAE f
 #align algebraic_geometry.quasi_compact.affine_open_cover_tfae AlgebraicGeometry.QuasiCompact.affine_openCover_tfae
 
-theorem QuasiCompact.is_local_at_target : PropertyIsLocalAtTarget @QuasiCompact :=
+theorem QuasiCompact.isLocalAtTarget : PropertyIsLocalAtTarget @QuasiCompact :=
   quasiCompact_eq_affineProperty.symm ▸
-    QuasiCompact.affineProperty_isLocal.targetAffineLocallyIsLocal
-#align algebraic_geometry.quasi_compact.is_local_at_target AlgebraicGeometry.QuasiCompact.is_local_at_target
+    QuasiCompact.affineProperty_isLocal.targetAffineLocally_isLocal
+#align algebraic_geometry.quasi_compact.is_local_at_target AlgebraicGeometry.QuasiCompact.isLocalAtTarget
 
 theorem QuasiCompact.openCover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) :
     List.TFAE
@@ -210,7 +210,7 @@ theorem QuasiCompact.openCover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) :
           QuasiCompact (pullback.snd : pullback f g ⟶ _),
         ∃ (ι : Type u) (U : ι → Opens Y.carrier) (_ : iSup U = ⊤), ∀ i, QuasiCompact (f ∣_ U i)] :=
   quasiCompact_eq_affineProperty.symm ▸
-    QuasiCompact.affineProperty_isLocal.targetAffineLocallyIsLocal.openCover_TFAE f
+    QuasiCompact.affineProperty_isLocal.targetAffineLocally_isLocal.openCover_TFAE f
 #align algebraic_geometry.quasi_compact.open_cover_tfae AlgebraicGeometry.QuasiCompact.openCover_tfae
 
 theorem quasiCompact_over_affine_iff {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] :
@@ -232,7 +232,7 @@ theorem QuasiCompact.affine_openCover_iff {X Y : Scheme.{u}} (𝒰 : Scheme.Open
 theorem QuasiCompact.openCover_iff {X Y : Scheme.{u}} (𝒰 : Scheme.OpenCover.{u} Y) (f : X ⟶ Y) :
     QuasiCompact f ↔ ∀ i, QuasiCompact (pullback.snd : pullback f (𝒰.map i) ⟶ _) :=
   quasiCompact_eq_affineProperty.symm ▸
-    QuasiCompact.affineProperty_isLocal.targetAffineLocallyIsLocal.openCover_iff f 𝒰
+    QuasiCompact.affineProperty_isLocal.targetAffineLocally_isLocal.openCover_iff f 𝒰
 #align algebraic_geometry.quasi_compact.open_cover_iff AlgebraicGeometry.QuasiCompact.openCover_iff
 
 theorem quasiCompact_respectsIso : MorphismProperty.RespectsIso @QuasiCompact :=

Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

@@ -109,8 +109,8 @@ theorem quasi_compact_affineProperty_iff_quasiSeparatedSpace {X Y : Scheme} [IsA
     simp_rw [isCompact_iff_compactSpace] at H
     exact
       @Homeomorph.compactSpace _ _ _ _
-        (H ⟨⟨_, h₁.base_open.isOpen_range⟩, rangeIsAffineOpenOfOpenImmersion _⟩
-          ⟨⟨_, h₂.base_open.isOpen_range⟩, rangeIsAffineOpenOfOpenImmersion _⟩)
+        (H ⟨⟨_, h₁.base_open.isOpen_range⟩, isAffineOpen_opensRange _⟩
+          ⟨⟨_, h₂.base_open.isOpen_range⟩, isAffineOpen_opensRange _⟩)
         e.symm
 #align algebraic_geometry.quasi_compact_affine_property_iff_quasi_separated_space AlgebraicGeometry.quasi_compact_affineProperty_iff_quasiSeparatedSpace
 
@@ -186,10 +186,10 @@ theorem QuasiSeparated.affine_openCover_TFAE {X Y : Scheme.{u}} (f : X ⟶ Y) :
   exact this
 #align algebraic_geometry.quasi_separated.affine_open_cover_tfae AlgebraicGeometry.QuasiSeparated.affine_openCover_TFAE
 
-theorem QuasiSeparated.is_local_at_target : PropertyIsLocalAtTarget @QuasiSeparated :=
+theorem QuasiSeparated.isLocalAtTarget : PropertyIsLocalAtTarget @QuasiSeparated :=
   quasiSeparated_eq_affineProperty_diagonal.symm ▸
-    QuasiCompact.affineProperty_isLocal.diagonal.targetAffineLocallyIsLocal
-#align algebraic_geometry.quasi_separated.is_local_at_target AlgebraicGeometry.QuasiSeparated.is_local_at_target
+    QuasiCompact.affineProperty_isLocal.diagonal.targetAffineLocally_isLocal
+#align algebraic_geometry.quasi_separated.is_local_at_target AlgebraicGeometry.QuasiSeparated.isLocalAtTarget
 
 open List in
 theorem QuasiSeparated.openCover_TFAE {X Y : Scheme.{u}} (f : X ⟶ Y) :
@@ -204,7 +204,7 @@ theorem QuasiSeparated.openCover_TFAE {X Y : Scheme.{u}} (f : X ⟶ Y) :
           QuasiSeparated (pullback.snd : pullback f g ⟶ _),
         ∃ (ι : Type u) (U : ι → Opens Y.carrier) (_ : iSup U = ⊤),
           ∀ i, QuasiSeparated (f ∣_ U i)] :=
-  QuasiSeparated.is_local_at_target.openCover_TFAE f
+  QuasiSeparated.isLocalAtTarget.openCover_TFAE f
 #align algebraic_geometry.quasi_separated.open_cover_tfae AlgebraicGeometry.QuasiSeparated.openCover_TFAE
 
 theorem quasiSeparated_over_affine_iff {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] :
@@ -228,7 +228,7 @@ theorem QuasiSeparated.affine_openCover_iff {X Y : Scheme.{u}} (𝒰 : Scheme.Op
 
 theorem QuasiSeparated.openCover_iff {X Y : Scheme.{u}} (𝒰 : Scheme.OpenCover.{u} Y) (f : X ⟶ Y) :
     QuasiSeparated f ↔ ∀ i, QuasiSeparated (pullback.snd : pullback f (𝒰.map i) ⟶ _) :=
-  QuasiSeparated.is_local_at_target.openCover_iff f 𝒰
+  QuasiSeparated.isLocalAtTarget.openCover_iff f 𝒰
 #align algebraic_geometry.quasi_separated.open_cover_iff AlgebraicGeometry.QuasiSeparated.openCover_iff
 
 instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiSeparated g] :
@@ -265,7 +265,7 @@ instance quasiSeparatedSpace_of_isAffine (X : Scheme) [IsAffine X] :
   intro i' _
   change IsCompact (X.basicOpen i ⊓ X.basicOpen i').1
   rw [← Scheme.basicOpen_mul]
-  exact ((topIsAffineOpen _).basicOpenIsAffine _).isCompact
+  exact ((isAffineOpen_top _).basicOpen _).isCompact
 #align algebraic_geometry.quasi_separated_space_of_is_affine AlgebraicGeometry.quasiSeparatedSpace_of_isAffine
 
 theorem IsAffineOpen.isQuasiSeparated {X : Scheme} {U : Opens X.carrier} (hU : IsAffineOpen U) :

Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

@@ -197,7 +197,7 @@ theorem affineLocally_iff_affineOpens_le
       · simp only [Scheme.ofRestrict_val_c_app, Scheme.restrict_presheaf_map, ← X.presheaf.map_comp]
         congr 1
   · intro H V
-    specialize H ⟨_, V.2.imageIsOpenImmersion (X.ofRestrict _)⟩ (Subtype.coe_image_subset _ _)
+    specialize H ⟨_, V.2.image_of_isOpenImmersion (X.ofRestrict _)⟩ (Subtype.coe_image_subset _ _)
     rw [← hP.cancel_right_isIso _ (X.presheaf.map (eqToHom _)), Category.assoc]
     · convert H
       simp only [Scheme.ofRestrict_val_c_app, Scheme.restrict_presheaf_map, ← X.presheaf.map_comp]
@@ -211,12 +211,12 @@ theorem scheme_restrict_basicOpen_of_localizationPreserves (h₁ : RingHom.Respe
     (U : (X.restrict ((Opens.map f.1.base).obj <| Y.basicOpen r).openEmbedding).affineOpens) :
     P (Scheme.Γ.map ((X.restrict ((Opens.map f.1.base).obj <|
       Y.basicOpen r).openEmbedding).ofRestrict U.1.openEmbedding ≫ f ∣_ Y.basicOpen r).op) := by
-  specialize H ⟨_, U.2.imageIsOpenImmersion (X.ofRestrict _)⟩
+  specialize H ⟨_, U.2.image_of_isOpenImmersion (X.ofRestrict _)⟩
   letI i1 : Algebra (Y.presheaf.obj <| Opposite.op ⊤) (Localization.Away r) := Localization.algebra
   exact (h₁.ofRestrict_morphismRestrict_iff f r
     ((Scheme.Hom.opensFunctor
       (X.ofRestrict ((Opens.map f.1.base).obj <| Y.basicOpen r).openEmbedding)).obj U.1)
-    (IsAffineOpen.imageIsOpenImmersion U.2
+    (IsAffineOpen.image_of_isOpenImmersion U.2
       (X.ofRestrict ((Opens.map f.1.base).obj <| Y.basicOpen r).openEmbedding))
     (Opens.ext (Set.preimage_image_eq _ Subtype.coe_injective).symm)).mpr (h₂.away r H)
 set_option linter.uppercaseLean3 false in
@@ -242,7 +242,7 @@ theorem sourceAffineLocally_isLocal (h₁ : RingHom.RespectsIso @P)
         intro V hV
         rw [Scheme.preimage_basicOpen] at hV
         subst hV
-        exact U.2.mapRestrictBasicOpen (Scheme.Γ.map f.op r.1)
+        exact U.2.ιOpens_preimage (Scheme.Γ.map f.op r.1)
 #align algebraic_geometry.source_affine_locally_is_local AlgebraicGeometry.sourceAffineLocally_isLocal
 
 variable (hP : RingHom.PropertyIsLocal @P)
@@ -274,7 +274,7 @@ theorem isOpenImmersionCat_comp_of_sourceAffineLocally (h₁ : RingHom.RespectsI
   rw [← h₁.cancel_right_isIso _
     (Scheme.Γ.map (IsOpenImmersion.isoOfRangeEq (Y.ofRestrict _) f _).hom.op),
     ← Functor.map_comp, ← op_comp]
-  · convert h₂ ⟨_, rangeIsAffineOpenOfOpenImmersion f⟩ using 3
+  · convert h₂ ⟨_, isAffineOpen_opensRange f⟩ using 3
     · rw [IsOpenImmersion.isoOfRangeEq_hom_fac_assoc]
       exact Subtype.range_coe
 #align algebraic_geometry.is_open_immersion_comp_of_source_affine_locally AlgebraicGeometry.isOpenImmersionCat_comp_of_sourceAffineLocally
@@ -291,7 +291,7 @@ theorem sourceAffineLocally_of_source_openCover {X Y : Scheme.{u}} (f : X ⟶ Y)
     (𝒰 : X.OpenCover) [∀ i, IsAffine (𝒰.obj i)] (H : ∀ i, P (Scheme.Γ.map (𝒰.map i ≫ f).op)) :
     sourceAffineLocally (@P) f := by
   let S i := (⟨⟨Set.range (𝒰.map i).1.base, (𝒰.IsOpen i).base_open.isOpen_range⟩,
-    rangeIsAffineOpenOfOpenImmersion (𝒰.map i)⟩ : X.affineOpens)
+    isAffineOpen_opensRange (𝒰.map i)⟩ : X.affineOpens)
   intro U
   -- Porting note: here is what we are eliminating into Lean
   apply of_affine_open_cover
@@ -360,7 +360,7 @@ theorem affine_openCover_TFAE {X Y : Scheme.{u}} [IsAffine Y] (f : X ⟶ Y) :
           P (Scheme.Γ.map (g ≫ f).op)] := by
   tfae_have 1 → 4
   · intro H U g _ hg
-    specialize H ⟨⟨_, hg.base_open.isOpen_range⟩, rangeIsAffineOpenOfOpenImmersion g⟩
+    specialize H ⟨⟨_, hg.base_open.isOpen_range⟩, isAffineOpen_opensRange g⟩
     rw [← hP.respectsIso.cancel_right_isIso _ (Scheme.Γ.map (IsOpenImmersion.isoOfRangeEq g
       (X.ofRestrict (Opens.openEmbedding ⟨_, hg.base_open.isOpen_range⟩))
       Subtype.range_coe.symm).hom.op),
@@ -446,7 +446,7 @@ theorem isLocal_sourceAffineLocally : (sourceAffineLocally @P).IsLocal :=
 #align ring_hom.property_is_local.is_local_source_affine_locally RingHom.PropertyIsLocal.isLocal_sourceAffineLocally
 
 theorem is_local_affineLocally : PropertyIsLocalAtTarget (affineLocally @P) :=
-  hP.isLocal_sourceAffineLocally.targetAffineLocallyIsLocal
+  hP.isLocal_sourceAffineLocally.targetAffineLocally_isLocal
 #align ring_hom.property_is_local.is_local_affine_locally RingHom.PropertyIsLocal.is_local_affineLocally
 
 theorem affine_openCover_iff {X Y : Scheme.{u}} (f : X ⟶ Y) (𝒰 : Scheme.OpenCover.{u} Y)

Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

@@ -85,19 +85,19 @@ instance universallyClosedSnd {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hf :
   universallyClosed_stableUnderBaseChange.snd f g hf
 #align algebraic_geometry.universally_closed_snd AlgebraicGeometry.universallyClosedSnd
 
-theorem universallyClosed_is_local_at_target : PropertyIsLocalAtTarget @UniversallyClosed := by
+theorem universallyClosed_isLocalAtTarget : PropertyIsLocalAtTarget @UniversallyClosed := by
   rw [universallyClosed_eq]
-  apply universallyIsLocalAtTargetOfMorphismRestrict
+  apply universally_isLocalAtTarget_of_morphismRestrict
   · exact topologically_isClosedMap_respectsIso
   · intro X Y f ι U hU H
     simp_rw [topologically, morphismRestrict_base] at H
     exact (isClosedMap_iff_isClosedMap_of_iSup_eq_top hU).mpr H
-#align algebraic_geometry.universally_closed_is_local_at_target AlgebraicGeometry.universallyClosed_is_local_at_target
+#align algebraic_geometry.universally_closed_is_local_at_target AlgebraicGeometry.universallyClosed_isLocalAtTarget
 
 theorem UniversallyClosed.openCover_iff {X Y : Scheme.{u}} (f : X ⟶ Y)
     (𝒰 : Scheme.OpenCover.{u} Y) :
     UniversallyClosed f ↔ ∀ i, UniversallyClosed (pullback.snd : pullback f (𝒰.map i) ⟶ _) :=
-  universallyClosed_is_local_at_target.openCover_iff f 𝒰
+  universallyClosed_isLocalAtTarget.openCover_iff f 𝒰
 #align algebraic_geometry.universally_closed.open_cover_iff AlgebraicGeometry.UniversallyClosed.openCover_iff
 
 end AlgebraicGeometry