diff --git a/FltRegular.lean b/FltRegular.lean
index f9693fa1..eca7cc89 100644
--- a/FltRegular.lean
+++ b/FltRegular.lean
@@ -29,4 +29,3 @@ import FltRegular.NumberTheory.RegularPrimes
 import FltRegular.NumberTheory.SystemOfUnits
 import FltRegular.NumberTheory.Unramified
 import FltRegular.ReadyForMathlib.Homogenization
-import FltRegular.ReadyForMathlib.PowerBasis
diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
index 1447820f..2fbbab81 100644
--- a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
@@ -3,7 +3,6 @@ import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import FltRegular.NumberTheory.Cyclotomic.CyclRat
 import Mathlib.RingTheory.Ideal.Norm
 import Mathlib.RingTheory.NormTrace
-import FltRegular.ReadyForMathlib.PowerBasis
 
 variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K]
 
@@ -90,10 +89,7 @@ lemma exists_zeta_sub_one_dvd_sub_Int (a : 𝓞 K) : ∃ b : ℤ, (hζ.unit' - 1
   letI : Fact (Nat.Prime p) := hpri
   simp_rw [← Ideal.Quotient.eq_zero_iff_dvd, ← Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_sub,
     sub_eq_zero, ← SModEq.def]
-  convert exists_int_sModEq hζ.subOneIntegralPowerBasis' a
-  rw [hζ.subOneIntegralPowerBasis'_gen]
-  rw [Subtype.ext_iff, AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one]
-  rfl
+  exact hζ.subOneIntegralPowerBasis'_gen ▸ hζ.subOneIntegralPowerBasis'.exists_smodEq a
 
 lemma exists_dvd_pow_sub_Int_pow (a : 𝓞 K) : ∃ b : ℤ, ↑p ∣ a ^ (p : ℕ) - (b : 𝓞 K) ^ (p : ℕ) := by
   obtain ⟨ζ, hζ⟩ := IsCyclotomicExtension.exists_prim_root ℚ (B := K) (Set.mem_singleton p)
diff --git a/FltRegular/ReadyForMathlib/PowerBasis.lean b/FltRegular/ReadyForMathlib/PowerBasis.lean
deleted file mode 100644
index 2dad68d4..00000000
--- a/FltRegular/ReadyForMathlib/PowerBasis.lean
+++ /dev/null
@@ -1,41 +0,0 @@
-import Mathlib.LinearAlgebra.SModEq
-import Mathlib.NumberTheory.NumberField.Basic
-
-open scoped NumberField
-
-open Ideal Finset Nat FiniteDimensional
-
-variable {K : Type*} [Field K] (pb : PowerBasis ℤ (𝓞 K))
-
-theorem exists_int_sModEq (x : 𝓞 K) :
-    ∃ (n : ℤ), SModEq (span ({ pb.gen } : Set (𝓞 K))) x n := by
-  refine ⟨(pb.basis.repr x) ⟨0, pb.dim_pos⟩, ?_⟩
-  have H := Basis.sum_repr pb.basis x
-  rw [PowerBasis.coe_basis, ← insert_erase (mem_univ (⟨0, pb.dim_pos⟩ : Fin pb.dim)), sum_insert] at H
-  · have :
-      ∀ i : (univ : Finset (Fin pb.dim)).erase ⟨0, pb.dim_pos⟩,
-        ↑((pb.basis.repr x) i) * pb.gen ^ ((i : Fin pb.dim) : ℕ) =
-          ↑((pb.basis.repr x) i) * pb.gen ^ (i : ℕ).pred.succ := by
-      rintro ⟨i, hi⟩
-      congr 1
-      rw [succ_pred_eq_of_pos]
-      rw [Subtype.coe_mk]
-      refine' Nat.pos_of_ne_zero fun h => _
-      cases' i with i₁ hi₁
-      simp only [Subtype.coe_mk] at h
-      simp only [mem_univ, not_true, mem_erase, ne_eq, Fin.mk.injEq, and_true] at hi
-      exact hi h
-    simp only [Fin.val_mk, _root_.pow_zero, zsmul_eq_mul] at H
-    rw [← Finset.sum_finset_coe] at H
-    conv_lhs at H =>
-      congr
-      rfl
-      congr
-      rfl
-      ext i
-      rw [this i, _root_.pow_succ, ← mul_assoc, mul_comm _ pb.gen]
-    rw [← mul_sum] at H
-    nth_rw 1 [← H]
-    rw [SModEq.sub_mem, mul_one, add_sub_cancel_left, mul_comm, mem_span_singleton']
-    exact ⟨_, rfl⟩
-  · exact not_mem_erase (⟨0, pb.dim_pos⟩ : Fin pb.dim) univ
diff --git a/lake-manifest.json b/lake-manifest.json
index a1b6471a..a2ed3ee2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "84542b3e09d0b491b76dc7b4eed87729001ca714",
+   "rev": "bb5c2ab8b54104352d8aaec9a606f327e5976028",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,