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..c0bda069 100644
--- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
+++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -4,8 +4,8 @@ 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
+import Mathlib
 
 /-!
 
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..25360bf4 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
@@ -47,5 +45,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/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..5d81432b 100644
--- a/FLT/Mathlib/Algebra/Module/LinearMap/Defs.lean
+++ b/FLT/Mathlib/Algebra/Module/LinearMap/Defs.lean
@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Module.LinearMap.Defs
 import Mathlib.Data.Fintype.Option
-import FLT.Mathlib.Algebra.BigOperators.Finprod
+import Mathlib
 
 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 sorry, finsum_option sorry] -- -- new finiteness goals?
+    simp [hX]
diff --git a/FLT/Mathlib/GroupTheory/Complement.lean b/FLT/Mathlib/GroupTheory/Complement.lean
index 0b1af2a8..f7f8183d 100644
--- a/FLT/Mathlib/GroupTheory/Complement.lean
+++ b/FLT/Mathlib/GroupTheory/Complement.lean
@@ -6,14 +6,6 @@ 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]
@@ -22,11 +14,6 @@ lemma IsComplement.nonempty_of_left (hst : IsComplement s t) : s.Nonempty := by
 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
 
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..c1c4833f 100644
--- a/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
+++ b/FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean
@@ -259,6 +259,7 @@ theorem Module.continuous_bilinear_of_pi_finite (ι : Type*) [Finite ι]
       convert finsum_eq_single (fun i ↦ Pi.single i (f i) j) j
         (by simp (config := {contextual := true})) using 1
       simp
+      sorry -- new finiteness goal?
     · apply Set.toFinite _--(Function.support fun x ↦ f x • Pi.single x 1)
   rw [foo]
   haveI : ContinuousAdd C := toContinuousAdd R C
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..3b3e1107 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": "15f16b1ec50f425147926be1aede7b4baa725380",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc2",
    "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": "c104265c34eb8181af14e8dbc14c2f034292cb02",
    "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..ab68c3bf 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" @ "v4.16.0-rc2"
 
 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