diff --git a/FLT.lean b/FLT.lean
index ca557983..79429319 100644
--- a/FLT.lean
+++ b/FLT.lean
@@ -1,36 +1,39 @@
-import FLT.FLT_files -- import the project files
-
-/-!
-
-# Fermat's Last Theorem
-
-There are many ways of stating Fermat's Last Theorem.
-In this file, we give the traditional statement using
-the positive integers `ℕ+`, and deduce it from
-a proof of Mathlib's version `FermatLastTheorem`
-of the statement (which is a statement about the
-nonnegative integers `ℕ`.)
-
-Note that many of the files imported by this file contain
-"sorried" theorems, that is, theorems whose proofs
-are not yet complete. So whilst the below looks
-like a complete proof of Fermat's Last Theorem, it
-currently relies on many incomplete proofs along the way,
-and is likely to do so for several years.
-
--/
-
-/-- Fermat's Last Theorem for positive naturals. -/
-theorem PNat.pow_add_pow_ne_pow
-    (x y z : ℕ+)
-    (n : ℕ) (hn : n > 2) :
-    x^n + y^n ≠ z^n :=
-  PNat.pow_add_pow_ne_pow_of_FermatLastTheorem FLT.Wiles_Taylor_Wiles x y z n hn
-
-#print axioms PNat.pow_add_pow_ne_pow
-/-
-'PNat.pow_add_pow_ne_pow' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
--/
-
--- The project will be complete when `sorryAx` is no longer
--- mentioned in the output of this last command.
+import FLT.AutomorphicForm.QuaternionAlgebra.Defs
+import FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional
+import FLT.AutomorphicRepresentation.Example
+import FLT.Basic.Reductions
+import FLT.DedekindDomain.FiniteAdeleRing.BaseChange
+import FLT.DivisionAlgebra.Finiteness
+import FLT.EllipticCurve.Torsion
+import FLT.FLT_files
+import FLT.ForMathlib.ActionTopology
+import FLT.ForMathlib.Algebra
+import FLT.ForMathlib.DomMulActMeasure
+import FLT.ForMathlib.MiscLemmas
+import FLT.ForMathlib.Topology.Algebra.Algebra
+import FLT.FromMathlib.Algebra
+import FLT.GaloisRepresentation.Cyclotomic
+import FLT.GaloisRepresentation.HardlyRamified
+import FLT.GlobalLanglandsConjectures.GLnDefs
+import FLT.GlobalLanglandsConjectures.GLzero
+import FLT.GroupScheme.FiniteFlat
+import FLT.HIMExperiments.flatness
+import FLT.HaarMeasure.DistribHaarChar
+import FLT.Hard.Results
+import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
+import FLT.Mathlib.Algebra.Order.Hom.Monoid
+import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
+import FLT.Mathlib.Data.ENNReal.Inv
+import FLT.MathlibExperiments.Coalgebra.Monoid
+import FLT.MathlibExperiments.Coalgebra.Sweedler
+import FLT.MathlibExperiments.Coalgebra.TensorProduct
+import FLT.MathlibExperiments.Frobenius
+import FLT.MathlibExperiments.Frobenius2
+import FLT.MathlibExperiments.FrobeniusRiou
+import FLT.MathlibExperiments.HopfAlgebra.Basic
+import FLT.MathlibExperiments.IsCentralSimple
+import FLT.MathlibExperiments.IsFrobenius
+import FLT.NumberField.AdeleRing
+import FLT.NumberField.InfiniteAdeleRing
+import FLT.NumberField.IsTotallyReal
+import FLT.TateCurve.TateCurve
diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
index 6ecd3312..0a5d9e62 100644
--- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
+++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -1,10 +1,11 @@
-import Mathlib -- **TODO** fix when finished or if `exact?` is too slow
---import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
---import Mathlib.NumberTheory.NumberField.Basic
---import Mathlib.NumberTheory.RamificationInertia
-import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
-import FLT.Mathlib.Algebra.Order.Hom.Monoid
+import Mathlib.FieldTheory.Separable
+import Mathlib.NumberTheory.RamificationInertia.Basic
+import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
+import Mathlib.RingTheory.DedekindDomain.IntegralClosure
+import Mathlib.Topology.Algebra.Algebra
+import Mathlib.Topology.Algebra.Module.ModuleTopology
 import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
+import FLT.Mathlib.Algebra.Order.Hom.Monoid
 
 /-!
 
@@ -275,6 +276,7 @@ noncomputable def adicCompletionTensorComapAlgHom (v : HeightOneSpectrum A) :
       Π w : {w : HeightOneSpectrum B // v = comap A w}, adicCompletion L w.1 :=
   Algebra.TensorProduct.lift (Algebra.ofId _ _) (adicCompletionComapAlgHom' A K L B v) fun _ _ ↦ .all _ _
 
+omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L] in
 lemma adicCompletionComapAlgIso_tmul_apply (v : HeightOneSpectrum A) (x y i) :
   adicCompletionTensorComapAlgHom A K L B v (x ⊗ₜ y) i =
     x • adicCompletionComapAlgHom A K L B v i.1 i.2 y := by
@@ -302,6 +304,7 @@ noncomputable def tensorAdicCompletionIntegersTo (v : HeightOneSpectrum A) :
     ((Algebra.TensorProduct.includeRight.restrictScalars A).comp (IsScalarTower.toAlgHom _ _ _))
     (fun _ _ ↦ .all _ _)
 
+omit [IsIntegralClosure B A L] [FiniteDimensional K L] [Algebra.IsSeparable K L] in
 set_option linter.deprecated false in -- `map_zero` and `map_add` time-outs
 theorem range_adicCompletionComapAlgIso_tensorAdicCompletionIntegersTo_le_pi
     (v : HeightOneSpectrum A) :
diff --git a/FLT/GlobalLanglandsConjectures/GLnDefs.lean b/FLT/GlobalLanglandsConjectures/GLnDefs.lean
index d57b2193..38918d70 100644
--- a/FLT/GlobalLanglandsConjectures/GLnDefs.lean
+++ b/FLT/GlobalLanglandsConjectures/GLnDefs.lean
@@ -285,7 +285,7 @@ noncomputable def preweight.fdRep (n : ℕ) (w : preweight n) :
     FDRep ℂ (orthogonalGroup (Fin n) ℝ) where
   V := FGModuleCat.of ℂ (Fin w.d → ℂ)
   ρ := {
-    toFun := fun A ↦ {
+    toFun := fun A ↦ ModuleCat.ofHom {
       toFun := fun x ↦ (w.rho A).1 *ᵥ x
       map_add' := fun _ _ ↦ Matrix.mulVec_add ..
       map_smul' := fun _ _ ↦ by simpa using Matrix.mulVec_smul .. }
diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
index a26924a8..d3c1e87a 100644
--- a/FLT/MathlibExperiments/FrobeniusRiou.lean
+++ b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -3,15 +3,8 @@ Copyright (c) 2024 Jou Glasheen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jou Glasheen, Amelia Livingston, Jujian Zhang, Kevin Buzzard
 -/
-import Mathlib.FieldTheory.Cardinality
-import Mathlib.RingTheory.DedekindDomain.Ideal
-import Mathlib.RingTheory.Ideal.Pointwise
-import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
-import Mathlib.RingTheory.Ideal.Pointwise
-import Mathlib.RingTheory.Ideal.Over
-import Mathlib.FieldTheory.Normal
 import Mathlib.FieldTheory.SeparableClosure
-import Mathlib.RingTheory.OreLocalization.Ring
+import Mathlib.RingTheory.Ideal.Over
 
 /-!
 
@@ -21,7 +14,7 @@ This file proves a general result in commutative algebra which can be used to de
 elements of Galois groups of local or fields (for example number fields).
 
 KB was alerted to this very general result (which needs no Noetherian or finiteness assumptions
-on the rings, just on the Galois group) by Joel Riou
+on the rings, just on the Galois group) by Joël Riou
 here https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Uses.20of.20Frobenius.20elements.20in.20mathematics/near/448934112
 
 ## Mathematical details
@@ -696,9 +689,6 @@ open scoped algebraMap
 noncomputable local instance : Algebra A[X] B[X] :=
   RingHom.toAlgebra (Polynomial.mapRingHom (Algebra.toRingHom))
 
-theorem IsAlgebraic.mul {R K : Type*} [CommRing R] [CommRing K] [Algebra R K] {x y : K}
-  (hx : IsAlgebraic R x) (hy : IsAlgebraic R y) : IsAlgebraic R (x * y) := sorry
-
 theorem IsAlgebraic.invLoc {R S K : Type*} [CommRing R] {M : Submonoid R} [CommRing S] [Algebra R S]
     [IsLocalization M S] {x : M} [CommRing K] [Algebra K S] (h : IsAlgebraic K ((x : R) : S)):
     IsAlgebraic K (IsLocalization.mk' S 1 x) := by
@@ -734,7 +724,7 @@ theorem algebraMap_algebraMap {R S T : Type*} [CommRing R] [CommRing S] [CommRin
   exact Eq.symm (IsScalarTower.algebraMap_apply R S T r)
 
 theorem Algebra.isAlgebraic_of_subring_isAlgebraic {R k K : Type*} [CommRing R] [CommRing k]
-    [CommRing K] [Algebra R K] [IsFractionRing R K] [Algebra k K]
+    [CommRing K] [Algebra R K] [IsFractionRing R K] [Algebra k K] [NoZeroDivisors k]
     (h : ∀ x : R, IsAlgebraic k (x : K)) : Algebra.IsAlgebraic k K := by
   rw [Algebra.isAlgebraic_def]
   let M := nonZeroDivisors R
diff --git a/FLT/NumberField/AdeleRing.lean b/FLT/NumberField/AdeleRing.lean
index 94f4f3f5..456c1f67 100644
--- a/FLT/NumberField/AdeleRing.lean
+++ b/FLT/NumberField/AdeleRing.lean
@@ -1,5 +1,12 @@
 import Mathlib
 
+/-!
+# TODO
+
+Is it expected that `InfinitePlace.Completion.Rat.norm_infinitePlace_completion` is called like
+that, rather than just `Rat.norm_infinitePlace_completion`?
+-/
+
 universe u
 
 section LocallyCompact
@@ -22,13 +29,6 @@ section Discrete
 
 open NumberField DedekindDomain
 
--- mathlib PR #19644
-lemma Rat.norm_infinitePlace_completion (v : InfinitePlace ℚ) (x : ℚ) :
-    ‖(x : v.completion)‖ = |x| := sorry -- this will be done when the mathlib PR is merged
-
--- mathlib PR #19644
-noncomputable def Rat.infinitePlace : InfinitePlace ℚ := .mk (Rat.castHom _)
-
 theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
     IsOpen U ∧ (algebraMap ℚ (AdeleRing ℚ)) ⁻¹' U = {0} := by
   use {f | ∀ v, f v ∈ (Metric.ball 0 1)} ×ˢ
diff --git a/lake-manifest.json b/lake-manifest.json
index 56490466..e37c0944 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "099b90e374ba73983c3fda87595be625f1931669",
+   "rev": "4e07f9201e4e4452cd24cf2bd217e93d28f68a69",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8e459c606cbf19248c6a59956570f051f05e6067",
+   "rev": "7edf946a4217aa3aa911290811204096e8464ada",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "41ff1f7899c971f91362710d4444e338b8acd644",
+   "rev": "31530f31d529f37cde81d086fe10b68e9eb1ee2f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -115,10 +115,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8b6048aa0a4a4b6bcf83597802d8dee734e64b7e",
+   "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -135,10 +135,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7805acf1864ba1a2e359f86a8f092ccf1438ad83",
+   "rev": "c016aa9938c4cedc9b7066099f99bcae1b1af625",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "FLT",