diff --git a/FLT/AutomorphicForm/QuaternionAlgebra.lean b/FLT/AutomorphicForm/QuaternionAlgebra.lean
index 0b320a13..fa3c83c3 100644
--- a/FLT/AutomorphicForm/QuaternionAlgebra.lean
+++ b/FLT/AutomorphicForm/QuaternionAlgebra.lean
@@ -3,12 +3,11 @@ Copyright (c) 2024 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard
 -/
-import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup
 import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
+import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
 import FLT.HIMExperiments.module_topology
---import Mathlib
 
 /-
 
diff --git a/FLT/AutomorphicRepresentation/Example.lean b/FLT/AutomorphicRepresentation/Example.lean
index c442b93c..1f244b70 100644
--- a/FLT/AutomorphicRepresentation/Example.lean
+++ b/FLT/AutomorphicRepresentation/Example.lean
@@ -278,13 +278,11 @@ lemma canonicalForm (z : QHat) : ∃ (N : ℕ+) (z' : ZHat), z = (1 / N : ℚ) 
     simp
   | tmul q z =>
     refine ⟨⟨q.den, q.den_pos ⟩, q.num * z, ?_⟩
-    simp only [← zsmul_eq_mul, TensorProduct.tmul_smul]
+    simp_rw [← zsmul_eq_mul, TensorProduct.tmul_smul, TensorProduct.smul_tmul']
     simp only [PNat.mk_coe, zsmul_eq_mul]
-    congr
-    · simp only [← q.mul_den_eq_num, LinearMap.mul_apply', mul_assoc,
-        one_div, ne_eq, Nat.cast_eq_zero, Rat.den_ne_zero, not_false_eq_true,
-        mul_inv_cancel, mul_one]
-    · simp
+    simp only [← q.mul_den_eq_num, LinearMap.mul_apply', mul_assoc,
+      one_div, ne_eq, Nat.cast_eq_zero, Rat.den_ne_zero, not_false_eq_true,
+      mul_inv_cancel, mul_one]
   | add x y hx hy =>
     obtain ⟨N₁, z₁, rfl⟩ := hx
     obtain ⟨N₂, z₂, rfl⟩ := hy
@@ -727,7 +725,7 @@ def norm (z : 𝓞) : ℤ :=
   - z.re * (z.im_o + z.im_oi) + z.im_i * (z.im_o - z.im_oi)
 
 lemma norm_eq_mul_conj (z : 𝓞) : (norm z : 𝓞) = z * star z := by
-  ext <;> simp [norm, ← Int.cast_add, -Int.cast_add] <;> ring
+  ext <;> simp [norm, ← Int.cast_add] <;> ring
 
 lemma coe_norm (z : 𝓞) :
     (norm z : ℝ) =
diff --git a/FLT/Basic/Reductions.lean b/FLT/Basic/Reductions.lean
index f16477f6..661c0a99 100644
--- a/FLT/Basic/Reductions.lean
+++ b/FLT/Basic/Reductions.lean
@@ -127,7 +127,6 @@ lemma gcdab_eq_gcdac {a b c : ℤ} {p : ℕ} (hp : 0 < p) (h : a ^ p + b ^ p = c
   apply Int.ofNat_dvd.1 at bar
   apply Int.ofNat_dvd.1 at foo
   exact congr_arg ((↑) : ℕ → ℤ) <| Nat.dvd_antisymm foo bar
-  done
 
 lemma hgcdac (P : FreyPackage) : gcd P.a P.c = 1 := by
   rw [← gcdab_eq_gcdac P.hppos P.hFLT, P.hgcdab]
diff --git a/FLT/GlobalLanglandsConjectures/GLnDefs.lean b/FLT/GlobalLanglandsConjectures/GLnDefs.lean
index cb7b7626..45f91878 100644
--- a/FLT/GlobalLanglandsConjectures/GLnDefs.lean
+++ b/FLT/GlobalLanglandsConjectures/GLnDefs.lean
@@ -3,20 +3,17 @@ Copyright (c) 2024 Kevin Buzzaed. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Jonas Bayer, Mario Carneiro
 -/
-import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup
-import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
-import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
+import Mathlib.Algebra.Lie.BaseChange
+import Mathlib.Algebra.Lie.UniversalEnveloping
 import Mathlib.Analysis.Complex.Basic
-import Mathlib.Topology.LocallyConstant.Basic
-import Mathlib.LinearAlgebra.UnitaryGroup
-import Mathlib.RepresentationTheory.FdRep
-import Mathlib.Analysis.Matrix
-import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup
-import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
 import Mathlib.Analysis.Matrix
 import Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
-import Mathlib.Algebra.Lie.UniversalEnveloping
-import Mathlib.Algebra.Lie.BaseChange
+import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
+import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
+import Mathlib.LinearAlgebra.UnitaryGroup
+import Mathlib.RepresentationTheory.FdRep
+import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
+import Mathlib.Topology.LocallyConstant.Basic
 
 suppress_compilation
 
@@ -67,22 +64,7 @@ lemma mem_FiniteAdeleRing (x : K_hat R K) : x ∈ (
 open Set
 
 /-- The finite adele ring is an algebra over the finite integral adeles. -/
-noncomputable instance : Algebra (R_hat R K) (FiniteAdeleRing R K) where
-  smul rhat fadele := ⟨fun v ↦ rhat v * fadele.1 v, by
-    have this := fadele.2
-    rw [mem_FiniteAdeleRing] at this ⊢
-    apply Finite.subset this (fun v hv ↦ ?_)
-    rw [mem_setOf_eq, mem_adicCompletionIntegers] at hv ⊢
-    contrapose! hv
-    sorry -- works in the PR, don't worry about this
-    ⟩
-  toFun r := ⟨r, by sorry⟩ -- works in the PR!
-  map_one' := by ext; rfl
-  map_mul' _ _ := by ext; rfl
-  map_zero' := by ext; rfl
-  map_add' _ _ := by ext; rfl
-  commutes' _ _ := mul_comm _ _
-  smul_def' r x := rfl
+noncomputable instance : Algebra (R_hat R K) (FiniteAdeleRing R K) := inferInstance
 
 end ProdAdicCompletions.IsFiniteAdele -- namespace
 
diff --git a/FLT/for_mathlib/Frobenius2.lean b/FLT/for_mathlib/Frobenius2.lean
index c95c9198..dbc30c04 100644
--- a/FLT/for_mathlib/Frobenius2.lean
+++ b/FLT/for_mathlib/Frobenius2.lean
@@ -3,10 +3,11 @@ 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.IntegralRestrict
+import Mathlib.RingTheory.Ideal.Pointwise
 import Mathlib.RingTheory.Ideal.QuotientOperations
-import Mathlib.FieldTheory.Cardinality
+import Mathlib.RingTheory.IntegralRestrict
 
 /-
 
@@ -79,21 +80,8 @@ i.e. supply the finiteness typeclasses and descent hypothesis in this case.
 
 variable (A : Type*) [CommRing A] {B : Type*} [CommRing B] [Algebra A B]
 
--- PR #13294
-variable {α : Type*} in
-instance Ideal.pointwiseMulSemiringAction
-    [Monoid α] [MulSemiringAction α B] : MulSemiringAction α (Ideal B) where
-  smul a I := Ideal.map (MulSemiringAction.toRingHom _ _ a) I
-  one_smul I :=
-    congr_arg (I.map ·) (RingHom.ext <| one_smul α) |>.trans I.map_id
-  mul_smul _a₁ _a₂ I :=
-    congr_arg (I.map ·) (RingHom.ext <| mul_smul _ _) |>.trans (I.map_map _ _).symm
-  smul_one a := by simp only [Ideal.one_eq_top]; exact Ideal.map_top _
-  smul_mul a I J := Ideal.map_mul _ I J
-  smul_add a I J := Ideal.map_sup _ I J
-  smul_zero a := Ideal.map_bot
-
--- should be in #13294?
+open scoped Pointwise
+
 variable {α : Type*} in
 lemma Ideal.map_eq_comap_symm [Group α] [MulSemiringAction α B] (J : Ideal B) (σ : α) :
     σ • J = J.comap (MulSemiringAction.toRingHom _ _ σ⁻¹) :=
@@ -329,7 +317,6 @@ lemma Frob_Q_eq_pow_card (x : B) : Frob A Q isGalois P x - x^(Fintype.card (A⧸
     rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem]
     change ((Frob A Q isGalois P) x : B ⧸ Q) = x ^ Fintype.card (A ⧸ P)
     rw [← hn2]
-    push_cast
     have fact1 := Frob_spec A Q isGalois P
     have fact2 : y A Q = (g Q : B⧸Q) := y_mod_Q A Q
     rw [← fact2]
@@ -345,10 +332,7 @@ lemma Frob_Q_eq_pow_card (x : B) : Frob A Q isGalois P x - x^(Fintype.card (A⧸
     rw [← smul_sub]
     nth_rw 3 [ ← fact3]
     suffices (x - y A Q ^ n) ∈ Q by
-      exact?
-    rw [smul_mem_smul]
-    simp
-    skip
+      exact? says exact Ideal.smul_mem_pointwise_smul_iff.mpr this
     sorry
 
 /- maths proof:
diff --git a/lake-manifest.json b/lake-manifest.json
index 9521dd52..30722bb0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
+   "scope": "leanprover-community",
+   "rev": "dc4a6b1ac3cd502988e283d5c9c5fdf261125a07",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,6 +14,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
+   "scope": "leanprover-community",
    "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
+   "scope": "leanprover-community",
+   "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
+   "scope": "leanprover-community",
+   "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +64,8 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "b84002db251bdfe6d7796c16364cfb47fdc9cf95",
+   "scope": "",
+   "rev": "363b8176ac29271af4b000b649f836c846f528fc",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -67,17 +74,19 @@
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "21a36f3c07a9229e1287483c16a0dd04e479ecc5",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/xubaiw/CMark.lean",
+  {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
-   "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
-   "name": "CMark",
+   "scope": "",
+   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
+   "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -85,25 +94,18 @@
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "effd8b8771cfd7ece69db99448168078e113c61f",
+   "scope": "",
+   "rev": "c74a052aebee847780e165611099854de050adf7",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargonix/LeanInk",
-   "type": "git",
-   "subDir": null,
-   "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f",
-   "name": "leanInk",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "doc-gen",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "c7f4ac84b973b6efd8f24ba2b006cad1b32c9c53",
+   "scope": "",
+   "rev": "b5197b656018a2d929e025f41aca5ba463557dd1",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 29c0cea4..d69d1ed2 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc2
+leanprover/lean4:v4.10.0-rc1