From 7b96a0461a39ec8ba0a699aa0921587c8950b3bf Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Fri, 17 Nov 2023 18:13:14 +0100
Subject: [PATCH] bump

---
 FltRegular/FltThree/Edwards.lean              |  4 +--
 FltRegular/NumberTheory/AuxLemmas.lean        | 28 ++++-------------
 .../NumberTheory/Cyclotomic/UnitLemmas.lean   |  6 ++--
 FltRegular/NumberTheory/Different.lean        | 10 +++----
 FltRegular/NumberTheory/Hilbert90.lean        |  2 +-
 FltRegular/NumberTheory/IdealNorm.lean        | 30 +++++++++----------
 .../NumberTheory/KummersLemma/Field.lean      | 10 +++----
 FltRegular/NumberTheory/MinpolyDiv.lean       |  2 +-
 FltRegular/NumberTheory/QuotientTrace.lean    | 22 +++++++-------
 lake-manifest.json                            |  4 +--
 10 files changed, 51 insertions(+), 67 deletions(-)

diff --git a/FltRegular/FltThree/Edwards.lean b/FltRegular/FltThree/Edwards.lean
index 64d068b7..afb4bdaf 100644
--- a/FltRegular/FltThree/Edwards.lean
+++ b/FltRegular/FltThree/Edwards.lean
@@ -24,7 +24,7 @@ theorem OddPrimeOrFour.im_ne_zero {p : ℤ√(-3)} (h : OddPrimeOrFour p.norm)
   · rw [H, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
     rw [← sq_abs, hcoprime] at h
     norm_num at h
-  · exact pow_not_prime one_lt_two.ne' hp
+  · exact not_prime_pow one_lt_two.ne' hp
 #align odd_prime_or_four.im_ne_zero OddPrimeOrFour.im_ne_zero
 
 theorem Zsqrt3.isUnit_iff {z : ℤ√(-3)} : IsUnit z ↔ abs z.re = 1 ∧ z.im = 0 :=
@@ -67,7 +67,7 @@ theorem OddPrimeOrFour.factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime
     rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two, eq_comm] at hc
     have := hprime.abs
     rw [←hc] at this
-    exact pow_not_prime one_lt_two.ne' this
+    exact not_prime_pow one_lt_two.ne' this
 #align odd_prime_or_four.factors OddPrimeOrFour.factors
 
 theorem step1a {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even a.norm) :
diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean
index 05b6be3b..d1a863ae 100644
--- a/FltRegular/NumberTheory/AuxLemmas.lean
+++ b/FltRegular/NumberTheory/AuxLemmas.lean
@@ -290,17 +290,6 @@ lemma rootsOfUnity_equiv_of_primitiveRoots_symm_apply {K L} [Field K] [Field L]
   obtain ⟨ε, rfl⟩ := (rootsOfUnity_equiv_of_primitiveRoots f n hζ).surjective η
   rw [MulEquiv.symm_apply_apply, rootsOfUnity_equiv_of_primitiveRoots_apply]
 
--- Mathlib/Algebra/Associated.lean
-lemma not_irreducible_pow {M} [Monoid M] {x : M} {n} (hn : n ≠ 1) : ¬ Irreducible (x ^ n) := by
-  cases n with
-  | zero => simp
-  | succ n =>
-    intro ⟨h₁, h₂⟩
-    have := h₂ _ _ (pow_succ _ _)
-    rw [isUnit_pow_iff, or_self] at this
-    exact h₁ (this.pow _)
-    exact Nat.succ_ne_succ.mp hn
-
 -- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
 section Cyclic
 
@@ -568,11 +557,6 @@ theorem IsIntegralClosure.isLocalization' (ha : Algebra.IsAlgebraic K L) [NoZero
   · simp only [IsIntegralClosure.algebraMap_injective C A L h]
 end
 
--- Mathlib/RingTheory/Algebraic.lean
-lemma Algebra.IsIntegral.isAlgebraic {R S} [CommRing R] [CommRing S] [Algebra R S] [Nontrivial R]
-    (h : Algebra.IsIntegral R S) : Algebra.IsAlgebraic R S :=
-  fun x ↦ _root_.IsIntegral.isAlgebraic _ (h x)
-
 -- Mathlib/RingTheory/Algebraic.lean
 -- or Mathlib/RingTheory/LocalProperties.lean
 open Polynomial in
@@ -640,13 +624,13 @@ lemma isAlgebraic_of_isFractionRing {R S} (K L) [CommRing R] [CommRing S] [Field
   intro x
   obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective S⁰ x
   rw [isAlgebraic_iff_isIntegral, IsLocalization.mk'_eq_mul_mk'_one]
-  apply RingHom.is_integral_mul
-  · apply isIntegral_of_isScalarTower (R := R)
+  apply RingHom.IsIntegralElem.mul
+  · apply IsIntegral.tower_top (R := R)
     apply IsIntegral.map (IsScalarTower.toAlgHom R S L)
     exact h x
   · show IsIntegral _ _
     rw [← isAlgebraic_iff_isIntegral, ← IsAlgebraic.invOf_iff, isAlgebraic_iff_isIntegral]
-    apply isIntegral_of_isScalarTower (R := R)
+    apply IsIntegral.tower_top (R := R)
     apply IsIntegral.map (IsScalarTower.toAlgHom R S L)
     exact h s
 
@@ -656,7 +640,7 @@ lemma isIntegralClosure_of_isIntegrallyClosed (R S K) [CommRing R] [CommRing S]
     [Nontrivial K] [IsIntegrallyClosed S] (hRS : Algebra.IsIntegral R S) :
     IsIntegralClosure S R K := by
   refine ⟨IsLocalization.injective _ le_rfl, fun {x} ↦
-    ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (isIntegral_of_isScalarTower (A := S) hx), ?_⟩⟩
+    ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := S) hx), ?_⟩⟩
   rintro ⟨y, rfl⟩
   exact IsIntegral.map (IsScalarTower.toAlgHom R S K) (hRS y)
 
@@ -696,8 +680,8 @@ lemma IsIntegral_of_isLocalization (R S Rₚ Sₚ) [CommRing R] [CommRing S] [Co
   obtain ⟨x, ⟨_, t, ht, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective
     (Algebra.algebraMapSubmonoid S M) x
   rw [IsLocalization.mk'_eq_mul_mk'_one]
-  apply RingHom.is_integral_mul
-  · exact isIntegral_of_isScalarTower (IsIntegral.map (IsScalarTower.toAlgHom R S Sₚ) (hRS x))
+  apply RingHom.IsIntegralElem.mul
+  · exact IsIntegral.tower_top (IsIntegral.map (IsScalarTower.toAlgHom R S Sₚ) (hRS x))
   · show IsIntegral _ _
     convert isIntegral_algebraMap (x := IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
     rw [this, IsLocalization.map_mk', _root_.map_one]
diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
index 85c16fa4..3ab5df4c 100644
--- a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
@@ -414,9 +414,9 @@ theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u :
       Units.val_pow_eq_pow_val] at hz
     norm_cast at hz
     simpa [hz] using unit_inv_conj_not_neg_zeta_runity hζ h u n hp
-  · apply RingHom.is_integral_mul
-    exact NumberField.RingOfIntegers.isIntegral_coe _
-    exact NumberField.RingOfIntegers.isIntegral_coe _
+  · apply RingHom.IsIntegralElem.mul
+    · exact NumberField.RingOfIntegers.isIntegral_coe _
+    · exact NumberField.RingOfIntegers.isIntegral_coe _
   · exact unit_lemma_val_one p u
 
 lemma inv_coe_coe {K A : Type*} [Field K] [SetLike A K] [SubsemiringClass A K] {S : A} (s : Sˣ) :
diff --git a/FltRegular/NumberTheory/Different.lean b/FltRegular/NumberTheory/Different.lean
index fb915e48..988ae9d9 100644
--- a/FltRegular/NumberTheory/Different.lean
+++ b/FltRegular/NumberTheory/Different.lean
@@ -115,7 +115,7 @@ lemma isIntegral_discr_mul_of_mem_traceFormDualSubmodule
   apply IsIntegral.sum
   intro i _
   rw [smul_mul_assoc, b.equivFun.map_smul, discr_def, mul_comm, ← H, Algebra.smul_def]
-  refine RingHom.is_integral_mul _ ?_ (hb _)
+  refine RingHom.IsIntegralElem.mul _ ?_ (hb _)
   apply IsIntegral.algebraMap
   rw [cramer_apply]
   apply IsIntegral.det
@@ -128,7 +128,7 @@ lemma isIntegral_discr_mul_of_mem_traceFormDualSubmodule
     have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp (hb j)
     rw [mul_comm, ← hy, ← Algebra.smul_def]
     exact I.smul_mem _ (ha)
-  · exact isIntegral_trace (RingHom.is_integral_mul _ (hb j) (hb k))
+  · exact isIntegral_trace (RingHom.IsIntegralElem.mul _ (hb j) (hb k))
 
 variable (A K)
 
@@ -327,10 +327,10 @@ lemma pow_sub_one_dvd_differentIdeal
     {p : Ideal A} [p.IsMaximal] (P : Ideal B) (e : ℕ) (hp : p ≠ ⊥)
     (hP : P ^ e ∣ p.map (algebraMap A B)) : P ^ (e - 1) ∣ differentIdeal A B := by
   have : IsIntegralClosure B A (FractionRing B) :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := A) (A := B))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := A) (B := B))
   have : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
     IsIntegralClosure.isLocalization' _ (FractionRing A) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := A) (A := B)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := A) (B := B)))
   have : FiniteDimensional (FractionRing A) (FractionRing B) :=
     Module.Finite_of_isLocalization A B _ _ A⁰
   by_cases he : e = 0
@@ -371,7 +371,7 @@ lemma traceFormDualSubmodule_span_adjoin
       (aeval x (derivative <| minpoly K x) : L)⁻¹ •
         (Subalgebra.toSubmodule (Algebra.adjoin A {x})) := by
   classical
-  have hKx : IsIntegral K x := Algebra.IsIntegral.of_finite (R := K) (A := L) x
+  have hKx : IsIntegral K x := Algebra.IsIntegral.of_finite (R := K) (B := L) x
   let pb := (Algebra.adjoin.powerBasis' hKx).map
     ((Subalgebra.equivOfEq _ _ hx).trans (Subalgebra.topEquiv))
   have pbgen : pb.gen = x := by simp
diff --git a/FltRegular/NumberTheory/Hilbert90.lean b/FltRegular/NumberTheory/Hilbert90.lean
index b3820b32..37024dd8 100644
--- a/FltRegular/NumberTheory/Hilbert90.lean
+++ b/FltRegular/NumberTheory/Hilbert90.lean
@@ -25,7 +25,7 @@ lemma Hilbert90_integral (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowe
   haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
   have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
     IsIntegralClosure.isLocalization' A K L B
-      (Algebra.isAlgebraic_iff_isIntegral.mpr <| Algebra.IsIntegral.of_finite (R := K) (A := L))
+      (Algebra.isAlgebraic_iff_isIntegral.mpr <| Algebra.IsIntegral.of_finite (R := K) (B := L))
   obtain ⟨ε, hε⟩ := Hilbert90 σ hσ _ hη
   obtain ⟨x, y, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid B A⁰) ε
   obtain ⟨t, ht, ht'⟩ := y.prop
diff --git a/FltRegular/NumberTheory/IdealNorm.lean b/FltRegular/NumberTheory/IdealNorm.lean
index d38ec9bb..ed233d6e 100644
--- a/FltRegular/NumberTheory/IdealNorm.lean
+++ b/FltRegular/NumberTheory/IdealNorm.lean
@@ -26,10 +26,10 @@ variable (R S K L) [CommRing R] [CommRing S] [Field K] [Field L]
     [IsIntegrallyClosed S] [IsSeparable (FractionRing R) (FractionRing S)]
 
 instance : IsIntegralClosure S R (FractionRing S) :=
-  isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S))
+  isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S))
 instance : IsLocalization (Algebra.algebraMapSubmonoid S R⁰) (FractionRing S) :=
     IsIntegralClosure.isLocalization' _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
 instance : FiniteDimensional (FractionRing R) (FractionRing S) :=
     Module.Finite_of_isLocalization R S _ _ R⁰
 
@@ -65,10 +65,10 @@ def Algebra.intNorm (R S) [CommRing R] [CommRing S] [IsIntegrallyClosed R]
     [Algebra R S] [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [hRS : Module.Finite R S]
     [IsIntegrallyClosed S] [IsSeparable (FractionRing R) (FractionRing S)] : S →* R := by
   haveI : IsIntegralClosure S R (FractionRing S) :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S))
   haveI : IsLocalization (algebraMapSubmonoid S R⁰) (FractionRing S) :=
     IsIntegralClosure.isLocalization' _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
   haveI : FiniteDimensional (FractionRing R) (FractionRing S) :=
     Module.Finite_of_isLocalization R S _ _ R⁰
   exact Algebra.intNormAux R S (FractionRing R) (FractionRing S)
@@ -81,10 +81,10 @@ lemma Algebra.algebraMap_intNorm {R S K L} [CommRing R] [CommRing S] [Field K] [
     [IsSeparable (FractionRing R) (FractionRing S)] (x : S) :
     algebraMap R K (Algebra.intNorm R S x) = Algebra.norm K (algebraMap S L x) := by
   haveI : IsIntegralClosure S R (FractionRing S) :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S))
   haveI : IsLocalization (algebraMapSubmonoid S R⁰) (FractionRing S) :=
     IsIntegralClosure.isLocalization' _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
   haveI : FiniteDimensional (FractionRing R) (FractionRing S) :=
     Module.Finite_of_isLocalization R S _ _ R⁰
   haveI := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
@@ -105,10 +105,10 @@ lemma Algebra.algebraMap_intNorm_fractionRing {R S} [CommRing R] [CommRing S]
     algebraMap R (FractionRing R) (Algebra.intNorm R S x) =
       Algebra.norm (FractionRing R) (algebraMap S (FractionRing S)  x) := by
   haveI : IsIntegralClosure S R (FractionRing S) :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S))
   haveI : IsLocalization (algebraMapSubmonoid S R⁰) (FractionRing S) :=
     IsIntegralClosure.isLocalization' _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
   haveI : FiniteDimensional (FractionRing R) (FractionRing S) :=
     Module.Finite_of_isLocalization R S _ _ R⁰
   exact Algebra.map_intNormAux x
@@ -119,10 +119,10 @@ lemma Algebra.intNorm_eq_norm (R S) [CommRing R] [CommRing S] [IsIntegrallyClose
     [IsSeparable (FractionRing R) (FractionRing S)] : Algebra.intNorm R S = Algebra.norm R := by
   ext x
   haveI : IsIntegralClosure S R (FractionRing S) :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S))
   haveI : IsLocalization (algebraMapSubmonoid S R⁰) (FractionRing S) :=
     IsIntegralClosure.isLocalization' _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
   apply IsFractionRing.injective R (FractionRing R)
   rw [Algebra.algebraMap_intNorm_fractionRing, Algebra.norm_localization R R⁰]
 
@@ -176,13 +176,13 @@ lemma Algebra.intNorm_eq_of_isLocalization (M : Submonoid R) (hM : M ≤ R⁰)
   letI := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
     (algebraMapSubmonoid S M) Sₘ L
   haveI : IsIntegralClosure S R L :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S))
   haveI : IsLocalization (algebraMapSubmonoid S R⁰) L :=
     IsIntegralClosure.isLocalization' _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
   haveI : FiniteDimensional K L := Module.Finite_of_isLocalization R S _ _ R⁰
   haveI : IsIntegralClosure Sₘ Rₘ L :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₘ) (A := Sₘ))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₘ) (B := Sₘ))
   apply IsFractionRing.injective Rₘ K
   rw [← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intNorm_fractionRing,
     Algebra.algebraMap_intNorm (L := L), ← IsScalarTower.algebraMap_apply]
@@ -285,7 +285,7 @@ theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R
   letI := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
     (Algebra.algebraMapSubmonoid S M) Sₘ L
   haveI : IsIntegralClosure Sₘ Rₘ L :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₘ) (A := Sₘ))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₘ) (B := Sₘ))
   cases h : subsingleton_or_nontrivial R
   · haveI := IsLocalization.unique R Rₘ M
     simp only [eq_iff_true_of_subsingleton]
@@ -495,7 +495,7 @@ theorem spanIntNorm_map (I : Ideal R) :
       IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
       RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
   haveI : IsIntegralClosure Sₚ Rₚ L :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₚ) (A := Sₚ))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₚ) (B := Sₚ))
   haveI : IsSeparable (FractionRing Rₚ) (FractionRing Sₚ) := by
     apply IsSeparable_of_equiv_equiv (FractionRing.algEquiv Rₚ (FractionRing R)).symm.toRingEquiv
       (FractionRing.algEquiv Sₚ (FractionRing S)).symm.toRingEquiv
diff --git a/FltRegular/NumberTheory/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean
index 018cd9a2..dfe38ee2 100644
--- a/FltRegular/NumberTheory/KummersLemma/Field.lean
+++ b/FltRegular/NumberTheory/KummersLemma/Field.lean
@@ -195,7 +195,7 @@ lemma isIntegralClosure_of_isScalarTower (R A K L B) [CommRing R] [CommRing A] [
   isIntegral_iff := fun {x} ↦ by
     refine Iff.trans ?_ (IsIntegralClosure.isIntegral_iff (R := R) (A := B) (B := L))
     exact ⟨isIntegral_trans (IsIntegralClosure.isIntegral_algebra R (A := A) K) x,
-      isIntegral_of_isScalarTower⟩
+      IsIntegral.tower_top⟩
 
 instance {K L} [Field K] [Field L] [Algebra K L] :
     IsIntegralClosure (𝓞 L) (𝓞 K) L := isIntegralClosure_of_isScalarTower ℤ _ K _ _
@@ -212,7 +212,7 @@ lemma minpoly_polyRoot'' {L : Type*} [Field L] [Algebra K L] (α : L)
     minpoly K (polyRoot hp hζ u hcong α e i : L) =
       (poly hp hζ u hcong).map (algebraMap (𝓞 K) K) := by
   have : IsIntegral K (polyRoot hp hζ u hcong α e i : L) :=
-    isIntegral_of_isScalarTower (polyRoot hp hζ u hcong α e i).prop
+    IsIntegral.tower_top (polyRoot hp hζ u hcong α e i).prop
   apply eq_of_monic_of_associated (minpoly.monic this) ((monic_poly hp hζ u hcong).map _)
   refine Irreducible.associated_of_dvd (minpoly.irreducible this)
     (irreducible_map_poly hp hζ u hcong hu) (minpoly.dvd _ _ ?_)
@@ -225,7 +225,7 @@ lemma minpoly_polyRoot' {L : Type*} [Field L] [Algebra K L] (α : L)
   apply map_injective (algebraMap (𝓞 K) K) Subtype.coe_injective
   rw [← minpoly.isIntegrallyClosed_eq_field_fractions' K]
   exact minpoly_polyRoot'' hp hζ u hcong hu α e i
-  exact isIntegral_of_isScalarTower (polyRoot hp hζ u hcong α e i).prop
+  exact IsIntegral.tower_top (polyRoot hp hζ u hcong α e i).prop
 
 lemma minpoly_polyRoot {L : Type*} [Field L] [Algebra K L] (α : L)
     (e : α ^ (p : ℕ) = algebraMap K L u) (i) :
@@ -283,7 +283,7 @@ lemma separable_poly (I : Ideal (𝓞 K)) [I.IsMaximal] :
     apply Ideal.Quotient.nontrivial
     rw [ne_eq, Ideal.map_eq_top_iff]; exact Ideal.IsMaximal.ne_top ‹_›
     · intros x y e; ext; exact (algebraMap K L).injective (congr_arg Subtype.val e)
-    · intros x; exact isIntegral_of_isScalarTower (IsIntegralClosure.isIntegral ℤ L x)
+    · intros x; exact IsIntegral.tower_top (IsIntegralClosure.isIntegral ℤ L x)
   rw [← Polynomial.separable_map' i, map_map, Ideal.quotientMap_comp_mk, ← map_map]
   apply Separable.map
   apply separable_poly_aux hp hζ u hcong
@@ -318,7 +318,7 @@ lemma isUnramified (L) [Field L] [Algebra K L] [IsSplittingField K L (X ^ (p : 
   constructor
   intros I hI hIbot
   refine isUnramifiedAt_of_Separable_minpoly (R := 𝓞 K) K (S := 𝓞 L) L I hIbot α ?_ hα ?_
-  · exact isIntegral_of_isScalarTower α.prop
+  · exact IsIntegral.tower_top α.prop
   · rw [minpoly_polyRoot' hp hζ u hcong hu]
     haveI := hI.isMaximal hIbot
     exact separable_poly hp hζ u hcong hu I
diff --git a/FltRegular/NumberTheory/MinpolyDiv.lean b/FltRegular/NumberTheory/MinpolyDiv.lean
index 8bbfd185..00e5922c 100644
--- a/FltRegular/NumberTheory/MinpolyDiv.lean
+++ b/FltRegular/NumberTheory/MinpolyDiv.lean
@@ -206,7 +206,7 @@ lemma sum_smul_minpolyDiv_eq_X_pow (E) [Field E] [IsAlgClosed E] [Algebra K E]
       refine ⟨finrank_pos, ?_⟩
       intro σ
       exact ((Polynomial.natDegree_smul_le _ _).trans (natDegree_map_le _ _)).trans_lt
-        ((natDegree_minpolyDiv_lt (Algebra.IsIntegral.of_finite x)).trans_le
+        ((natDegree_minpolyDiv_lt (Algebra.IsIntegral.of_finite _ _ x)).trans_le
           (minpoly.natDegree_le _))
     · rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card]
 
diff --git a/FltRegular/NumberTheory/QuotientTrace.lean b/FltRegular/NumberTheory/QuotientTrace.lean
index 51959ab9..1a10bd2b 100644
--- a/FltRegular/NumberTheory/QuotientTrace.lean
+++ b/FltRegular/NumberTheory/QuotientTrace.lean
@@ -143,10 +143,10 @@ def Algebra.intTrace (R S) [CommRing R] [CommRing S] [IsIntegrallyClosed R]
     [Algebra R S] [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [hRS : Module.Finite R S]
     [IsIntegrallyClosed S] : S →ₗ[R] R := by
   haveI : IsIntegralClosure S R (FractionRing S) :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite _ _)
   haveI : IsLocalization (algebraMapSubmonoid S R⁰) (FractionRing S) :=
     IsIntegralClosure.isLocalization' _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
   haveI : FiniteDimensional (FractionRing R) (FractionRing S) :=
     Module.Finite_of_isLocalization R S _ _ R⁰
   exact Algebra.intTraceAux R S (FractionRing R) (FractionRing S)
@@ -158,10 +158,10 @@ lemma Algebra.algebraMap_intTrace {R S K L} [CommRing R] [CommRing S] [Field K]
     [NoZeroSMulDivisors R S] [hRS : Module.Finite R S] (x : S) :
     algebraMap R K (Algebra.intTrace R S x) = Algebra.trace K L (algebraMap S L x) := by
   haveI : IsIntegralClosure S R (FractionRing S) :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S))
   haveI : IsLocalization (algebraMapSubmonoid S R⁰) (FractionRing S) :=
     IsIntegralClosure.isLocalization' _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
   haveI : FiniteDimensional (FractionRing R) (FractionRing S) :=
     Module.Finite_of_isLocalization R S _ _ R⁰
   haveI := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
@@ -181,10 +181,10 @@ lemma Algebra.algebraMap_intTrace_fractionRing {R S} [CommRing R] [CommRing S]
     algebraMap R (FractionRing R) (Algebra.intTrace R S x) =
       Algebra.trace (FractionRing R) (FractionRing S) (algebraMap S _ x) := by
   haveI : IsIntegralClosure S R (FractionRing S) :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S))
   haveI : IsLocalization (algebraMapSubmonoid S R⁰) (FractionRing S) :=
     IsIntegralClosure.isLocalization' _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
   haveI : FiniteDimensional (FractionRing R) (FractionRing S) :=
     Module.Finite_of_isLocalization R S _ _ R⁰
   exact Algebra.map_intTraceAux x
@@ -194,10 +194,10 @@ lemma Algebra.intTrace_eq_trace (R S) [CommRing R] [CommRing S] [IsIntegrallyClo
     [IsIntegrallyClosed S] [Module.Free R S] : Algebra.intTrace R S = Algebra.trace R S := by
   ext x
   haveI : IsIntegralClosure S R (FractionRing S) :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S))
   haveI : IsLocalization (algebraMapSubmonoid S R⁰) (FractionRing S) :=
     IsIntegralClosure.isLocalization' _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
   apply IsFractionRing.injective R (FractionRing R)
   rw [Algebra.algebraMap_intTrace_fractionRing, Algebra.trace_localization R R⁰]
 
@@ -238,13 +238,13 @@ lemma Algebra.intTrace_eq_of_isLocalization {R S} [CommRing R] [CommRing S] [Alg
   letI := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
     (algebraMapSubmonoid S p.primeCompl) Sₚ L
   haveI : IsIntegralClosure S R L :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S))
   haveI : IsLocalization (algebraMapSubmonoid S R⁰) L :=
     IsIntegralClosure.isLocalization' _ (FractionRing R) _ _
-      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (A := S)))
+      (isAlgebraic_of_isFractionRing _ _ (Algebra.IsIntegral.of_finite (R := R) (B := S)))
   haveI : FiniteDimensional K L := Module.Finite_of_isLocalization R S _ _ R⁰
   haveI : IsIntegralClosure Sₚ Rₚ L :=
-    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₚ) (A := Sₚ))
+    isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₚ) (B := Sₚ))
   apply IsFractionRing.injective Rₚ K
   rw [← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intTrace_fractionRing,
     Algebra.algebraMap_intTrace (L := L), ← IsScalarTower.algebraMap_apply]
diff --git a/lake-manifest.json b/lake-manifest.json
index 3ae188f0..773acac1 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "0c29911784aaca87ea2d4a2c8b1f311769402a7c",
+   "rev": "d3049643f6dded69eb7ce8124796cb1ec8df8840",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "909a2b4acca95430dc47b721044bfb6d091c4af7",
+   "rev": "f8794a02c68f154bbda8c213dcf859e52636e957",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,