diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
index 89637f8a..e0ccb3ce 100644
--- a/FLT/FLT_files.lean
+++ b/FLT/FLT_files.lean
@@ -8,7 +8,6 @@ import FLT.EllipticCurve.Torsion
 import FLT.ForMathlib.ActionTopology
 import FLT.ForMathlib.Algebra
 import FLT.ForMathlib.DomMulActMeasure
-import FLT.ForMathlib.MeasurableSpacePadics
 import FLT.ForMathlib.MiscLemmas
 import FLT.ForMathlib.Topology.Algebra.Algebra
 import FLT.FromMathlib.Algebra
@@ -33,6 +32,7 @@ import FLT.Mathlib.GroupTheory.Complement
 import FLT.Mathlib.LinearAlgebra.Determinant
 import FLT.Mathlib.MeasureTheory.Group.Action
 import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+import FLT.Mathlib.NumberTheory.Padics.MeasurableSpacePadics
 import FLT.Mathlib.RingTheory.Norm.Defs
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler
diff --git a/FLT/HaarMeasure/ConcreteCharCalculations.lean b/FLT/HaarMeasure/ConcreteCharCalculations.lean
index 842f68c3..6c826798 100644
--- a/FLT/HaarMeasure/ConcreteCharCalculations.lean
+++ b/FLT/HaarMeasure/ConcreteCharCalculations.lean
@@ -3,13 +3,13 @@ import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 import Mathlib.RingTheory.Complex
 import Mathlib.RingTheory.Localization.NumDen
 import Mathlib.Analysis.Normed.Group.Ultra
-import FLT.ForMathlib.MeasurableSpacePadics
 import FLT.HaarMeasure.DistribHaarChar
 import FLT.Mathlib.Analysis.Complex.Basic
 import FLT.Mathlib.Data.Complex.Basic
 import FLT.Mathlib.LinearAlgebra.Determinant
 import FLT.Mathlib.MeasureTheory.Group.Action
 import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+import FLT.Mathlib.NumberTheory.Padics.MeasurableSpacePadics
 import FLT.Mathlib.RingTheory.Norm.Defs
 
 open Real Complex Padic MeasureTheory Measure NNReal Set TopologicalSpace