diff --git a/FLT/AutomorphicForm/QuaternionAlgebra/Defs.lean b/FLT/AutomorphicForm/QuaternionAlgebra/Defs.lean
index 1a12cc19..da7e7cb6 100644
--- a/FLT/AutomorphicForm/QuaternionAlgebra/Defs.lean
+++ b/FLT/AutomorphicForm/QuaternionAlgebra/Defs.lean
@@ -33,7 +33,7 @@ noncomputable abbrev incl₁ : Dˣ →* Dfx F D :=
   Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom
 
 noncomputable abbrev incl₂ : (FiniteAdeleRing (𝓞 F) F)ˣ →* Dfx F D :=
-  Units.map Algebra.TensorProduct.rightAlgebra.toMonoidHom
+  Units.map Algebra.TensorProduct.rightAlgebra.algebraMap.toMonoidHom
 
 /-!
 This definition is made in mathlib-generality but is *not* the definition of an automorphic
diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
index 00992525..26421c0b 100644
--- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
+++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -1,12 +1,19 @@
+import Mathlib.Algebra.Algebra.Subalgebra.Pi
+import Mathlib.Algebra.Group.Int.TypeTags
+import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.Algebra.Order.Group.Int
 import Mathlib.FieldTheory.Separable
 import Mathlib.NumberTheory.RamificationInertia.Basic
+import Mathlib.Order.CompletePartialOrder
+import Mathlib.RingTheory.DedekindDomain.Dvr
 import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
-import Mathlib.RingTheory.DedekindDomain.IntegralClosure
-import Mathlib.Topology.Algebra.Algebra
+import Mathlib.RingTheory.Henselian
 import Mathlib.Topology.Algebra.Module.ModuleTopology
-import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
+import Mathlib.Topology.Separation.CompletelyRegular
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
 
+import Mathlib.RingTheory.DedekindDomain.IntegralClosure -- for example
+
 /-!
 
 # Base change of adele rings.
@@ -194,13 +201,18 @@ noncomputable def adicCompletionComapRingHom
 -- So we need to be careful making L_w into a K-algebra
 -- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/beef.20up.20smul.20on.20completion.20to.20algebra.20instance/near/484166527
 -- Hopefully resolved in https://github.com/leanprover-community/mathlib4/pull/19466
+variable (w : HeightOneSpectrum B) in
+noncomputable instance : SMul K (w.adicCompletion L) := inferInstanceAs <|
+  SMul K (@UniformSpace.Completion L w.adicValued.toUniformSpace)
+
 variable (w : HeightOneSpectrum B) in
 noncomputable instance : Algebra K (adicCompletion L w) where
-  toFun k := algebraMap L (adicCompletion L w) (algebraMap K L k)
-  map_one' := by simp only [map_one]
-  map_mul' k₁ k₂ := by simp only [map_mul]
-  map_zero' := by simp only [map_zero]
-  map_add' k₁ k₂ := by simp only [map_add]
+  algebraMap :=
+    { toFun k := algebraMap L (adicCompletion L w) (algebraMap K L k)
+      map_one' := by simp only [map_one]
+      map_mul' k₁ k₂ := by simp only [map_mul]
+      map_zero' := by simp only [map_zero]
+      map_add' k₁ k₂ := by simp only [map_add] }
   commutes' k lhat := mul_comm _ _
   smul_def' k lhat := by
     simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
@@ -253,8 +265,8 @@ lemma v_adicCompletionComapAlgHom
   · exact Valued.continuous_valuation.pow _
   · exact Valued.continuous_valuation.comp (adicCompletionComapAlgHom ..).cont
   intro a
-  simp only [Valued.valuedCompletion_apply, adicCompletionComapAlgHom_coe]
-  show v.valuation a ^ _ = (w.valuation _)
+  simp_rw [adicCompletionComapAlgHom_coe, adicCompletion, Valued.valuedCompletion_apply,
+    adicValued_apply]
   subst hvw
   rw [← valuation_comap A K L B w a]
 
diff --git a/FLT/DivisionAlgebra/Finiteness.lean b/FLT/DivisionAlgebra/Finiteness.lean
index 41bee032..fa25b24a 100644
--- a/FLT/DivisionAlgebra/Finiteness.lean
+++ b/FLT/DivisionAlgebra/Finiteness.lean
@@ -9,7 +9,6 @@ import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
 import Mathlib.Algebra.Group.Subgroup.Pointwise
 import FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
-import FLT.NumberField.IsTotallyReal
 import FLT.NumberField.AdeleRing
 import Mathlib.GroupTheory.DoubleCoset
 
diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
index 3bd6d5d1..fb105925 100644
--- a/FLT/FLT_files.lean
+++ b/FLT/FLT_files.lean
@@ -21,8 +21,6 @@ import FLT.Hard.Results
 import FLT.HIMExperiments.flatness
 import FLT.Junk.Algebra
 import FLT.Junk.Algebra2
-import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
-import FLT.Mathlib.Algebra.BigOperators.Finprod
 import FLT.Mathlib.Algebra.Group.Subgroup.Defs
 import FLT.Mathlib.Algebra.Module.LinearMap.Defs
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
@@ -32,7 +30,6 @@ import FLT.MathlibExperiments.Coalgebra.TensorProduct
 import FLT.MathlibExperiments.HopfAlgebra.Basic
 import FLT.MathlibExperiments.IsCentralSimple
 import FLT.MathlibExperiments.IsFrobenius
-import FLT.Mathlib.GroupTheory.Complement
 import FLT.Mathlib.GroupTheory.Index
 import FLT.Mathlib.LinearAlgebra.Determinant
 import FLT.Mathlib.LinearAlgebra.Span.Defs
@@ -47,5 +44,4 @@ import FLT.Mathlib.Topology.Constructions
 import FLT.Mathlib.Topology.Homeomorph
 import FLT.NumberField.AdeleRing
 import FLT.NumberField.InfiniteAdeleRing
-import FLT.NumberField.IsTotallyReal
 import FLT.TateCurve.TateCurve
diff --git a/FLT/GlobalLanglandsConjectures/GLnDefs.lean b/FLT/GlobalLanglandsConjectures/GLnDefs.lean
index 9bf02fe9..3fbd5368 100644
--- a/FLT/GlobalLanglandsConjectures/GLnDefs.lean
+++ b/FLT/GlobalLanglandsConjectures/GLnDefs.lean
@@ -166,7 +166,7 @@ variable (n : ℕ)
 variable (G : Type) [TopologicalSpace G] [Group G]
   (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E]
   [ChartedSpace E G]
-  [LieGroup 𝓘(ℝ, E) G]
+  [LieGroup 𝓘(ℝ, E) ⊤ G]
 
 def action :
     LeftInvariantDerivation 𝓘(ℝ, E) G →ₗ⁅ℝ⁆ (Module.End ℝ C^∞⟮𝓘(ℝ, E), G; ℝ⟯) where
diff --git a/FLT/GlobalLanglandsConjectures/GLzero.lean b/FLT/GlobalLanglandsConjectures/GLzero.lean
index 085304e5..227a0a21 100644
--- a/FLT/GlobalLanglandsConjectures/GLzero.lean
+++ b/FLT/GlobalLanglandsConjectures/GLzero.lean
@@ -80,7 +80,7 @@ def ofComplex (c : ℂ) : AutomorphicFormForGLnOverQ 0 ρ := {
       rw [annihilator]
       simp
       exact {
-        out := by sorry
+        fg_top := by sorry
       }
     has_finite_level := by
       let U : Subgroup (GL (Fin 0) (DedekindDomain.FiniteAdeleRing ℤ ℚ)) := {
diff --git a/FLT/HIMExperiments/flatness.lean b/FLT/HIMExperiments/flatness.lean
index d86cfbd2..180657e4 100644
--- a/FLT/HIMExperiments/flatness.lean
+++ b/FLT/HIMExperiments/flatness.lean
@@ -127,7 +127,7 @@ theorem flat_iff_torsion_eq_bot [IsPrincipalIdealRing R] [IsDomain R] :
     -- now assume R is a PID and M is a torsionfree R-module
   · intro htors
     -- we need to show that if I is an ideal of R then the natural map I ⊗ M → M is injective
-    constructor
+    rw [iff_lift_lsmul_comp_subtype_injective]
     rintro I -
     -- If I = 0 this is obvious because I ⊗ M is a subsingleton (i.e. has ≤1 element)
     obtain (rfl | h) := eq_or_ne I ⊥
diff --git a/FLT/Mathlib/Algebra/Algebra/Subalgebra/Pi.lean b/FLT/Mathlib/Algebra/Algebra/Subalgebra/Pi.lean
deleted file mode 100644
index 5e02768f..00000000
--- a/FLT/Mathlib/Algebra/Algebra/Subalgebra/Pi.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-import Mathlib.Algebra.Algebra.Pi
-import Mathlib.Algebra.Algebra.Subalgebra.Basic
-import Mathlib.LinearAlgebra.Pi
-
-def Subalgebra.pi {ι R : Type*} {S : ι → Type*} [CommSemiring R] [∀ i, Semiring (S i)]
-    [∀ i, Algebra R (S i)] (t : Set ι) (s : ∀ i, Subalgebra R (S i)) : Subalgebra R (Π i, S i) where
-  __ := Submodule.pi t (fun i ↦ (s i).toSubmodule)
-  mul_mem' hx hy i hi := (s i).mul_mem (hx i hi) (hy i hi)
-  algebraMap_mem' _ i _ := (s i).algebraMap_mem _
diff --git a/FLT/Mathlib/Algebra/BigOperators/Finprod.lean b/FLT/Mathlib/Algebra/BigOperators/Finprod.lean
deleted file mode 100644
index 646421fa..00000000
--- a/FLT/Mathlib/Algebra/BigOperators/Finprod.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-import Mathlib.Algebra.BigOperators.Finprod
-import Mathlib.Algebra.BigOperators.Pi
-
-@[to_additive]
-lemma finprod_option {ι : Type*} {B : Type*} [Finite ι] [CommMonoid B] (φ : Option ι → B) :
-    (∏ᶠ oi, φ oi) = φ none * ∏ᶠ (j : ι),  φ (some j) := by
-  rw [← finprod_mem_univ]
-  convert finprod_mem_insert φ (show none ∉ Set.range Option.some by aesop)
-    (Set.finite_range some)
-  · exact (Set.insert_none_range_some ι).symm
-  · rw [finprod_mem_range]
-    exact Option.some_injective ι
-
-@[to_additive]
-lemma finprod_apply {α ι N : Type*} [CommMonoid N] [Finite ι] (f : ι → α → N) (a : α) :
-    (∏ᶠ i, f i) a = ∏ᶠ i, (f i) a := by
-  classical
-  simp only [finprod_def, dif_pos (Set.toFinite _), Finset.prod_apply]
-  symm
-  apply Finset.prod_subset <;> aesop
diff --git a/FLT/Mathlib/Algebra/Module/LinearMap/Defs.lean b/FLT/Mathlib/Algebra/Module/LinearMap/Defs.lean
index 8a8c52e7..f8377d0c 100644
--- a/FLT/Mathlib/Algebra/Module/LinearMap/Defs.lean
+++ b/FLT/Mathlib/Algebra/Module/LinearMap/Defs.lean
@@ -1,6 +1,6 @@
+import Mathlib.Algebra.BigOperators.Finprod
 import Mathlib.Algebra.Module.LinearMap.Defs
 import Mathlib.Data.Fintype.Option
-import FLT.Mathlib.Algebra.BigOperators.Finprod
 
 theorem LinearMap.finsum_apply {R : Type*} [Semiring R] {A B : Type*} [AddCommMonoid A] [Module R A]
     [AddCommMonoid B] [Module R B] {ι : Type*} [Finite ι] (φ : ∀ _ : ι, A →ₗ[R] B) (a : A) :
@@ -12,4 +12,5 @@ theorem LinearMap.finsum_apply {R : Type*} [Semiring R] {A B : Type*} [AddCommMo
     · exact (finsum_comp_equiv e).symm
   · simp [finsum_of_isEmpty]
   · case h_option X _ hX =>
-    simp [finsum_option, hX]
+    rw [finsum_option (Set.toFinite _), finsum_option (Set.toFinite _)]
+    simp [hX]
diff --git a/FLT/Mathlib/GroupTheory/Complement.lean b/FLT/Mathlib/GroupTheory/Complement.lean
deleted file mode 100644
index 0b1af2a8..00000000
--- a/FLT/Mathlib/GroupTheory/Complement.lean
+++ /dev/null
@@ -1,54 +0,0 @@
-import Mathlib.GroupTheory.Complement
-
-open Set
-open scoped Pointwise
-
-namespace Subgroup
-variable {G : Type*} [Group G] {s t : Set G}
-
-@[to_additive (attr := simp)]
-lemma not_isComplement_empty_left : ¬ IsComplement ∅ t :=
-  fun h ↦ by simpa [eq_comm (a := ∅)] using h.mul_eq
-
-@[to_additive (attr := simp)]
-lemma not_isComplement_empty_right : ¬ IsComplement s ∅ :=
-  fun h ↦ by simpa [eq_comm (a := ∅)] using h.mul_eq
-
-@[to_additive]
-lemma IsComplement.nonempty_of_left (hst : IsComplement s t) : s.Nonempty := by
-  contrapose! hst; simp [hst]
-
-@[to_additive]
-lemma IsComplement.nonempty_of_right (hst : IsComplement s t) : t.Nonempty := by
-  contrapose! hst; simp [hst]
-
-@[to_additive] lemma IsComplement.pairwiseDisjoint_smul (hst : IsComplement s t) :
-    s.PairwiseDisjoint (· • t) := fun a ha b hb hab ↦ disjoint_iff_forall_ne.2 <| by
-  rintro _ ⟨c, hc, rfl⟩ _ ⟨d, hd, rfl⟩
-  exact hst.1.ne (a₁ := (⟨a, ha⟩, ⟨c, hc⟩)) (a₂:= (⟨b, hb⟩, ⟨d, hd⟩)) (by simp [hab])
-
-@[to_additive]
-lemma not_empty_mem_leftTransversals : ∅ ∉ leftTransversals s := not_isComplement_empty_left
-
-@[to_additive]
-lemma not_empty_mem_rightTransversals : ∅ ∉ rightTransversals s := not_isComplement_empty_right
-
-@[to_additive]
-lemma nonempty_of_mem_leftTransversals (hst : s ∈ leftTransversals t) : s.Nonempty :=
-  hst.nonempty_of_left
-
-@[to_additive]
-lemma nonempty_of_mem_rightTransversals (hst : s ∈ rightTransversals t) : s.Nonempty :=
-  hst.nonempty_of_right
-
-variable {H : Subgroup G} [H.FiniteIndex]
-
-@[to_additive]
-lemma finite_of_mem_leftTransversals (hs : s ∈ leftTransversals H) : s.Finite :=
-  Nat.finite_of_card_ne_zero <| by rw [card_left_transversal hs]; exact FiniteIndex.finiteIndex
-
-@[to_additive]
-lemma finite_of_mem_rightTransversals (hs : s ∈ rightTransversals H) : s.Finite :=
-  Nat.finite_of_card_ne_zero <| by rw [card_right_transversal hs]; exact FiniteIndex.finiteIndex
-
-end Subgroup
diff --git a/FLT/Mathlib/MeasureTheory/Group/Action.lean b/FLT/Mathlib/MeasureTheory/Group/Action.lean
index 9b4ec6c2..7842eb0b 100644
--- a/FLT/Mathlib/MeasureTheory/Group/Action.lean
+++ b/FLT/Mathlib/MeasureTheory/Group/Action.lean
@@ -1,8 +1,8 @@
+import Mathlib.GroupTheory.Complement
 import Mathlib.MeasureTheory.Group.Action
 import Mathlib.MeasureTheory.Group.Pointwise
 import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
 import FLT.Mathlib.Algebra.Group.Subgroup.Defs
-import FLT.Mathlib.GroupTheory.Complement
 import FLT.Mathlib.GroupTheory.Index
 
 /-!
@@ -45,12 +45,12 @@ instance (μ : Measure G) [μ.IsMulRightInvariant] :
 @[to_additive index_mul_addHaar_addSubgroup]
 lemma index_mul_haar_subgroup [H.FiniteIndex] (hH : MeasurableSet (H : Set G)) (μ : Measure G)
     [μ.IsMulLeftInvariant] : H.index * μ H = μ univ := by
-  obtain ⟨s, hs, -⟩ := H.exists_left_transversal 1
-  have hs' : Finite s := finite_of_mem_leftTransversals hs
+  obtain ⟨s, hs, -⟩ := H.exists_isComplement_left 1
+  have hs' : Finite s := hs.finite_left_iff.mpr inferInstance
   calc
     H.index * μ H = ∑' a : s, μ (a.val • H) := by
       simp [measure_smul]
-      rw [← Set.Finite.cast_ncard_eq hs', ← Nat.card_coe_set_eq, card_left_transversal hs]
+      rw [← Set.Finite.cast_ncard_eq hs', ← Nat.card_coe_set_eq, hs.card_left]
       norm_cast
     _ = μ univ := by
       rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]
diff --git a/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
deleted file mode 100644
index 07bca0f3..00000000
--- a/FLT/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
+++ /dev/null
@@ -1,37 +0,0 @@
-import Mathlib.RingTheory.DedekindDomain.AdicValuation
-
-open IsDedekindDomain
-
--- mathlib PR #20523
-namespace IsDedekindDomain.HeightOneSpectrum
-
-variable (R K : Type*) [CommRing R] [Field K] [IsDedekindDomain R] [Algebra R K]
-    [IsFractionRing R K] in
-theorem mem_integers_of_valuation_le_one (x : K)
-    (h : ∀ v : HeightOneSpectrum R, v.valuation x ≤ 1) : x ∈ (algebraMap R K).range := by
-  obtain ⟨⟨n, d, hd⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors R) x
-  obtain rfl : x = IsLocalization.mk' K n ⟨d, hd⟩ := IsLocalization.eq_mk'_iff_mul_eq.mpr hx
-  have hd0 := nonZeroDivisors.ne_zero hd
-  obtain rfl | hn0 := eq_or_ne n 0
-  · simp
-  suffices Ideal.span {d} ∣ (Ideal.span {n} : Ideal R) by
-    obtain ⟨z, rfl⟩ := Ideal.span_singleton_le_span_singleton.1 (Ideal.le_of_dvd this)
-    use z
-    rw [map_mul, mul_comm,mul_eq_mul_left_iff] at hx
-    cases' hx with h h
-    · exact h.symm
-    · simp [hd0] at h
-  classical
-  have ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥ := fun {r} ↦ mt Ideal.span_singleton_eq_bot.mp
-  rw [← Associates.mk_le_mk_iff_dvd, ← Associates.factors_le, Associates.factors_mk _ (ine hn0),
-    Associates.factors_mk _ (ine hd0), WithTop.coe_le_coe, Multiset.le_iff_count]
-  rintro ⟨v, hv⟩
-  obtain ⟨v, rfl⟩ := Associates.mk_surjective v
-  have hv' := hv
-  rw [Associates.irreducible_mk, irreducible_iff_prime] at hv
-  specialize h ⟨v, Ideal.isPrime_of_prime hv, hv.ne_zero⟩
-  simp_rw [valuation_of_mk', intValuation, ← Valuation.toFun_eq_coe,
-    intValuationDef_if_neg _ hn0, intValuationDef_if_neg _ hd0, ← WithZero.coe_div,
-    ← WithZero.coe_one, WithZero.coe_le_coe, Associates.factors_mk _ (ine hn0),
-    Associates.factors_mk _ (ine hd0), Associates.count_some hv'] at h
-  simpa using h
diff --git a/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean b/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
index aa463458..dfcf0d82 100644
--- a/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
+++ b/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
@@ -255,7 +255,7 @@ theorem Module.continuous_bilinear_of_pi_finite (ι : Type*) [Finite ι]
       -- Is there a missing delaborator? No ∑ᶠ notation
       change (∑ᶠ (i : ι), Pi.single i (f i)) j = f j
       -- last tactic has no effect
-      rw [finsum_apply]
+      rw [finsum_apply (Set.toFinite _)]
       convert finsum_eq_single (fun i ↦ Pi.single i (f i) j) j
         (by simp (config := {contextual := true})) using 1
       simp
diff --git a/FLT/NumberField/AdeleRing.lean b/FLT/NumberField/AdeleRing.lean
index 6dc3b3b2..f8b2b76a 100644
--- a/FLT/NumberField/AdeleRing.lean
+++ b/FLT/NumberField/AdeleRing.lean
@@ -1,9 +1,10 @@
 import Mathlib
 import FLT.Mathlib.NumberTheory.NumberField.Basic
-import FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation
 
 universe u
 
+open NumberField
+
 section LocallyCompact
 
 -- see https://github.com/smmercuri/adele-ring_locally-compact
@@ -11,7 +12,7 @@ section LocallyCompact
 
 variable (K : Type*) [Field K] [NumberField K]
 
-instance NumberField.AdeleRing.locallyCompactSpace : LocallyCompactSpace (AdeleRing K) :=
+instance NumberField.AdeleRing.locallyCompactSpace : LocallyCompactSpace (AdeleRing (𝓞 K) K) :=
   sorry -- issue #253
 
 end LocallyCompact
@@ -22,10 +23,10 @@ end BaseChange
 
 section Discrete
 
-open NumberField DedekindDomain
+open DedekindDomain
 
-theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
-    IsOpen U ∧ (algebraMap ℚ (AdeleRing ℚ)) ⁻¹' U = {0} := by
+theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing (𝓞 ℚ) ℚ),
+    IsOpen U ∧ (algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ)) ⁻¹' U = {0} := by
   use {f | ∀ v, f v ∈ (Metric.ball 0 1)} ×ˢ
     {f | ∀ v , f v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v}
   refine ⟨?_, ?_⟩
@@ -36,7 +37,7 @@ theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
     · intro x hx
       rw [Set.mem_preimage] at hx
       simp only [Set.mem_singleton_iff]
-      have : (algebraMap ℚ (AdeleRing ℚ)) x =
+      have : (algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ)) x =
         (algebraMap ℚ (InfiniteAdeleRing ℚ) x, algebraMap ℚ (FiniteAdeleRing (𝓞 ℚ) ℚ) x)
       · rfl
       rw [this] at hx
@@ -52,7 +53,7 @@ theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
       simp at h1
       have intx: ∃ (y:ℤ), y = x
       · obtain ⟨z, hz⟩ := IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one
-            (𝓞 ℚ) ℚ x <| fun v ↦ by
+            ℚ x <| fun v ↦ by
           specialize h2 v
           letI : UniformSpace ℚ := v.adicValued.toUniformSpace
           rw [IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers] at h2
@@ -88,11 +89,11 @@ theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
 -- Maybe this discreteness isn't even stated in the best way?
 -- I'm ambivalent about how it's stated
 open Pointwise in
-theorem Rat.AdeleRing.discrete : ∀ q : ℚ, ∃ U : Set (AdeleRing ℚ),
-    IsOpen U ∧ (algebraMap ℚ (AdeleRing ℚ)) ⁻¹' U = {q} := by
+theorem Rat.AdeleRing.discrete : ∀ q : ℚ, ∃ U : Set (AdeleRing (𝓞 ℚ) ℚ),
+    IsOpen U ∧ (algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ)) ⁻¹' U = {q} := by
   obtain ⟨V, hV, hV0⟩ := zero_discrete
   intro q
-  set ι  := algebraMap ℚ (AdeleRing ℚ)    with hι
+  set ι  := algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ)    with hι
   set qₐ := ι q                           with hqₐ
   set f  := Homeomorph.subLeft qₐ         with hf
   use f ⁻¹' V, f.isOpen_preimage.mpr hV
@@ -104,8 +105,8 @@ theorem Rat.AdeleRing.discrete : ∀ q : ℚ, ∃ U : Set (AdeleRing ℚ),
 
 variable (K : Type*) [Field K] [NumberField K]
 
-theorem NumberField.AdeleRing.discrete : ∀ k : K, ∃ U : Set (AdeleRing K),
-    IsOpen U ∧ (algebraMap K (AdeleRing K)) ⁻¹' U = {k} := sorry -- issue #257
+theorem NumberField.AdeleRing.discrete : ∀ k : K, ∃ U : Set (AdeleRing (𝓞 K) K),
+    IsOpen U ∧ (algebraMap K (AdeleRing (𝓞 K) K)) ⁻¹' U = {k} := sorry -- issue #257
 
 end Discrete
 
@@ -114,13 +115,13 @@ section Compact
 open NumberField
 
 theorem Rat.AdeleRing.cocompact :
-    CompactSpace (AdeleRing ℚ ⧸ AddMonoidHom.range (algebraMap ℚ (AdeleRing ℚ)).toAddMonoidHom) :=
+    CompactSpace (AdeleRing (𝓞 ℚ) ℚ ⧸ AddMonoidHom.range (algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ)).toAddMonoidHom) :=
   sorry -- issue #258
 
 variable (K : Type*) [Field K] [NumberField K]
 
 theorem NumberField.AdeleRing.cocompact :
-    CompactSpace (AdeleRing K ⧸ AddMonoidHom.range (algebraMap K (AdeleRing K)).toAddMonoidHom) :=
+    CompactSpace (AdeleRing (𝓞 K) K ⧸ AddMonoidHom.range (algebraMap K (AdeleRing (𝓞 K) K)).toAddMonoidHom) :=
   sorry -- issue #259
 
 end Compact
diff --git a/FLT/NumberField/IsTotallyReal.lean b/FLT/NumberField/IsTotallyReal.lean
deleted file mode 100644
index 3cc17bf1..00000000
--- a/FLT/NumberField/IsTotallyReal.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-import Mathlib.NumberTheory.NumberField.Basic
-import Mathlib.Data.Complex.Basic
-
-namespace NumberField
-
--- #20542
-class IsTotallyReal (F : Type*) [Field F] [NumberField F] : Prop where
-  isTotallyReal : ∀ τ : F →+* ℂ, ∀ f : F, ∃ r : ℝ, τ f = r
-
-instance : IsTotallyReal ℚ where
-  isTotallyReal τ q := ⟨q, by simp⟩
diff --git a/lake-manifest.json b/lake-manifest.json
index 13e96041..eccbb5c3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0291556f04e89d46cd2999f0f4c1164c81778207",
+   "rev": "8c60540fe18528a8a857d4d88094b005af61d97b",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
+   "rev": "e5ab45ea78696d399f7632d6fbc9007a1c32579f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/mhuisi/lean4-cli",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "470c41643209208d325a5a7315116f293c7443fb",
+   "rev": "b64b8eab8cfcf24c398e84b11c77b6555b61095a",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "46376bc3c8f46ac1a1fd7712856b0f7bd6166098",
+   "rev": "9e99cb8cd9ba6906472634e6973c7e27482a70bb",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e",
+   "rev": "26b1d510d9b5238d36b521d5367c707146fecd9d",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,10 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -95,30 +95,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
+   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.48",
+   "inputRev": "v0.0.50",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -135,10 +135,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "FLT",
diff --git a/lakefile.lean b/lakefile.lean
index 125bcbc6..a1d02a04 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -8,14 +8,14 @@ package FLT where
     ⟨`relaxedAutoImplicit, false⟩ -- switch off relaxed auto-implicit
   ]
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "master"
 
 require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
 -- This is run only if we're in `dev` mode. This is so not everyone has to build doc-gen
 meta if get_config? env = some "dev" then
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "v4.15.0"
+  "https://github.com/leanprover/doc-gen4" @ "v4.16.0-rc2"
 
 @[default_target]
 lean_lib FLT where
diff --git a/lean-toolchain b/lean-toolchain
index d0eb99ff..2ffc30ce 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0-rc2
\ No newline at end of file