diff --git a/ClassFieldTheory.lean b/ClassFieldTheory.lean
index 3a3141da..a4c7bc49 100644
--- a/ClassFieldTheory.lean
+++ b/ClassFieldTheory.lean
@@ -40,13 +40,11 @@ import ClassFieldTheory.IsNonarchimedeanLocalField.ValuationExactSequence
 import ClassFieldTheory.LocalCFT.Continuity
 import ClassFieldTheory.LocalCFT.Teichmuller
 import ClassFieldTheory.Mathlib.Algebra.Algebra.Subalgebra.Basic
-import ClassFieldTheory.Mathlib.Algebra.Group.Action.Units
 import ClassFieldTheory.Mathlib.Algebra.Group.Solvable
-import ClassFieldTheory.Mathlib.Algebra.Group.Units.Basic
+import ClassFieldTheory.Mathlib.Algebra.Group.Units.Defs
 import ClassFieldTheory.Mathlib.Algebra.Group.Units.Hom
 import ClassFieldTheory.Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import ClassFieldTheory.Mathlib.Algebra.Homology.ConcreteCategory
-import ClassFieldTheory.Mathlib.Algebra.Homology.ImageToKernel
 import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
 import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.Exact
 import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.ModuleCat
@@ -54,13 +52,10 @@ import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.ShortExact
 import ClassFieldTheory.Mathlib.Algebra.Module.Equiv.Basic
 import ClassFieldTheory.Mathlib.Algebra.Module.Equiv.Defs
 import ClassFieldTheory.Mathlib.Algebra.Module.LinearMap.Defs
-import ClassFieldTheory.Mathlib.Algebra.Module.NatInt
-import ClassFieldTheory.Mathlib.Algebra.Module.Submodule.Range
 import ClassFieldTheory.Mathlib.Algebra.Module.Torsion.Basic
+import ClassFieldTheory.Mathlib.Algebra.Order.Group.OrderIso
 import ClassFieldTheory.Mathlib.Algebra.Order.GroupWithZero.Canonical
-import ClassFieldTheory.Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
 import ClassFieldTheory.Mathlib.Algebra.Order.Hom.Monoid
-import ClassFieldTheory.Mathlib.CategoryTheory.Abelian.Exact
 import ClassFieldTheory.Mathlib.CategoryTheory.Category.Basic
 import ClassFieldTheory.Mathlib.CategoryTheory.Category.Cat
 import ClassFieldTheory.Mathlib.Data.Finset.Range
diff --git a/ClassFieldTheory/Cohomology/AugmentationModule.lean b/ClassFieldTheory/Cohomology/AugmentationModule.lean
index 34fa165e..0f1c8eb5 100644
--- a/ClassFieldTheory/Cohomology/AugmentationModule.lean
+++ b/ClassFieldTheory/Cohomology/AugmentationModule.lean
@@ -1,5 +1,5 @@
 import ClassFieldTheory.Cohomology.Functors.Restriction
-import ClassFieldTheory.Cohomology.Functors.UpDown
+import ClassFieldTheory.Cohomology.IndCoind.TrivialCohomology
 import ClassFieldTheory.Cohomology.LeftRegular
 import ClassFieldTheory.Cohomology.TrivialCohomology
 import ClassFieldTheory.Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
diff --git a/ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean b/ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean
index 34d4349e..f7968e1d 100644
--- a/ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean
+++ b/ClassFieldTheory/Cohomology/FiniteCyclic/UpDown.lean
@@ -1,9 +1,7 @@
 import ClassFieldTheory.Cohomology.Functors.UpDown
 import ClassFieldTheory.Cohomology.IndCoind.Finite
-import ClassFieldTheory.Mathlib.Algebra.Homology.ImageToKernel
 import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.Exact
 import ClassFieldTheory.Mathlib.Algebra.Homology.ShortComplex.ModuleCat
-import ClassFieldTheory.Mathlib.CategoryTheory.Abelian.Exact
 import ClassFieldTheory.Mathlib.GroupTheory.SpecificGroups.Cyclic
 
 /-!
diff --git a/ClassFieldTheory/Cohomology/Functors/Corestriction.lean b/ClassFieldTheory/Cohomology/Functors/Corestriction.lean
index 47cec077..bb209fed 100644
--- a/ClassFieldTheory/Cohomology/Functors/Corestriction.lean
+++ b/ClassFieldTheory/Cohomology/Functors/Corestriction.lean
@@ -4,12 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Aaron Liu, Yunzhou Xie
 -/
 import ClassFieldTheory.Cohomology.Functors.UpDown
-import ClassFieldTheory.Mathlib.GroupTheory.GroupAction.Quotient
+import ClassFieldTheory.Mathlib.Algebra.Module.Torsion.Basic
 import ClassFieldTheory.Mathlib.CategoryTheory.Category.Basic
 import ClassFieldTheory.Mathlib.CategoryTheory.Category.Cat
+import ClassFieldTheory.Mathlib.GroupTheory.GroupAction.Quotient
 import ClassFieldTheory.Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
-import ClassFieldTheory.Mathlib.Algebra.Module.NatInt
-import ClassFieldTheory.Mathlib.Algebra.Module.Torsion.Basic
 
 /-!
 # Corestriction
@@ -303,14 +302,15 @@ lemma torsion_of_finite_of_neZero {n : ℕ} [NeZero n] [DecidableEq G] (M : Rep
 
 lemma pTorsion_eq_sylowTorsion {n : ℕ} [NeZero n] [Finite G] [DecidableEq G] (M : Rep R G)
     (p : ℕ) [Fact p.Prime] (P : Sylow p G) (x : groupCohomology M n) :
-    (∃ d, (p ^ d) • x = 0) ↔ x ∈ Submodule.torsionBy R _ (Nat.card P) :=
-  ⟨fun ⟨d, hd⟩ ↦ Submodule.mem_torsionBy_iff _ _ |>.2 <| by
+    (∃ d, (p ^ d) • x = 0) ↔ x ∈ Submodule.torsionBy R _ (Nat.card P) where
+  mp := by
+    rintro ⟨d, hd⟩
     obtain ⟨k, hk1, hk2⟩ := Nat.dvd_prime_pow Fact.out|>.1 <| Nat.gcd_dvd_right (Nat.card G) (p ^ d)
     obtain ⟨m, hm⟩ := P.pow_dvd_card_of_pow_dvd_card (hk2 ▸ Nat.gcd_dvd_left (Nat.card G) (p ^ d))
-    simp [hm, mul_comm _ m, mul_smul, - Nat.cast_pow, Nat.cast_smul_eq_nsmul, ← hk2,
-      AddCommGroup.isTorsion_gcd_iff _ (p ^ d) x|>.2 ⟨torsion_of_finite_of_neZero M x, hd⟩],
-    fun h ↦ ⟨(Nat.card G).factorization p, P.card_eq_multiplicity ▸ by
-    simpa [Nat.cast_smul_eq_nsmul] using h⟩⟩
+    simp [hm, mul_comm _ m, mul_smul, - Nat.cast_pow, Nat.cast_smul_eq_nsmul, ← hk2, smul_comm m]
+    simp [smul_comm _ m, hd, torsion_of_finite_of_neZero]
+  mpr h := ⟨(Nat.card G).factorization p, P.card_eq_multiplicity ▸ by
+    simpa [Nat.cast_smul_eq_nsmul] using h⟩
 
 lemma injects_to_sylowCoh {n : ℕ} [NeZero n] [Finite G] [DecidableEq G] (M : Rep R G)
     (p : ℕ) [Fact p.Prime] (P : Sylow p G) : Function.Injective
diff --git a/ClassFieldTheory/Cohomology/IndCoind/TrivialCohomology.lean b/ClassFieldTheory/Cohomology/IndCoind/TrivialCohomology.lean
index 6d82af63..7deca865 100644
--- a/ClassFieldTheory/Cohomology/IndCoind/TrivialCohomology.lean
+++ b/ClassFieldTheory/Cohomology/IndCoind/TrivialCohomology.lean
@@ -6,7 +6,6 @@ Authors: Yaël Dillies, Nailin Guan, Gareth Ma, Arend Mellendijk, Yannis Monbru,
 -/
 import ClassFieldTheory.Cohomology.IndCoind.Finite
 import ClassFieldTheory.Cohomology.TrivialCohomology
-import ClassFieldTheory.Mathlib.Algebra.Module.Submodule.Range
 import ClassFieldTheory.Mathlib.LinearAlgebra.Finsupp.Defs
 import ClassFieldTheory.Mathlib.RepresentationTheory.Rep
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro
diff --git a/ClassFieldTheory/Cohomology/Subrep/Basic.lean b/ClassFieldTheory/Cohomology/Subrep/Basic.lean
index c315f5aa..0d1f45be 100644
--- a/ClassFieldTheory/Cohomology/Subrep/Basic.lean
+++ b/ClassFieldTheory/Cohomology/Subrep/Basic.lean
@@ -14,19 +14,20 @@ structure Subrep {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) extends Su
   le_comap (g) : toSubmodule ≤ toSubmodule.comap (A.ρ g)
 
 namespace Subrep
-variable {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G)
+variable {k G : Type u} [CommRing k] [Monoid G] {A : Rep k G}
+
+lemma toSubmodule_injective : (toSubmodule : Subrep A → Submodule k A.V).Injective :=
+  fun ⟨_, _⟩ _ _ ↦ by congr!
 
 instance : SetLike (Subrep A) A.V where
   coe w := w.carrier
-  coe_injective' := fun ⟨_, _⟩ ⟨_, _⟩ h ↦ by congr; exact SetLike.coe_injective h
+  coe_injective' := SetLike.coe_injective.comp toSubmodule_injective
 
 instance : AddSubgroupClass (Subrep A) A.V where
   add_mem {w} := w.add_mem
   zero_mem {w} := w.zero_mem
   neg_mem {w} := w.neg_mem
 
-variable {A}
-
 /-- `w` interpreted as a `G`-rep. -/
 @[coe] noncomputable def toRep (w : Subrep A) : Rep k G :=
   .subrepresentation _ w.toSubmodule w.le_comap
@@ -43,12 +44,14 @@ noncomputable def quotient (w : Subrep A) : Rep k G :=
 @[simps!] noncomputable def mkQ (w : Subrep A) : A ⟶ w.quotient :=
   A.mkQ _ _
 
+instance : Min (Subrep A) where
+  min w₁ w₂ := ⟨w₁.toSubmodule ⊓ w₂.toSubmodule, fun g ↦ inf_le_inf (w₁.le_comap g) (w₂.le_comap g)⟩
+
+@[simp] lemma toSubmodule_inf (w₁ w₂ : Subrep A) :
+    (w₁ ⊓ w₂).toSubmodule = w₁.toSubmodule ⊓ w₂.toSubmodule := rfl
+
 -- todo: complete lattice, two adjoint functors (aka galois insertions)
-instance : SemilatticeInf (Subrep A) where
-  inf w₁ w₂ := ⟨w₁.toSubmodule ⊓ w₂.toSubmodule, fun g ↦ inf_le_inf (w₁.le_comap g) (w₂.le_comap g)⟩
-  inf_le_left w₁ _ := inf_le_left (a := w₁.toSubmodule)
-  inf_le_right w₁ _ := inf_le_right (a := w₁.toSubmodule)
-  le_inf w₁ _ _ := le_inf (a := w₁.toSubmodule)
+instance : SemilatticeInf (Subrep A) := toSubmodule_injective.semilatticeInf _ toSubmodule_inf
 
 instance : OrderTop (Subrep A) where
   top := ⟨⊤, fun _ _ _ ↦ trivial⟩
diff --git a/ClassFieldTheory/IsNonarchimedeanLocalField/Actions.lean b/ClassFieldTheory/IsNonarchimedeanLocalField/Actions.lean
index 8beba054..699ae064 100644
--- a/ClassFieldTheory/IsNonarchimedeanLocalField/Actions.lean
+++ b/ClassFieldTheory/IsNonarchimedeanLocalField/Actions.lean
@@ -1,6 +1,5 @@
 import ClassFieldTheory.IsNonarchimedeanLocalField.Basic
 import ClassFieldTheory.Mathlib.Topology.Algebra.Valued.ValuativeRel
-import Mathlib.FieldTheory.Galois.IsGaloisGroup
 
 /-! # Actions on local fields
 
diff --git a/ClassFieldTheory/IsNonarchimedeanLocalField/Basic.lean b/ClassFieldTheory/IsNonarchimedeanLocalField/Basic.lean
index c3ffd0e2..850796b0 100644
--- a/ClassFieldTheory/IsNonarchimedeanLocalField/Basic.lean
+++ b/ClassFieldTheory/IsNonarchimedeanLocalField/Basic.lean
@@ -1,19 +1,21 @@
 import ClassFieldTheory.LocalCFT.Continuity
+import ClassFieldTheory.Mathlib.Algebra.Order.Group.OrderIso
 import ClassFieldTheory.Mathlib.Algebra.Order.GroupWithZero.Canonical
-import ClassFieldTheory.Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
 import ClassFieldTheory.Mathlib.Data.Int.WithZero
 import ClassFieldTheory.Mathlib.RingTheory.DiscreteValuationRing.Basic
 import ClassFieldTheory.Mathlib.RingTheory.Localization.AtPrime.Basic
 import ClassFieldTheory.Mathlib.RingTheory.Unramified.Basic
 import ClassFieldTheory.Mathlib.RingTheory.Unramified.LocalRing
+import ClassFieldTheory.Mathlib.RingTheory.LocalRing.ResidueField.Basic
 import ClassFieldTheory.Mathlib.Topology.Algebra.Valued.ValuativeRel
+import ClassFieldTheory.Mathlib.Topology.Algebra.Valued.NormedValued
 import Mathlib.Analysis.Normed.Module.FiniteDimension
+import Mathlib.Analysis.Normed.Unbundled.SpectralNorm
 import Mathlib.FieldTheory.Finite.GaloisField
 import Mathlib.NumberTheory.LocalField.Basic
 import Mathlib.NumberTheory.Padics.ProperSpace
 import Mathlib.NumberTheory.Padics.ValuativeRel
 import Mathlib.NumberTheory.RamificationInertia.Basic
-import Mathlib.Order.CompletePartialOrder
 
 /-!
 # Non-Archimedean Local Fields
diff --git a/ClassFieldTheory/IsNonarchimedeanLocalField/UnramifiedCohomology.lean b/ClassFieldTheory/IsNonarchimedeanLocalField/UnramifiedCohomology.lean
index b9047350..6e1c198d 100644
--- a/ClassFieldTheory/IsNonarchimedeanLocalField/UnramifiedCohomology.lean
+++ b/ClassFieldTheory/IsNonarchimedeanLocalField/UnramifiedCohomology.lean
@@ -1,4 +1,5 @@
 import ClassFieldTheory.IsNonarchimedeanLocalField.ValuationExactSequence
+import Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
 
 /-! # Galois cohomology of unramified extensions of local fields
 
diff --git a/ClassFieldTheory/IsNonarchimedeanLocalField/Valuation.lean b/ClassFieldTheory/IsNonarchimedeanLocalField/Valuation.lean
index 5a3a2a12..ae1b02b0 100644
--- a/ClassFieldTheory/IsNonarchimedeanLocalField/Valuation.lean
+++ b/ClassFieldTheory/IsNonarchimedeanLocalField/Valuation.lean
@@ -3,18 +3,15 @@ Copyright (c) 2025 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard
 -/
-import ClassFieldTheory.Cohomology.Functors.Restriction
 import ClassFieldTheory.IsNonarchimedeanLocalField.Basic
 import ClassFieldTheory.Mathlib.Topology.Algebra.Valued.ValuativeRel
-import Mathlib.FieldTheory.Galois.IsGaloisGroup
-/-
 
+/-!
 # 1 → 𝒪[K]ˣ → Kˣ → ℤ → 0
 
 We construct the short exact sequence `0 → Additive 𝒪[K]ˣ → Additive (Kˣ) → ℤ → 0` in
 the following sense: we define the maps `kerV K` and `v K`, prove the first is
 injective, the second is surjective, and the pair is `Function.Exact`.
-
 -/
 
 namespace ValuativeRel
diff --git a/ClassFieldTheory/IsNonarchimedeanLocalField/ValuationExactSequence.lean b/ClassFieldTheory/IsNonarchimedeanLocalField/ValuationExactSequence.lean
index 7a00e74e..c70d50fe 100644
--- a/ClassFieldTheory/IsNonarchimedeanLocalField/ValuationExactSequence.lean
+++ b/ClassFieldTheory/IsNonarchimedeanLocalField/ValuationExactSequence.lean
@@ -1,21 +1,20 @@
 import ClassFieldTheory.Cohomology.Subrep.ShortExact
 import ClassFieldTheory.IsNonarchimedeanLocalField.Actions
 import ClassFieldTheory.IsNonarchimedeanLocalField.Valuation
-import ClassFieldTheory.Mathlib.Algebra.Group.Action.Units
-/-
+import Mathlib.FieldTheory.Galois.IsGaloisGroup
 
+/-!
 # 1 → 𝒪[L]ˣ → Lˣ → ℤ → 0 as G-module
 
 If L/K is a finite Galois extension of nonarch local fields, we construct the
 short exact sequence `0 → Additive 𝒪[K]ˣ → Additive (Kˣ) → ℤ → 0` in `Rep ℤ G`
-
 -/
 
 /-- The `G`-module `Mˣ` where `G` acts on `M` distributively. -/
 noncomputable abbrev Rep.units
     (G M : Type) [Monoid G] [CommMonoid M] [MulDistribMulAction G M] :
     Rep ℤ G :=
-  let : MulDistribMulAction G Mˣ := Units.mulDistribMulActionRight G M
+  let : MulDistribMulAction G Mˣ := Units.mulDistribMulActionRight
   Rep.ofMulDistribMulAction G Mˣ
 
 namespace IsNonarchimedeanLocalField
diff --git a/ClassFieldTheory/LocalCFT/Continuity.lean b/ClassFieldTheory/LocalCFT/Continuity.lean
index 74deeb4b..d607318b 100644
--- a/ClassFieldTheory/LocalCFT/Continuity.lean
+++ b/ClassFieldTheory/LocalCFT/Continuity.lean
@@ -1,9 +1,10 @@
-import Mathlib.Analysis.Normed.Unbundled.SpectralNorm
-import ClassFieldTheory.Mathlib.Topology.Algebra.Valued.NormedValued
+import ClassFieldTheory.Mathlib.RingTheory.Valuation.ValuativeRel
+import Mathlib.FieldTheory.Minpoly.Field
+import Mathlib.Topology.Algebra.Algebra
 import Mathlib.Topology.Algebra.Valued.ValuativeRel
 import Mathlib.Topology.Algebra.Valued.ValuedField
-/-!
 
+/-!
 # Main theorems
 
 * `continuous_algebraMap_of_density` Given a valuative algebraic extension of valuative topological
@@ -12,6 +13,7 @@ import Mathlib.Topology.Algebra.Valued.ValuedField
 * An instance of `ContinuousSMul K L` if `K,L` are valuative topological fields and `L/K`
   is a valuative algebraic extension.
 -/
+
 open ValuativeRel
 
 theorem Valuation.sum_eq_iSup {ι R Γ₀ : Type*} (f : ι → R) (s : Finset ι)
diff --git a/ClassFieldTheory/Mathlib/Algebra/Group/Action/Units.lean b/ClassFieldTheory/Mathlib/Algebra/Group/Action/Units.lean
deleted file mode 100644
index a90ae7ac..00000000
--- a/ClassFieldTheory/Mathlib/Algebra/Group/Action/Units.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-import Mathlib.Algebra.Group.Action.Units
-
-def Units.mulDistribMulActionRight (G M : Type*) [Monoid G] [Monoid M] [MulDistribMulAction G M] :
-    MulDistribMulAction G Mˣ where
-  smul g u := ⟨g • u, g • u⁻¹, by simp [← smul_mul', smul_one], by simp [← smul_mul', smul_one]⟩
-  one_smul u := Units.ext <| one_smul ..
-  mul_smul g₁ g₂ u := Units.ext <| mul_smul ..
-  smul_mul g₁ u₁ u₂ := Units.ext <| smul_mul' ..
-  smul_one g := Units.ext <| smul_one g
-
-attribute [local instance] Units.mulDistribMulActionRight
-
-@[simp] lemma Units.coe_smul {G M : Type*} [Monoid G] [Monoid M] [MulDistribMulAction G M]
-    {g : G} {u : Mˣ} : (g • u : Mˣ).val = g • u.val := rfl
diff --git a/ClassFieldTheory/Mathlib/Algebra/Group/Units/Basic.lean b/ClassFieldTheory/Mathlib/Algebra/Group/Units/Defs.lean
similarity index 88%
rename from ClassFieldTheory/Mathlib/Algebra/Group/Units/Basic.lean
rename to ClassFieldTheory/Mathlib/Algebra/Group/Units/Defs.lean
index c054a5d6..b5cd3011 100644
--- a/ClassFieldTheory/Mathlib/Algebra/Group/Units/Basic.lean
+++ b/ClassFieldTheory/Mathlib/Algebra/Group/Units/Defs.lean
@@ -1,4 +1,4 @@
-import Mathlib.Algebra.Group.Units.Basic
+import Mathlib.Algebra.Group.Units.Defs
 
 theorem IsUnit.of_mul {M : Type*} [Monoid M] {x y z : M}
     (hxy : IsUnit (x * y)) (hzx : IsUnit (z * x)) : IsUnit x :=
diff --git a/ClassFieldTheory/Mathlib/Algebra/Group/Units/Hom.lean b/ClassFieldTheory/Mathlib/Algebra/Group/Units/Hom.lean
index f0c79b98..662870e5 100644
--- a/ClassFieldTheory/Mathlib/Algebra/Group/Units/Hom.lean
+++ b/ClassFieldTheory/Mathlib/Algebra/Group/Units/Hom.lean
@@ -1,4 +1,4 @@
-import ClassFieldTheory.Mathlib.Algebra.Group.Units.Basic
+import ClassFieldTheory.Mathlib.Algebra.Group.Units.Defs
 import Mathlib.Algebra.Group.Units.Hom
 
 theorem isLocalHom_iff_one {R S F : Type*} [Monoid R] [Monoid S]
diff --git a/ClassFieldTheory/Mathlib/Algebra/Homology/ImageToKernel.lean b/ClassFieldTheory/Mathlib/Algebra/Homology/ImageToKernel.lean
deleted file mode 100644
index 02e2b408..00000000
--- a/ClassFieldTheory/Mathlib/Algebra/Homology/ImageToKernel.lean
+++ /dev/null
@@ -1,24 +0,0 @@
-import Mathlib.Algebra.Homology.ImageToKernel
-import Mathlib.CategoryTheory.Abelian.Basic
-
-open CategoryTheory CategoryTheory.Limits
-
-universe v u
-variable {ι : Type*} {V : Type u} [Category.{v} V]
-
-noncomputable section
-
-namespace CategoryTheory.Abelian
-variable [Abelian V] {A B C : V}
-
-@[ext]
-lemma coimage.ext (f : A ⟶ B) {g h : C ⟶ Abelian.coimage f}
-    (w : g ≫ Abelian.factorThruCoimage f = h ≫ Abelian.factorThruCoimage f) : g = h :=
-  (cancel_mono <| Abelian.factorThruCoimage f).1 w
-
-/-- Any short complex with maps `f : A ⟶ B` and `g : B ⟶ C` gives rise to a map from the cokernel
-of `f` to the kernel of `g`. -/
-def cokernelToCoimage (f : A ⟶ B) (g : B ⟶ C) (w : f ≫ g = 0) : cokernel f ⟶ Abelian.coimage g :=
-  cokernel.desc f (coimage.π g) <| by ext; simpa using w
-
-end CategoryTheory.Abelian
diff --git a/ClassFieldTheory/Mathlib/Algebra/Homology/ShortComplex/Exact.lean b/ClassFieldTheory/Mathlib/Algebra/Homology/ShortComplex/Exact.lean
index 1bb54743..4c60d99a 100644
--- a/ClassFieldTheory/Mathlib/Algebra/Homology/ShortComplex/Exact.lean
+++ b/ClassFieldTheory/Mathlib/Algebra/Homology/ShortComplex/Exact.lean
@@ -1,5 +1,4 @@
-import ClassFieldTheory.Mathlib.CategoryTheory.Abelian.Exact
-import Mathlib.CategoryTheory.Limits.Shapes.Kernels
+import Mathlib.Algebra.Homology.ShortComplex.Exact
 
 noncomputable section
 
diff --git a/ClassFieldTheory/Mathlib/Algebra/Module/NatInt.lean b/ClassFieldTheory/Mathlib/Algebra/Module/NatInt.lean
deleted file mode 100644
index c37735f3..00000000
--- a/ClassFieldTheory/Mathlib/Algebra/Module/NatInt.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-import Mathlib.Algebra.Module.NatInt
-import Mathlib.Data.Int.GCD
-
-lemma AddCommGroup.isTorsion_gcd_iff {M} (a b : ℕ) [AddCommGroup M] (x : M) :
-    (a.gcd b) • x = 0 ↔ a • x = 0 ∧ b • x = 0 := by
-  constructor
-  · intro h
-    obtain ⟨⟨n1, hn1⟩, ⟨n2, hn2⟩⟩ := Nat.gcd_dvd a b
-    exact ⟨hn1 ▸ mul_comm _ n1 ▸ mul_smul n1 _ x ▸ smul_zero (A := M) n1 ▸ congr(HSMul.hSMul n1 $h),
-      hn2 ▸ mul_comm _ n2 ▸ mul_smul n2 _ x ▸ smul_zero (A := M) n2 ▸ congr(HSMul.hSMul n2 $h)⟩
-  · rintro ⟨ha, hb⟩
-    rw [← natCast_zsmul, Nat.gcd_eq_gcd_ab, mul_comm (a : ℤ), mul_comm (b : ℤ)]
-    simp [add_smul, mul_smul, ha, hb]
-
-lemma AddCommGroup.isTorsion_gcd_coprime_iff {M} {a b : ℕ} [AddCommGroup M] (x : M)
-    (h : a.Coprime b) : x = 0 ↔ a • x = 0 ∧ b • x = 0 := by
-  simp [h, ← AddCommGroup.isTorsion_gcd_iff]
diff --git a/ClassFieldTheory/Mathlib/Algebra/Module/Submodule/Range.lean b/ClassFieldTheory/Mathlib/Algebra/Module/Submodule/Range.lean
deleted file mode 100644
index 66c87b79..00000000
--- a/ClassFieldTheory/Mathlib/Algebra/Module/Submodule/Range.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-import Mathlib.Algebra.Module.Submodule.Range
-
-/-!
-# TODO
-
-Rename `LinearMap.range_coe` to `LinearMap.range_coe`.
--/
-
-namespace Submodule
-variable {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M}
-
-@[simp] lemma submoduleOf_eq_top : p.submoduleOf q = ⊤ ↔ q ≤ p := by simp [submoduleOf]
-
-end Submodule
diff --git a/ClassFieldTheory/Mathlib/Algebra/Module/Torsion/Basic.lean b/ClassFieldTheory/Mathlib/Algebra/Module/Torsion/Basic.lean
index cb0ef121..0da68515 100644
--- a/ClassFieldTheory/Mathlib/Algebra/Module/Torsion/Basic.lean
+++ b/ClassFieldTheory/Mathlib/Algebra/Module/Torsion/Basic.lean
@@ -4,10 +4,10 @@ import Mathlib.Algebra.Module.Torsion.Basic
 def Module.IsTorsionBy.coprime_decompose {k m1 m2: ℕ} {R M : Type*} [CommRing R] [AddCommGroup M]
     [Module R M] (hk : k = m1 * m2) (hmm : m1.Coprime m2) (hA : Module.IsTorsionBy R M k):
     M ≃ₗ[R] Submodule.torsionBy R M m1 × Submodule.torsionBy R M m2 where
-  toFun m := ⟨⟨(m2 : R) • m, by simp [← MulAction.mul_smul, ← Nat.cast_mul, ← hk, hA]⟩,
-    ⟨(m1 : R) • m, by simp [← MulAction.mul_smul, mul_comm, ← Nat.cast_mul, ← hk, hA]⟩⟩
+  toFun m := ⟨⟨(m2 : R) • m, by simp [← mul_smul, ← Nat.cast_mul, ← hk, hA]⟩,
+    ⟨(m1 : R) • m, by simp [← mul_smul, mul_comm, ← Nat.cast_mul, ← hk, hA]⟩⟩
   map_add' := by simp
-  map_smul' := by simp [← MulAction.mul_smul, mul_comm]
+  map_smul' := by simp [← mul_smul, mul_comm]
   invFun := fun ⟨x1, x2⟩ ↦ (m1.gcdB m2 : R) • x1.1 + (m1.gcdA m2 : R) • x2.1
   left_inv x := by
     simp only [← smul_assoc, smul_eq_mul, ← add_smul]
diff --git a/ClassFieldTheory/Mathlib/Algebra/Order/GroupWithZero/Unbundled/OrderIso.lean b/ClassFieldTheory/Mathlib/Algebra/Order/Group/OrderIso.lean
similarity index 80%
rename from ClassFieldTheory/Mathlib/Algebra/Order/GroupWithZero/Unbundled/OrderIso.lean
rename to ClassFieldTheory/Mathlib/Algebra/Order/Group/OrderIso.lean
index fb33daf7..6609e70a 100644
--- a/ClassFieldTheory/Mathlib/Algebra/Order/GroupWithZero/Unbundled/OrderIso.lean
+++ b/ClassFieldTheory/Mathlib/Algebra/Order/Group/OrderIso.lean
@@ -1,4 +1,4 @@
-import Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso
+import Mathlib.Algebra.Order.Group.OrderIso
 
 @[simp] lemma map_lt_one_iff {F α β : Type*} [Preorder α] [Preorder β]
     [MulOneClass α] [MulOneClass β] [EquivLike F α β] [OrderIsoClass F α β] [MulEquivClass F α β]
diff --git a/ClassFieldTheory/Mathlib/CategoryTheory/Abelian/Exact.lean b/ClassFieldTheory/Mathlib/CategoryTheory/Abelian/Exact.lean
deleted file mode 100644
index aa9f055d..00000000
--- a/ClassFieldTheory/Mathlib/CategoryTheory/Abelian/Exact.lean
+++ /dev/null
@@ -1,31 +0,0 @@
-import ClassFieldTheory.Mathlib.Algebra.Homology.ImageToKernel
-import Mathlib.CategoryTheory.Abelian.Exact
-
-namespace CategoryTheory.ShortComplex
-universe v₁ u₁
-variable {C : Type u₁} [Category.{v₁} C] [Abelian C] {S : ShortComplex C}
-
-open Abelian
-
-lemma exact_iff_isIso_imageToKernel' : S.Exact ↔ IsIso (imageToKernel' S.f S.g S.zero) := by
-  simp only [S.exact_iff_epi_imageToKernel', isIso_iff_mono_and_epi, iff_and_self]
-  intro
-  apply CategoryTheory.Limits.kernel.lift_mono
-
-lemma Exact.isIso_imageToKernel (hS : S.Exact) : IsIso (imageToKernel S.f S.g S.zero) :=
-  S.exact_iff_isIso_imageToKernel.1 hS
-
-lemma Exact.isIso_imageToKernel' (hS : S.Exact) : IsIso (imageToKernel' S.f S.g S.zero) :=
-  S.exact_iff_isIso_imageToKernel'.1 hS
-
-proof_wanted exact_iff_isIso_cokernelToCoimage : S.Exact ↔ IsIso (cokernelToCoimage S.f S.g S.zero)
-
--- alias ⟨Exact.isIso_cokernelToCoimage, _⟩ := exact_iff_isIso_cokernelToCoimage
-
-lemma Exact.mono_cokernelDesc (hS : S.Exact) : Mono (Limits.cokernel.desc S.f S.g S.zero) :=
-  S.exact_iff_mono_cokernel_desc.1 hS
-
-lemma Exact.epi_kernelLift (hS : S.Exact) : Epi (Limits.kernel.lift S.g S.f S.zero) :=
-  S.exact_iff_epi_kernel_lift.1 hS
-
-end CategoryTheory.ShortComplex
diff --git a/ClassFieldTheory/Mathlib/CategoryTheory/Category/Cat.lean b/ClassFieldTheory/Mathlib/CategoryTheory/Category/Cat.lean
index ed8ec549..9e16de90 100644
--- a/ClassFieldTheory/Mathlib/CategoryTheory/Category/Cat.lean
+++ b/ClassFieldTheory/Mathlib/CategoryTheory/Category/Cat.lean
@@ -1,4 +1,3 @@
-import Mathlib.Data.Set.Function
 import Mathlib.CategoryTheory.Category.Cat
 
 open CategoryTheory
diff --git a/ClassFieldTheory/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean b/ClassFieldTheory/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
index f5e47606..31ace04c 100644
--- a/ClassFieldTheory/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
+++ b/ClassFieldTheory/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
@@ -15,7 +15,7 @@ theorem factors_maximalIdeal_pow (n : ℕ) :
     Multiset.replicate n (IsLocalRing.maximalIdeal R) :=
   UniqueFactorizationMonoid.factors_spec_of_subsingleton_units
     (Multiset.mem_replicate.not.mpr <| mt And.right not_a_field'.symm)
-    (by simp; rfl) (by simp [Multiset.mem_replicate])
+    (by simp) (by simp [Multiset.mem_replicate])
 
 theorem factors_maximalIdeal :
     UniqueFactorizationMonoid.factors (IsLocalRing.maximalIdeal R) = {IsLocalRing.maximalIdeal R} :=
diff --git a/ClassFieldTheory/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean b/ClassFieldTheory/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
index d4fe6a9f..8c9f47f7 100644
--- a/ClassFieldTheory/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
+++ b/ClassFieldTheory/Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
@@ -13,12 +13,4 @@ instance instAlgebra' : Algebra (IsLocalRing.ResidueField R) (IsLocalRing.Residu
   Ideal.Quotient.algebraQuotientOfLEComap <|
     ((IsLocalRing.local_hom_TFAE (algebraMap R S)).out 0 3).mp <| by infer_instance
 
-@[simp] lemma algebraMap_residue (x : R) :
-    (algebraMap (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S))
-      (IsLocalRing.residue R x) = IsLocalRing.residue S (algebraMap R S x) := rfl
-
-instance instIsScalarTower' :
-    IsScalarTower R (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) :=
-  .of_algebraMap_eq' rfl
-
 end IsLocalRing.ResidueField
diff --git a/ClassFieldTheory/Mathlib/RingTheory/Unramified/LocalRing.lean b/ClassFieldTheory/Mathlib/RingTheory/Unramified/LocalRing.lean
index 7ef12c96..7a5cc7e3 100644
--- a/ClassFieldTheory/Mathlib/RingTheory/Unramified/LocalRing.lean
+++ b/ClassFieldTheory/Mathlib/RingTheory/Unramified/LocalRing.lean
@@ -1,6 +1,5 @@
 import ClassFieldTheory.Mathlib.FieldTheory.Separable
 import ClassFieldTheory.Mathlib.RingTheory.Ideal.Maps
-import ClassFieldTheory.Mathlib.RingTheory.LocalRing.ResidueField.Basic
 import Mathlib.RingTheory.Unramified.LocalRing
 
 /-- Extra flexibility in the choice of:
@@ -24,8 +23,9 @@ lemma Algebra.isUnramifiedAt_iff_map_eq' {R : Type*} {S : Type*} [CommRing R] [C
       (IsLocalRing.ResidueField.mapEquiv <| Localization.algEquiv q.primeCompl S') ?_
     refine IsLocalization.ringHom_ext (nonZeroDivisors (R ⧸ p)) <| Ideal.Quotient.ringHom_ext <|
       RingHom.ext fun x ↦ ?_
-    simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, algebraMap_mk,
-      IsLocalRing.ResidueField.mapEquiv_apply, AlgEquiv.toRingEquiv_toRingHom]
+    simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
+      Ideal.algebraMap_quotient_residueField_mk, IsLocalRing.ResidueField.mapEquiv_apply,
+      AlgEquiv.toRingEquiv_toRingHom]
     rw [← IsScalarTower.algebraMap_apply,
       IsScalarTower.algebraMap_eq R (Localization.AtPrime p) p.ResidueField,
       RingHom.comp_apply, IsLocalRing.ResidueField.algebraMap_eq,
diff --git a/ClassFieldTheory/Mathlib/RingTheory/Valuation/ValuativeRel.lean b/ClassFieldTheory/Mathlib/RingTheory/Valuation/ValuativeRel.lean
index 91a207cf..f0c994c6 100644
--- a/ClassFieldTheory/Mathlib/RingTheory/Valuation/ValuativeRel.lean
+++ b/ClassFieldTheory/Mathlib/RingTheory/Valuation/ValuativeRel.lean
@@ -1,5 +1,5 @@
 import ClassFieldTheory.Mathlib.Algebra.Algebra.Subalgebra.Basic
-import ClassFieldTheory.Mathlib.RingTheory.Valuation.Basic
+import Mathlib.Algebra.Algebra.Subalgebra.Basic
 import Mathlib.RingTheory.Valuation.ValuativeRel.Basic
 
 namespace ValuativeRel
diff --git a/ClassFieldTheory/Mathlib/Topology/Algebra/Valued/NormedValued.lean b/ClassFieldTheory/Mathlib/Topology/Algebra/Valued/NormedValued.lean
index fe71e207..6b292944 100644
--- a/ClassFieldTheory/Mathlib/Topology/Algebra/Valued/NormedValued.lean
+++ b/ClassFieldTheory/Mathlib/Topology/Algebra/Valued/NormedValued.lean
@@ -1,3 +1,4 @@
+import ClassFieldTheory.Mathlib.RingTheory.Valuation.Basic
 import ClassFieldTheory.Mathlib.RingTheory.Valuation.ValuativeRel
 import Mathlib.Topology.Algebra.Valued.NormedValued
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 3c49c721..ab0c133b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d2965a4bb6fcdf827a079d7da0bcfb6d2780a259",
+   "rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "v4.26.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "74835c84b38e4070b8240a063c6417c767e551ae",
+   "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6e3bb4bf31f731ab28891fe229eb347ec7d5dad3",
+   "rev": "e9f31324f15ead11048b1443e62c5deaddd055d2",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2aaad968dd10a168b644b6a5afd4b92496af4710",
+   "rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.82",
+   "inputRev": "v0.0.83",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ea86e311a31a4dfa2abf3d7c0664b8c28499369e",
+   "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a31845b5557fd5e47d52b9e2977a1b0eff3c38c3",
+   "rev": "9312503909aa8e8bb392530145cc1677a6298574",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c0b0d08446817bd410548d9ea8ddcccf5d89f63f",
+   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9",
+   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0-rc2",
+   "inputRev": "v4.26.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "ClassFieldTheory",
diff --git a/lakefile.toml b/lakefile.toml
index 74ac3602..10dbb709 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -12,6 +12,7 @@ warn.sorry = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "v4.26.0"
 
 [[require]]
 name = "checkdecls"
diff --git a/lean-toolchain b/lean-toolchain
index 7035713c..2654c20b 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.26.0-rc2
\ No newline at end of file
+leanprover/lean4:v4.26.0
\ No newline at end of file