[Merged by Bors] - chore: cleanups following #8609 and #8714

Mathlib/Data/Polynomial/Splits.lean

@@ -30,7 +30,7 @@ open BigOperators Polynomial
 
 universe u v w
 
-variable {F : Type u} {K : Type v} {L : Type w}
+variable {R : Type*} {F : Type u} {K : Type v} {L : Type w}
 
 namespace Polynomial
 
@@ -224,7 +224,7 @@ theorem degree_eq_card_roots' {p : K[X]} {i : K →+* L} (p_ne_zero : p.map i 
 
 end CommRing
 
-variable [Field K] [Field L] [Field F]
+variable [CommRing R] [Field K] [Field L] [Field F]
 
 variable (i : K →+* L)
 
@@ -329,17 +329,17 @@ theorem roots_map {f : K[X]} (hf : f.Splits <| RingHom.id K) : (f.map i).roots =
       rw [map_id]).symm
 #align polynomial.roots_map Polynomial.roots_map
 
-theorem image_rootSet [Algebra F K] [Algebra F L] {p : F[X]} (h : p.Splits (algebraMap F K))
-    (f : K →ₐ[F] L) : f '' p.rootSet K = p.rootSet L := by
+theorem image_rootSet [Algebra R K] [Algebra R L] {p : R[X]} (h : p.Splits (algebraMap R K))
+    (f : K →ₐ[R] L) : f '' p.rootSet K = p.rootSet L := by
   classical
     rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← f.coe_toRingHom,
-      ← roots_map _ ((splits_id_iff_splits (algebraMap F K)).mpr h), map_map, f.comp_algebraMap,
+      ← roots_map _ ((splits_id_iff_splits (algebraMap R K)).mpr h), map_map, f.comp_algebraMap,
       ← rootSet]
 #align polynomial.image_root_set Polynomial.image_rootSet
 
-theorem adjoin_rootSet_eq_range [Algebra F K] [Algebra F L] {p : F[X]}
-    (h : p.Splits (algebraMap F K)) (f : K →ₐ[F] L) :
-    Algebra.adjoin F (p.rootSet L) = f.range ↔ Algebra.adjoin F (p.rootSet K) = ⊤ := by
+theorem adjoin_rootSet_eq_range [Algebra R K] [Algebra R L] {p : R[X]}
+    (h : p.Splits (algebraMap R K)) (f : K →ₐ[R] L) :
+    Algebra.adjoin R (p.rootSet L) = f.range ↔ Algebra.adjoin R (p.rootSet K) = ⊤ := by
   rw [← image_rootSet h f, Algebra.adjoin_image, ← Algebra.map_top]
   exact (Subalgebra.map_injective f.toRingHom.injective).eq_iff
 #align polynomial.adjoin_root_set_eq_range Polynomial.adjoin_rootSet_eq_range
@@ -370,7 +370,8 @@ theorem eq_X_sub_C_of_splits_of_single_root {x : K} {h : K[X]} (h_splits : Split
 set_option linter.uppercaseLean3 false in
 #align polynomial.eq_X_sub_C_of_splits_of_single_root Polynomial.eq_X_sub_C_of_splits_of_single_root
 
-theorem mem_lift_of_splits_of_roots_mem_range (R : Type*) [CommRing R] [Algebra R K] {f : K[X]}
+variable (R) in
+theorem mem_lift_of_splits_of_roots_mem_range [Algebra R K] {f : K[X]}
     (hs : f.Splits (RingHom.id K)) (hm : f.Monic) (hr : ∀ a ∈ f.roots, a ∈ (algebraMap R K).range) :
     f ∈ Polynomial.lifts (algebraMap R K) := by
   rw [eq_prod_roots_of_monic_of_splits_id hm hs, lifts_iff_liftsRing]
@@ -438,27 +439,22 @@ theorem splits_id_of_splits {f : K[X]} (h : Splits i f)
     (roots_mem_range : ∀ a ∈ (f.map i).roots, a ∈ i.range) : Splits (RingHom.id K) f :=
   splits_of_comp (RingHom.id K) i h roots_mem_range
 
-theorem splits_of_algHom {R L' : Type*} [CommRing R] [Field L'] [Algebra R L] [Algebra R L']
-    {f : R[X]} (h : Polynomial.Splits (algebraMap R L) f) (e : L →ₐ[R] L') :
-    Polynomial.Splits (algebraMap R L') f := by
-  rw [← splits_id_iff_splits, ← AlgHom.comp_algebraMap_of_tower R e, ← map_map,
-    splits_id_iff_splits]
-  exact splits_of_splits_id e.toRingHom <| (splits_id_iff_splits _).mpr h
-
-theorem splits_of_isScalarTower {R : Type*} (L' : Type*) [CommRing R] [Field L'] [Algebra R L]
-    [Algebra R L'] [Algebra L L'] [IsScalarTower R L L'] {f : R[X]}
-    (h : Polynomial.Splits (algebraMap R L) f) :
-    Polynomial.Splits (algebraMap R L') f :=
-  splits_of_algHom h (IsScalarTower.toAlgHom R L L')
-
-theorem splits_comp_of_splits (j : L →+* F) {f : K[X]} (h : Splits i f) : Splits (j.comp i) f := by
-  -- Porting note: was
-  -- change i with (RingHom.id _).comp i at h
-  rw [← splits_map_iff]
-  rw [← RingHom.id_comp i, ← splits_map_iff i] at h
-  exact splits_of_splits_id _ h
+theorem splits_comp_of_splits (i : R →+* K) (j : K →+* L) {f : R[X]} (h : Splits i f) :
+    Splits (j.comp i) f :=
+  (splits_map_iff i j).mp (splits_of_splits_id _ <| (splits_map_iff i <| .id K).mpr h)
 #align polynomial.splits_comp_of_splits Polynomial.splits_comp_of_splits
 
+variable [Algebra R K] [Algebra R L]
+
+theorem splits_of_algHom {f : R[X]} (h : Splits (algebraMap R K) f) (e : K →ₐ[R] L) :
+    Splits (algebraMap R L) f := by
+  rw [← e.comp_algebraMap_of_tower R]; exact splits_comp_of_splits _ _ h
+
+variable (L) in
+theorem splits_of_isScalarTower {f : R[X]} [Algebra K L] [IsScalarTower R K L]
+    (h : Splits (algebraMap R K) f) : Splits (algebraMap R L) f :=
+  splits_of_algHom h (IsScalarTower.toAlgHom R K L)
+
 /-- A polynomial splits if and only if it has as many roots as its degree. -/
 theorem splits_iff_card_roots {p : K[X]} :
     Splits (RingHom.id K) p ↔ Multiset.card p.roots = p.natDegree := by

Mathlib/FieldTheory/Adjoin.lean

@@ -848,14 +848,20 @@ theorem finrank_eq_one_iff : finrank F K = 1 ↔ K = ⊥ := by
     bot_toSubalgebra]
 #align intermediate_field.finrank_eq_one_iff IntermediateField.finrank_eq_one_iff
 
-@[simp]
+@[simp] protected
 theorem rank_bot : Module.rank F (⊥ : IntermediateField F E) = 1 := by rw [rank_eq_one_iff]
 #align intermediate_field.rank_bot IntermediateField.rank_bot
 
-@[simp]
+@[simp] protected
 theorem finrank_bot : finrank F (⊥ : IntermediateField F E) = 1 := by rw [finrank_eq_one_iff]
 #align intermediate_field.finrank_bot IntermediateField.finrank_bot
 
+@[simp] protected theorem rank_top : Module.rank (⊤ : IntermediateField F E) E = 1 :=
+  Subalgebra.bot_eq_top_iff_rank_eq_one.mp <| top_le_iff.mp fun x _ ↦ ⟨⟨x, trivial⟩, rfl⟩
+
+@[simp] protected theorem finrank_top : finrank (⊤ : IntermediateField F E) E = 1 :=
+  rank_eq_one_iff_finrank_eq_one.mp IntermediateField.rank_top
+
 theorem rank_adjoin_eq_one_iff : Module.rank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : IntermediateField F E) :=
   Iff.trans rank_eq_one_iff adjoin_eq_bot_iff
 #align intermediate_field.rank_adjoin_eq_one_iff IntermediateField.rank_adjoin_eq_one_iff

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -398,55 +398,47 @@ end IsAlgClosure
 
 section Algebra.IsAlgebraic
 
-variable {F K : Type*} (A : Type*) [Field F] [Field K] [Field A] [IsAlgClosed A] [Algebra F K]
-  (hK : Algebra.IsAlgebraic F K) [Algebra F A]
+variable {F K : Type*} (A : Type*) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A]
+  (hK : Algebra.IsAlgebraic F K)
 
 /-- Let `A` be an algebraically closed field and let `x ∈ K`, with `K/F` an algebraic extension
   of fields. Then the images of `x` by the `F`-algebra morphisms from `K` to `A` are exactly
   the roots in `A` of the minimal polynomial of `x` over `F`. -/
-theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly (x : K) :
+theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly [IsAlgClosed A] (x : K) :
     (Set.range fun ψ : K →ₐ[F] A ↦ ψ x) = (minpoly F x).rootSet A :=
   range_eval_eq_rootSet_minpoly_of_splits A (fun _ ↦ IsAlgClosed.splits_codomain _) hK x
 #align algebra.is_algebraic.range_eval_eq_root_set_minpoly Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly
 
-/-- All `F`-`AlgHom`s from `K` to an algebraic closed field `A` factor through any subextension of
-`A/F` in which the minimal polynomial of elements of `K` splits. -/
+/-- All `F`-embeddings of a field `K` into another field `A` factor through any intermediate
+field of `A/F` in which the minimal polynomial of elements of `K` splits. -/
 @[simps]
-def IntermediateField.algHomEquivAlgHomOfIsAlgClosed (L : IntermediateField F A)
+def IntermediateField.algHomEquivAlgHomOfSplits (L : IntermediateField F A)
     (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) :
     (K →ₐ[F] L) ≃ (K →ₐ[F] A) where
   toFun := L.val.comp
-  invFun := by
-    refine fun f => f.codRestrict _ (fun x => ?_)
-    suffices f x ∈ L.val '' rootSet (minpoly F x) L by
-      obtain ⟨z, -, hz⟩ := this
-      rw [← hz]
-      exact SetLike.coe_mem z
-    rw [image_rootSet (hL x), ← Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly _ hK]
-    exact Set.mem_range_self f
+  invFun f := f.codRestrict _ fun x ↦
+    ((hK x).isIntegral.map f).mem_intermediateField_of_minpoly_splits <| by
+      rw [minpoly.algHom_eq f f.injective]; exact hL x
   left_inv _ := rfl
   right_inv _ := by rfl
 
-theorem IntermediateField.algHomEquivAlgHomOfIsAlgClosed_apply_apply (L : IntermediateField F A)
+theorem IntermediateField.algHomEquivAlgHomOfSplits_apply_apply (L : IntermediateField F A)
     (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (f : K →ₐ[F] L) (x : K) :
-    algHomEquivAlgHomOfIsAlgClosed A hK L hL f x = algebraMap L A (f x) := rfl
+    algHomEquivAlgHomOfSplits A hK L hL f x = algebraMap L A (f x) := rfl
 
-/-- All `F`-`AlgHom`s from `K` to an algebraic closed field `A` factor through any subfield of `A`
-in which the minimal polynomial of elements of `K` splits. -/
-noncomputable def Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed (L : Type*) [Field L]
+/-- All `F`-embeddings of a field `K` into another field `A` factor through any subextension
+of `A/F` in which the minimal polynomial of elements of `K` splits. -/
+noncomputable def Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits (L : Type*) [Field L]
     [Algebra F L] [Algebra L A] [IsScalarTower F L A]
     (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) :
-    (K →ₐ[F] L) ≃ (K →ₐ[F] A) := by
-  refine (AlgEquiv.refl.arrowCongr
-    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L A))).trans ?_
-  refine IntermediateField.algHomEquivAlgHomOfIsAlgClosed
-    A hK (IsScalarTower.toAlgHom F L A).fieldRange ?_
-  exact fun x => splits_of_algHom (hL x) (AlgHom.rangeRestrict _)
-
-theorem Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed_apply_apply (L : Type*) [Field L]
+    (K →ₐ[F] L) ≃ (K →ₐ[F] A) :=
+  (AlgEquiv.refl.arrowCongr (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L A))).trans <|
+    IntermediateField.algHomEquivAlgHomOfSplits A hK (IsScalarTower.toAlgHom F L A).fieldRange
+    fun x ↦ splits_of_algHom (hL x) (AlgHom.rangeRestrict _)
+
+theorem Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits_apply_apply (L : Type*) [Field L]
     [Algebra F L] [Algebra L A] [IsScalarTower F L A]
     (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (f : K →ₐ[F] L) (x : K) :
-    Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed A hK L hL f x =
-    algebraMap L A (f x) := rfl
+    Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits A hK L hL f x = algebraMap L A (f x) := rfl
 
 end Algebra.IsAlgebraic

Mathlib/FieldTheory/PrimitiveElement.lean

@@ -360,7 +360,7 @@ theorem AlgHom.card (K : Type*) [Field K] [IsAlgClosed K] [Algebra F K] :
 theorem AlgHom.card_of_splits (L : Type*) [Field L] [Algebra F L]
     (hL : ∀ x : E, (minpoly F x).Splits (algebraMap F L)) :
     Fintype.card (E →ₐ[F] L) = finrank F E := by
-  rw [← Fintype.ofEquiv_card <| Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed
+  rw [← Fintype.ofEquiv_card <| Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits
     (AlgebraicClosure L) (Algebra.IsAlgebraic.of_finite F E) _ hL]
   convert AlgHom.card F E (AlgebraicClosure L)
 
@@ -397,34 +397,14 @@ theorem primitive_element_iff_algHom_eq_of_eval' (α : E) :
 
 theorem primitive_element_iff_algHom_eq_of_eval (α : E)
     (φ : E →ₐ[F] A) : F⟮α⟯ = ⊤ ↔ ∀ ψ : E →ₐ[F] A, φ α = ψ α → φ = ψ := by
-  rw [Field.primitive_element_iff_algHom_eq_of_eval' F A hA]
-  refine ⟨fun h _ eq => h eq, fun h φ₀ ψ₀ h' => ?_⟩
-  let K := normalClosure F E A
-  have : IsNormalClosure F E K := by
-    refine Algebra.IsAlgebraic.isNormalClosure_normalClosure ?_ hA
-    exact Algebra.IsAlgebraic.of_finite F E
-  have hK_mem : ∀ (ψ : E →ₐ[F] A) (x : E), ψ x ∈ K :=
-    fun ψ x => AlgHom.fieldRange_le_normalClosure ψ ⟨x, rfl⟩
-  let res : (E →ₐ[F] A) → (E →ₐ[F] K) := fun ψ => AlgHom.codRestrict ψ K.toSubalgebra (hK_mem ψ)
-  rsuffices ⟨σ, hσ⟩ : ∃ σ : K →ₐ[F] A, σ (⟨φ₀ α, hK_mem _ _⟩) = φ α
-  · suffices res φ₀ = res ψ₀ by
-      ext x
-      exact Subtype.mk_eq_mk.mp (AlgHom.congr_fun this x)
-    have eq₁ : φ = AlgHom.comp σ (res φ₀) := h (AlgHom.comp σ (res φ₀)) hσ.symm
-    have eq₂ : φ = AlgHom.comp σ (res ψ₀) := by
-      refine h (AlgHom.comp σ (res ψ₀)) ?_
-      simp_rw [← hσ, h']
-      rfl
-    ext1 x
-    exact (RingHom.injective σ.toRingHom) <| AlgHom.congr_fun (eq₁.symm.trans eq₂) x
-  refine IntermediateField.exists_algHom_of_splits_of_aeval ?_ ?_
-  · refine fun x => ⟨IsAlgebraic.isIntegral (IsAlgebraic.of_finite F x), ?_⟩
-    refine Polynomial.splits_of_algHom ?_ K.toSubalgebra.val
-    exact Normal.splits (IsNormalClosure.normal (K := E)) x
-  · rw [aeval_algHom_apply, _root_.map_eq_zero]
-    convert minpoly.aeval F α
-    letI : Algebra E K := (res φ₀).toAlgebra
-    exact minpoly.algebraMap_eq (algebraMap E K).injective α
+  refine ⟨fun h ψ hψ ↦ (Field.primitive_element_iff_algHom_eq_of_eval' F A hA α).mp h hψ,
+    fun h ↦ eq_of_le_of_finrank_eq' le_top ?_⟩
+  letI : Algebra F⟮α⟯ A := (φ.comp F⟮α⟯.val).toAlgebra
+  haveI := isSeparable_tower_top_of_isSeparable F F⟮α⟯ E
+  rw [IntermediateField.finrank_top, ← AlgHom.card_of_splits _ _ A, Fintype.card_eq_one_iff]
+  · exact ⟨{ __ := φ, commutes' := fun _ ↦ rfl }, fun ψ ↦ AlgHom.restrictScalars_injective F <|
+      Eq.symm <| h _ (ψ.commutes <| AdjoinSimple.gen F α).symm⟩
+  · exact fun x ↦ (IsIntegral.of_finite F x).minpoly_splits_tower_top (hA x)
 
 end Field
 

Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

@@ -151,16 +151,16 @@ end IsSplittingField
 
 end Polynomial
 
-namespace IntermediateField
-
 open Polynomial
 
-variable {K L} [Field K] [Field L] [Algebra K L] {p : K[X]}
+variable {K L} [Field K] [Field L] [Algebra K L] {p : K[X]} {F : IntermediateField K L}
 
-theorem splits_of_splits {F : IntermediateField K L} (h : p.Splits (algebraMap K L))
+theorem IntermediateField.splits_of_splits (h : p.Splits (algebraMap K L))
     (hF : ∀ x ∈ p.rootSet L, x ∈ F) : p.Splits (algebraMap K F) := by
   simp_rw [← F.fieldRange_val, rootSet_def, Finset.mem_coe, Multiset.mem_toFinset] at hF
   exact splits_of_comp _ F.val.toRingHom h hF
 #align intermediate_field.splits_of_splits IntermediateField.splits_of_splits
 
-end IntermediateField
+theorem IsIntegral.mem_intermediateField_of_minpoly_splits {x : L} (int : IsIntegral K x)
+    {F : IntermediateField K L} (h : Splits (algebraMap K F) (minpoly K x)) : x ∈ F := by
+  rw [← F.fieldRange_val]; exact int.mem_range_algebraMap_of_minpoly_splits h

Mathlib/NumberTheory/NumberField/Discriminant.lean

@@ -43,7 +43,7 @@ theorem discr_eq_discr {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι
 
 theorem discr_eq_discr_of_algEquiv {L : Type*} [Field L] [NumberField L] (f : K ≃ₐ[ℚ] L) :
     discr K = discr L := by
-  let f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (integralClosure_algEquiv_restrict (f.restrictScalars ℤ)).toLinearEquiv
+  let f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (f.restrictScalars ℤ).mapIntegralClosure.toLinearEquiv
   let e : Module.Free.ChooseBasisIndex ℤ (𝓞 K) ≃ (K →ₐ[ℚ] ℂ) := by
     refine Fintype.equivOfCardEq ?_
     rw [← FiniteDimensional.finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, AlgHom.card]

Mathlib/RingTheory/Adjoin/Field.lean

@@ -82,3 +82,23 @@ theorem Polynomial.lift_of_splits {F K L : Type*} [Field F] [Field K] [Field L]
 #align lift_of_splits Polynomial.lift_of_splits
 
 end Embeddings
+
+variable {R K L M : Type*} [CommRing R] [Field K] [Field L] [CommRing M] [Algebra R K] [Algebra R L]
+  [Algebra R M] {x : L} (int : IsIntegral R x) (h : Splits (algebraMap R K) (minpoly R x))
+
+theorem IsIntegral.mem_range_algHom_of_minpoly_splits (f : K →ₐ[R] L) : x ∈ f.range :=
+  show x ∈ Set.range f from Set.image_subset_range _ _ <| by
+    rw [image_rootSet h f, mem_rootSet']
+    exact ⟨((minpoly.monic int).map _).ne_zero, minpoly.aeval R x⟩
+
+theorem IsIntegral.mem_range_algebraMap_of_minpoly_splits [Algebra K L] [IsScalarTower R K L] :
+    x ∈ (algebraMap K L).range :=
+  int.mem_range_algHom_of_minpoly_splits h (IsScalarTower.toAlgHom R K L)
+
+theorem IsIntegral.minpoly_splits_tower_top
+    [Algebra K L] [IsScalarTower R K L] [Algebra K M] [IsScalarTower R K M]
+    {x : M} (int : IsIntegral R x) (h : Splits (algebraMap R L) (minpoly R x)) :
+    Splits (algebraMap K L) (minpoly K x) := by
+  rw [IsScalarTower.algebraMap_eq R K L] at h
+  exact splits_of_splits_of_dvd _ ((minpoly.monic int).map _).ne_zero
+    ((splits_map_iff _ _).mpr h) (minpoly.dvd_map_of_isScalarTower R _ x)

Mathlib/RingTheory/IntegralClosure.lean

@@ -469,27 +469,25 @@ theorem integralClosure_map_algEquiv [Algebra R S] (f : A ≃ₐ[R] S) :
 
 /-- An `AlgHom` between two rings restrict to an `AlgHom` between the integral closures inside
 them. -/
-def integralClosure_algHom_restrict [Algebra R S] (f : A →ₐ[R] S) :
+def AlgHom.mapIntegralClosure [Algebra R S] (f : A →ₐ[R] S) :
     integralClosure R A →ₐ[R] integralClosure R S :=
   (f.restrictDomain (integralClosure R A)).codRestrict (integralClosure R S) (fun ⟨_, h⟩ => h.map f)
 
 @[simp]
-theorem integralClosure_coe_algHom_restrict [Algebra R S] (f : A →ₐ[R] S)
-    (x : integralClosure R A) : (integralClosure_algHom_restrict f x : S) = f (x : A) := rfl
+theorem AlgHom.coe_mapIntegralClosure [Algebra R S] (f : A →ₐ[R] S)
+    (x : integralClosure R A) : (f.mapIntegralClosure x : S) = f (x : A) := rfl
 
 /-- An `AlgEquiv` between two rings restrict to an `AlgEquiv` between the integral closures inside
 them. -/
-noncomputable def integralClosure_algEquiv_restrict [Algebra R S] (f : A ≃ₐ[R] S) :
-    integralClosure R A ≃ₐ[R] integralClosure R S := by
-  refine AlgEquiv.ofBijective (integralClosure_algHom_restrict f) ⟨?_, ?_⟩
-  · erw [AlgHom.injective_codRestrict]
-    exact (EquivLike.injective f).comp Subtype.val_injective
-  · rintro ⟨y, hy⟩
-    exact ⟨⟨f.symm y, hy.map f.symm⟩, by rw [Subtype.mk_eq_mk]; simp⟩
+def AlgEquiv.mapIntegralClosure [Algebra R S] (f : A ≃ₐ[R] S) :
+    integralClosure R A ≃ₐ[R] integralClosure R S :=
+  AlgEquiv.ofAlgHom (f : A →ₐ[R] S).mapIntegralClosure (f.symm : S →ₐ[R] A).mapIntegralClosure
+    (AlgHom.ext fun _ ↦ Subtype.ext (f.right_inv _))
+    (AlgHom.ext fun _ ↦ Subtype.ext (f.left_inv _))
 
 @[simp]
-theorem integralClosure_coe_algEquiv_restrict [Algebra R S] (f : A ≃ₐ[R] S)
-    (x : integralClosure R A) : (integralClosure_algEquiv_restrict f x : S) = f (x : A) := rfl
+theorem AlgEquiv.coe_mapIntegralClosure [Algebra R S] (f : A ≃ₐ[R] S)
+    (x : integralClosure R A) : (f.mapIntegralClosure x : S) = f (x : A) := rfl
 
 theorem integralClosure.isIntegral (x : integralClosure R A) : IsIntegral R x :=
   let ⟨p, hpm, hpx⟩ := x.2