diff --git a/Pi1/FundamentalGroup/AffineAnd.lean b/Pi1/FundamentalGroup/AffineAnd.lean
index 22bd3dd..01dd181 100644
--- a/Pi1/FundamentalGroup/AffineAnd.lean
+++ b/Pi1/FundamentalGroup/AffineAnd.lean
@@ -351,21 +351,21 @@ def _root_.AlgebraicGeometry.IsAffineOpen.ΓProp
     exact (this U hU).2
   map {X Y} f := MorphismProperty.Under.homMk
       (f.unop.left.appLE (X.unop.hom ⁻¹ᵁ U) (Y.unop.hom ⁻¹ᵁ U)
-      (by rw [← Scheme.preimage_comp, CategoryTheory.Over.w])) <| by
-    simp [Scheme.Hom.app_eq_appLE, Scheme.appLE_comp_appLE]
+      (by rw [← Scheme.Hom.comp_preimage, CategoryTheory.Over.w])) <| by
+    simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_comp_appLE]
   map_id X := by
     ext : 1
     simp only [Functor.id_obj, Functor.const_obj_obj,
       Scheme.Hom.appLE,
       homOfLE_leOfHom, homOfLE_refl, op_id, unop_id, Comma.id_hom,
-      CategoryTheory.Comma.id_left, Scheme.id.base, Scheme.id_app, Category.id_comp,
+      CategoryTheory.Comma.id_left, Scheme.Hom.id_app, Category.id_comp,
       Under.homMk_hom, Under.homMk_right, CategoryTheory.Comma.id_right]
     apply CategoryTheory.Functor.map_id
   map_comp {X Y Z} f g := by
     ext : 1
     show Scheme.Hom.appLE (g.unop.left ≫ f.unop.left) _ _ _ =
       Scheme.Hom.appLE _ _ _ _ ≫ Scheme.Hom.appLE _ _ _ _
-    rw [Scheme.appLE_comp_appLE]
+    rw [Scheme.Hom.appLE_comp_appLE]
 
 @[simps! obj_hom]
 def ΓProp (hQi : RingHom.RespectsIso Q) (S : Scheme.{u}) [IsAffine S] :
diff --git a/Pi1/FundamentalGroup/Galois.lean b/Pi1/FundamentalGroup/Galois.lean
index 32b40af..7cf6bbb 100644
--- a/Pi1/FundamentalGroup/Galois.lean
+++ b/Pi1/FundamentalGroup/Galois.lean
@@ -370,7 +370,7 @@ def forgetInventIso [IsSepClosed Ω] : 𝟭 (FiniteEtale _) ≅ forgetScheme Ω
         MorphismProperty.Comma.comp_hom, Comma.comp_left,
         MorphismProperty.Over.isoMk_hom_left, Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom,
         Iso.symm_hom, RingEquiv.toCommRingCatIso_inv, Scheme.Spec_map, Quiver.Hom.unop_op,
-        Functor.comp_map, inventScheme_map, forgetScheme_map_hom, MorphismProperty.Over.homMk_hom,
+        Functor.comp_map, inventScheme_map, MorphismProperty.Over.homMk_hom,
         Over.homMk_left, Category.assoc]
       simp only [IsFiniteEtale.isoSpecPi, Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom,
         RingEquiv.toCommRingCatIso_hom, Scheme.Spec_map, Quiver.Hom.unop_op, Category.assoc]
@@ -402,7 +402,7 @@ def forgetInventIso [IsSepClosed Ω] : 𝟭 (FiniteEtale _) ≅ forgetScheme Ω
       rw [← FintypeCat.hom_apply]
       dsimp [- FintypeCat.hom_apply]
       rw [← Scheme.Hom.comp_apply, ← Scheme.isoSpec_inv_naturality]
-      simp only [Scheme.comp_coeBase, TopCat.hom_comp, ContinuousMap.comp_apply]
+      simp only [Scheme.Hom.comp_base, TopCat.hom_comp, ContinuousMap.comp_apply]
       rfl
 
 def equivFintypeCat [IsSepClosed Ω] : FiniteEtale (Spec <| .of Ω) ≌ FintypeCat.{u} :=
@@ -428,7 +428,7 @@ instance [IsSepClosed Ω] : PreservesFiniteLimits (pullback ξ) := by
 
 instance (X : Type*) [TopologicalSpace X] [LocallyConnectedSpace X] :
     DiscreteTopology (ConnectedComponents X) := by
-  rw [← singletons_open_iff_discrete]
+  rw [discreteTopology_iff_isOpen_singleton]
   intro i
   obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe i
   rw [← ConnectedComponents.isQuotientMap_coe.isOpen_preimage,
@@ -533,7 +533,7 @@ instance [ConnectedSpace X] (Y : FiniteEtale X) :
     dsimp
     infer_instance
   exact Y.hom.isOpenMap.finite_connectedComponents_of_finite_preimage_singleton Y.hom.continuous
-    Y.hom.isClosedMap (fun y ↦ IsFinite.finite_preimage_singleton _ y)
+    Y.hom.isClosedMap (fun y ↦ Scheme.Hom.finite_preimage_singleton _ y)
 
 open MorphismProperty
 
diff --git a/Pi1/FundamentalGroup/Point.lean b/Pi1/FundamentalGroup/Point.lean
index 8f8e188..ee0cc6e 100644
--- a/Pi1/FundamentalGroup/Point.lean
+++ b/Pi1/FundamentalGroup/Point.lean
@@ -209,7 +209,7 @@ def homEquivAlgHom (X : FiniteEtale (Spec (.of k))) :
         have := congr((CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of K)).hom)
           ($(Over.w x).appTop.hom
             ((Scheme.ΓSpecIso (CommRingCat.of k)).commRingCatIsoToRingEquiv.symm a)))
-        dsimp only [Functor.const_obj_obj, Over.mk_left, Scheme.comp_app,
+        dsimp only [Functor.const_obj_obj, Over.mk_left, Scheme.Hom.comp_app,
           TopologicalSpace.Opens.map_top, CommRingCat.hom_comp, RingHom.coe_comp,
           Function.comp_apply, Functor.id_obj, Over.mk_hom] at this
         dsimp only [Over.mk_left, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe,
@@ -217,7 +217,7 @@ def homEquivAlgHom (X : FiniteEtale (Spec (.of k))) :
         rw [RingHom.algebraMap_toAlgebra]
         dsimp [Scheme.Hom.appTop]
         convert this
-        · simp [Scheme.Hom.appLE, Scheme.Hom.appTop]
+        · simp [Scheme.Hom.appLE]
         · dsimp [Iso.commRingCatIsoToRingEquiv]
           rw [← CommRingCat.comp_apply]
           rw [← CommRingCat.comp_apply]
@@ -256,7 +256,7 @@ lemma homEquivAlgHom_smul (X : FiniteEtale (Spec (.of k))) [IsConnected X] (g :
     (homEquivAlgHom k K X) (g • x) = g • (homEquivAlgHom k K X x) := by
   rw [homEquivAlgHom]
   dsimp only [Over.mk_left, AlgHom.toRingHom_eq_coe, Equiv.coe_fn_mk, algEquiv_smul_hom,
-    Scheme.comp_app, TopologicalSpace.Opens.map_top, CommRingCat.hom_comp]
+    Scheme.Hom.comp_app, TopologicalSpace.Opens.map_top, CommRingCat.hom_comp]
   rw [AlgEquiv.smul_algHom_def]
   ext1 a
   dsimp only [AlgHom.coe_mk, RingHom.coe_comp, Function.comp_apply, AlgHom.coe_comp, AlgHom.coe_coe]
diff --git a/Pi1/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean b/Pi1/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
index 2cdf05d..e220d26 100644
--- a/Pi1/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
+++ b/Pi1/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
@@ -10,18 +10,18 @@ namespace AlgebraicGeometry
 instance : (topologically IsOpenMap).RespectsIso :=
   topologically_respectsIso _ (fun f ↦ f.isOpenMap) (fun _ _ hf hg ↦ hg.comp hf)
 
-instance : IsLocalAtSource (topologically IsOpenMap) :=
-  topologically_isLocalAtSource' (fun _ ↦ _) fun _ _ _ hU _ ↦ hU.isOpenMap_iff_comp
+instance : IsZariskiLocalAtSource (topologically IsOpenMap) :=
+  topologically_isZariskiLocalAtSource' (fun _ ↦ _) fun _ _ _ hU _ ↦ hU.isOpenMap_iff_comp
 
 instance : (topologically GeneralizingMap).RespectsIso :=
   topologically_respectsIso _ (fun f ↦ f.isOpenEmbedding.generalizingMap
     f.isOpenEmbedding.isOpen_range.stableUnderGeneralization) (fun _ _ hf hg ↦ hf.comp hg)
 
-instance : IsLocalAtSource (topologically GeneralizingMap) :=
-  topologically_isLocalAtSource' (fun _ ↦ _) fun _ _ _ hU _ ↦ hU.generalizingMap_iff_comp
+instance : IsZariskiLocalAtSource (topologically GeneralizingMap) :=
+  topologically_isZariskiLocalAtSource' (fun _ ↦ _) fun _ _ _ hU _ ↦ hU.generalizingMap_iff_comp
 
-instance : IsLocalAtTarget (topologically GeneralizingMap) :=
-  topologically_isLocalAtTarget' (fun _ ↦ _) fun _ _ _ hU _ ↦
+instance : IsZariskiLocalAtTarget (topologically GeneralizingMap) :=
+  topologically_isZariskiLocalAtTarget' (fun _ ↦ _) fun _ _ _ hU _ ↦
     hU.generalizingMap_iff_restrictPreimage
 
 section Surjective
diff --git a/Pi1/Mathlib/AlgebraicGeometry/PullbackCarrier.lean b/Pi1/Mathlib/AlgebraicGeometry/PullbackCarrier.lean
index ca87505..1885a1e 100644
--- a/Pi1/Mathlib/AlgebraicGeometry/PullbackCarrier.lean
+++ b/Pi1/Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@@ -13,14 +13,15 @@ lemma exists_preimage_of_isPullback {P X Y Z : Scheme.{u}} {fst : P ⟶ X} {snd
   let e := h.isoPullback
   obtain ⟨z, hzl, hzr⟩ := AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback x y hxy
   use h.isoPullback.inv.base z
-  simp [← Scheme.comp_base_apply, hzl, hzr]
+  simp [← Scheme.Hom.comp_apply, hzl, hzr]
 
 lemma image_preimage_eq_of_isPullback {P X Y Z : Scheme.{u}} {fst : P ⟶ X} {snd : P ⟶ Y}
     {f : X ⟶ Z} {g : Y ⟶ Z} (h : IsPullback fst snd f g) (s : Set X) :
     snd.base '' (fst.base ⁻¹' s) = g.base ⁻¹' (f.base '' s) := by
   refine subset_antisymm ?_ (fun x hx ↦ ?_)
-  · rw [Set.image_subset_iff, ← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.comp_base, ← h.1.1]
-    rw [Scheme.comp_base, TopCat.coe_comp, ← Set.image_subset_iff, Set.image_comp]
+  · rw [Set.image_subset_iff, ← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base,
+        ← h.1.1]
+    rw [Scheme.Hom.comp_base, TopCat.coe_comp, ← Set.image_subset_iff, Set.image_comp]
     exact Set.image_mono (Set.image_preimage_subset _ _)
   · obtain ⟨y, hy, heq⟩ := hx
     obtain ⟨o, hl, hr⟩ := exists_preimage_of_isPullback h y x heq
diff --git a/Pi1/Mathlib/RingTheory/Etale/Basic.lean b/Pi1/Mathlib/RingTheory/Etale/Basic.lean
index 388ee88..872ddf3 100644
--- a/Pi1/Mathlib/RingTheory/Etale/Basic.lean
+++ b/Pi1/Mathlib/RingTheory/Etale/Basic.lean
@@ -12,10 +12,10 @@ instance (R S : Type u) [CommRing R] [CommRing S] :
     letI : Algebra (R × S) S := (RingHom.snd R S).toAlgebra
     Algebra.Etale (R × S) S := by
   algebraize [RingHom.snd R S]
-  exact Algebra.Etale.of_isLocalization_Away (0, 1)
+  exact Algebra.Etale.of_isLocalizationAway (0, 1)
 
 instance (R S : Type u) [CommRing R] [CommRing S] :
     letI : Algebra (R × S) R := (RingHom.fst R S).toAlgebra
     Algebra.Etale (R × S) R := by
   algebraize [RingHom.fst R S]
-  exact Algebra.Etale.of_isLocalization_Away (1, 0)
+  exact Algebra.Etale.of_isLocalizationAway (1, 0)
diff --git a/Pi1/RingTheory/FiniteEtale/Equalizer.lean b/Pi1/RingTheory/FiniteEtale/Equalizer.lean
index f65d3a7..b767cd2 100644
--- a/Pi1/RingTheory/FiniteEtale/Equalizer.lean
+++ b/Pi1/RingTheory/FiniteEtale/Equalizer.lean
@@ -107,7 +107,7 @@ lemma Algebra.exists_cover_rankAtStalk_eq {R : Type*} (S : Type*) [CommRing R] [
   apply heq
   apply hrU
   simp only [PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Set.mem_compl_iff,
-    PrimeSpectrum.mem_zeroLocus, Ideal.coe_comap, Set.singleton_subset_iff, Set.mem_preimage,
+    PrimeSpectrum.mem_zeroLocus, Set.singleton_subset_iff,
     SetLike.mem_coe]
   obtain ⟨-, b⟩ := (IsLocalization.isPrime_iff_isPrime_disjoint (.powers r) _ q.asIdeal).mp q.2
   rw [Set.disjoint_left] at b
diff --git a/Pi1/RingTheory/RingOfDefinition.lean b/Pi1/RingTheory/RingOfDefinition.lean
index 2da73e7..c42ac78 100644
--- a/Pi1/RingTheory/RingOfDefinition.lean
+++ b/Pi1/RingTheory/RingOfDefinition.lean
@@ -93,7 +93,7 @@ lemma exists_preimage_of_coefficients' (f : R →+* S) (t : MvPolynomial ι S)
   choose c h1 h2 using this
   let p : (ι →₀ ℕ) →₀ R := Finsupp.ofSupportFinite c <| by
     apply Set.Finite.subset
-    · exact Finsupp.finite_support t
+    · exact Finsupp.hasFiniteSupport t
     · intro m minc h
       exact minc (h2 m h)
   use p
@@ -119,7 +119,7 @@ lemma exists_preimage_of_coefficients (t : MvPolynomial ι S)
   choose c h1 h2 using this
   let p : (ι →₀ ℕ) →₀ R := Finsupp.ofSupportFinite c <| by
     apply Set.Finite.subset
-    · exact Finsupp.finite_support t
+    · exact Finsupp.hasFiniteSupport t
     · intro m minc h
       exact minc (h2 m h)
   use p
diff --git a/Pi1/RingTheory/RingOfDefinition/Utils.lean b/Pi1/RingTheory/RingOfDefinition/Utils.lean
index 2f45d22..c66c986 100644
--- a/Pi1/RingTheory/RingOfDefinition/Utils.lean
+++ b/Pi1/RingTheory/RingOfDefinition/Utils.lean
@@ -31,7 +31,7 @@ theorem MvPolynomial.coefficients_finite (p : MvPolynomial ι R) :
   apply Set.Finite.image
   change Set.Finite (Finsupp.support p : Set (ι →₀ ℕ))
   rw [← Finsupp.fun_support_eq]
-  exact Finsupp.finite_support p
+  exact Finsupp.hasFiniteSupport p
 
 theorem MvPolynomial.Set.coefficients_finite_of_finite (S : Set (MvPolynomial ι R))
     (hf : Set.Finite S) : Set.Finite (MvPolynomial.Set.coefficients S) := by
diff --git a/Pi1/RingTheory/TotallySplit.lean b/Pi1/RingTheory/TotallySplit.lean
index ffe7470..c06c32e 100644
--- a/Pi1/RingTheory/TotallySplit.lean
+++ b/Pi1/RingTheory/TotallySplit.lean
@@ -167,7 +167,7 @@ lemma exists_isSplitOfRank_tensorProduct [Etale R S] [Module.Finite R S] {n : 
       let e := e₁.trans <| e₂.trans <| e₃.trans <| e₄.trans e₅
       refine ⟨V, inferInstance, inferInstance, ?_, ?_, ?_⟩
       · have : Module.FaithfullyFlat R S := by
-          apply Module.FaithfullyFlat.of_specComap_surjective
+          apply Module.FaithfullyFlat.of_comap_surjective
           rw [← Algebra.rankAtStalk_pos_iff_specComap_surjective]
           intro p
           simp [hn]
diff --git a/Pi1/RingTheory/Transcendence.lean b/Pi1/RingTheory/Transcendence.lean
index 2a36b33..2dd45e4 100644
--- a/Pi1/RingTheory/Transcendence.lean
+++ b/Pi1/RingTheory/Transcendence.lean
@@ -10,7 +10,7 @@ lemma Algebra.finite_of_intermediateFieldFG_of_isAlgebraic
   obtain ⟨s, hs⟩ := h
   have : Algebra.FiniteType k K := by
     use s
-    rw [← IntermediateField.adjoin_algebraic_toSubalgebra
+    rw [← IntermediateField.adjoin_toSubalgebra_of_isAlgebraic
       (fun x hx ↦ Algebra.IsAlgebraic.isAlgebraic x)]
     simpa [← IntermediateField.toSubalgebra_inj] using hs
   exact Algebra.IsIntegral.finite