diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean
index ea0527ada8..44522f5611 100644
--- a/LeanCamCombi.lean
+++ b/LeanCamCombi.lean
@@ -51,12 +51,10 @@ import LeanCamCombi.Mathlib.Data.Nat.Factors
 import LeanCamCombi.Mathlib.Data.Nat.Lattice
 import LeanCamCombi.Mathlib.Data.Nat.Order.Lemmas
 import LeanCamCombi.Mathlib.Data.Nat.Squarefree
-import LeanCamCombi.Mathlib.Data.Set.Equitable
 import LeanCamCombi.Mathlib.Data.Set.Finite
 import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.Data.Set.Prod
-import LeanCamCombi.Mathlib.Data.Sym.Sym2
 import LeanCamCombi.Mathlib.Data.ZMod.Defs
 import LeanCamCombi.Mathlib.Data.ZMod.Quotient
 import LeanCamCombi.Mathlib.GroupTheory.GroupAction.Defs
@@ -70,7 +68,6 @@ import LeanCamCombi.Mathlib.GroupTheory.Subgroup.Stabilizer
 import LeanCamCombi.Mathlib.GroupTheory.Subgroup.ZPowers
 import LeanCamCombi.Mathlib.GroupTheory.Submonoid.Membership
 import LeanCamCombi.Mathlib.GroupTheory.Submonoid.Operations
-import LeanCamCombi.Mathlib.GroupTheory.Torsion
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.Independent
 import LeanCamCombi.Mathlib.Logic.Basic
@@ -80,11 +77,9 @@ import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace
 import LeanCamCombi.Mathlib.NumberTheory.MaricaSchoenheim
 import LeanCamCombi.Mathlib.Order.Category.BoolAlg
 import LeanCamCombi.Mathlib.Order.ConditionallyCompleteLattice.Basic
-import LeanCamCombi.Mathlib.Order.Disjoint
 import LeanCamCombi.Mathlib.Order.Hom.Lattice
 import LeanCamCombi.Mathlib.Order.Hom.Set
 import LeanCamCombi.Mathlib.Order.LocallyFinite
-import LeanCamCombi.Mathlib.Order.Partition.Equipartition
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.Sublattice
 import LeanCamCombi.Mathlib.Order.SupClosed
diff --git a/LeanCamCombi/Kneser/CauchyDavenport.lean b/LeanCamCombi/Kneser/CauchyDavenport.lean
index 0421112d69..4c9aea71f5 100644
--- a/LeanCamCombi/Kneser/CauchyDavenport.lean
+++ b/LeanCamCombi/Kneser/CauchyDavenport.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yaël Dillies, Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
-import Mathlib.Combinatorics.Additive.Etransform
+import Mathlib.Combinatorics.Additive.ETransform
 import LeanCamCombi.Mathlib.Algebra.Group.Defs
 import LeanCamCombi.Mathlib.GroupTheory.MinOrder
 import LeanCamCombi.Kneser.Mathlib
@@ -138,8 +138,8 @@ lemma Finset.min_le_card_mul (hs : s.Nonempty) (ht : t.Nonempty) :
       ⟨inter_subset_left _ _, fun h =>
         hsg <|
           eq_of_superset_of_card_ge (h.trans <| inter_subset_right _ _) (card_smul_finset _ _).le⟩
-  replace aux1 := card_mono (mulEtransformLeft.fst_mul_snd_subset g (s, t))
-  replace aux2 := card_mono (mulEtransformRight.fst_mul_snd_subset g (s, t))
+  replace aux1 := card_mono (mulETransformLeft.fst_mul_snd_subset g (s, t))
+  replace aux2 := card_mono (mulETransformRight.fst_mul_snd_subset g (s, t))
   -- If the left translate of `t` by `g⁻¹` is disjoint from `t`, then we're easily done.
   obtain hgt | hgt := disjoint_or_nonempty_inter t (g⁻¹ • t)
   · rw [← card_smul_finset g⁻¹ t]
@@ -149,7 +149,7 @@ lemma Finset.min_le_card_mul (hs : s.Nonempty) (ht : t.Nonempty) :
   -- Else, we're done by induction on either `(s', t')` or `(s'', t'')` depending on whether
   -- `|s| + |t| ≤ |s'| + |t'|` or `|s| + |t| < |s''| + |t''|`. One of those two inequalities must
   -- hold since `2 * (|s| + |t|) = |s'| + |t'| + |s''| + |t''|`.
-  obtain hstg | hstg := le_or_lt_of_add_le_add (MulEtransform.card g (s, t)).ge
+  obtain hstg | hstg := le_or_lt_of_add_le_add (MulETransform.card g (s, t)).ge
   · exact
       (ih _ _ hgs (hgt.mono inter_subset_union) <| devosMulRel_of_le_of_le aux1 hstg hsg).imp
         (WithTop.coe_le_coe.2 aux1).trans' fun h => hstg.trans <| h.trans <| add_le_add_right aux1 _
diff --git a/LeanCamCombi/Kneser/Impact.lean b/LeanCamCombi/Kneser/Impact.lean
index 3d8076ac6f..533b2259d0 100644
--- a/LeanCamCombi/Kneser/Impact.lean
+++ b/LeanCamCombi/Kneser/Impact.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Combinatorics.Additive.Etransform
+import Mathlib.Combinatorics.Additive.ETransform
 import LeanCamCombi.Mathlib.Data.Finset.Pointwise
 import LeanCamCombi.Mathlib.Data.Set.Finite
 import LeanCamCombi.Mathlib.Data.Nat.Lattice
diff --git a/LeanCamCombi/Kneser/KneserRuzsa.lean b/LeanCamCombi/Kneser/KneserRuzsa.lean
index 308955bafc..456cc8fc05 100644
--- a/LeanCamCombi/Kneser/KneserRuzsa.lean
+++ b/LeanCamCombi/Kneser/KneserRuzsa.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Mantas Bakšys, Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mantas Bakšys, Yaël Dillies
 -/
-import Mathlib.Combinatorics.Additive.Etransform
+import Mathlib.Combinatorics.Additive.ETransform
 import LeanCamCombi.Mathlib.Algebra.Order.Ring.Canonical
 import LeanCamCombi.Mathlib.Data.Finset.Basic
 import LeanCamCombi.Mathlib.Data.Finset.Card
@@ -158,8 +158,8 @@ lemma le_card_mul_add_card_mulStab_mul (hs : s.Nonempty) (ht : t.Nonempty) :
   refine'
     Nat.find_min' _
       ⟨_, _, mem_inter.2 ⟨hbt' _, _⟩, (hs' _).trans <| subset_union_left _ _,
-        (mulDysonEtransform.subset _ (s' b, t' b)).trans <| hst' _,
-        (mulDysonEtransform.card _ _).trans <| hstcard _, rfl⟩
+        (mulDysonETransform.subset _ (s' b, t' b)).trans <| hst' _,
+        (mulDysonETransform.card _ _).trans <| hstcard _, rfl⟩
   rwa [mem_inv_smul_finset_iff, smul_eq_mul, inv_mul_cancel_right]
 
 /-- **Kneser's multiplication lemma**: A lower bound on the size of `s * t` in terms of its
diff --git a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean
index 6e630d6315..c80c51f9b3 100644
--- a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean
+++ b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean
@@ -5,7 +5,6 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.BigOperators.Basic
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
-import LeanCamCombi.Mathlib.Data.Sym.Sym2
 
 /-!
 # Containment of graphs
@@ -208,13 +207,8 @@ noncomputable def labelledCopyCount (G : SimpleGraph α) (H : SimpleGraph β) :
 
 @[simp] lemma labelledCopyCount_of_isEmpty [IsEmpty α] (G : SimpleGraph α) (H : SimpleGraph β) :
     G.labelledCopyCount H = 1 := by
-  classical
-  have : Unique {f : G →g H // Injective f} :=
-    { default := ⟨default, isEmptyElim⟩
-      uniq := fun _ ↦ Subsingleton.elim _ _ }
-  rw [labelledCopyCount]
-  sorry
-  -- exact @Fintype.card_unique _ (this) _
+  convert Fintype.card_unique
+  exact { default := ⟨default, isEmptyElim⟩, uniq := fun _ ↦ Subsingleton.elim _ _ }
 
 @[simp] lemma labelledCopyCount_eq_zero : G.labelledCopyCount H = 0 ↔ ¬ G ⊑ H := by
   simp [labelledCopyCount, IsContained, Fintype.card_eq_zero_iff]
@@ -225,9 +219,9 @@ noncomputable def labelledCopyCount (G : SimpleGraph α) (H : SimpleGraph β) :
 /-- There's more labelled copies of `H` of-`G` than unlabelled ones. -/
 lemma copyCount_le_labelledCopyCount : G.copyCount H ≤ G.labelledCopyCount H := by
   rw [copyCount, ←Fintype.card_coe]
-  refine' Fintype.card_le_of_injective (fun H' ↦
+  refine Fintype.card_le_of_injective (fun H' ↦
     ⟨H'.val.hom.comp (mem_filter.1 H'.2).2.some.toHom,
-      Subtype.coe_injective.comp (mem_filter.1 H'.2).2.some.injective⟩) _
+      Subtype.coe_injective.comp (mem_filter.1 H'.2).2.some.injective⟩) ?_
   sorry
 
 end LabelledCopyCount
diff --git a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
index fd0b420752..7eb0a83dd5 100644
--- a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
+++ b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
@@ -12,9 +12,6 @@ namespace SimpleGraph
 
 namespace Subgraph
 
--- TODO: Replace `coe_Adj`
-alias coe_adj := coe_Adj
-
 instance (G : SimpleGraph V) (H : Subgraph G) [DecidableRel H.Adj] : DecidableRel H.coe.Adj :=
   fun a b ↦ ‹DecidableRel H.Adj› _ _
 
diff --git a/LeanCamCombi/Mathlib/Data/Nat/Factorization/Basic.lean b/LeanCamCombi/Mathlib/Data/Nat/Factorization/Basic.lean
index 63601273fc..be29e1ad38 100644
--- a/LeanCamCombi/Mathlib/Data/Nat/Factorization/Basic.lean
+++ b/LeanCamCombi/Mathlib/Data/Nat/Factorization/Basic.lean
@@ -1,21 +1 @@
-import Mathlib.Data.Nat.Factorization.Basic
-import LeanCamCombi.Mathlib.Data.Nat.Factors
-
-namespace Nat
-variable {n p : ℕ}
-
--- TODO: Rename `Nat.factors` to `Nat.primeFactorsList`
 -- TODO: Protect `Nat.Prime.factorization`
-
-def primeFactors (n : ℕ) : Finset ℕ := n.factors.toFinset
-
-@[simp] lemma support_factorization' (n : ℕ) : (factorization n).support = n.primeFactors := rfl
-@[simp] lemma toFinset_factors (n : ℕ) : n.factors.toFinset = n.primeFactors := rfl
-
-@[simp] lemma mem_primeFactors : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
-  simp_rw [←toFinset_factors, List.mem_toFinset, mem_factors']
-
-lemma mem_primeFactors_of_ne_zero (hn : n ≠ 0) : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n := by
-  simp [hn]
-
-end Nat
diff --git a/LeanCamCombi/Mathlib/Data/Nat/Factors.lean b/LeanCamCombi/Mathlib/Data/Nat/Factors.lean
index af6113e87f..1e17c4e2c9 100644
--- a/LeanCamCombi/Mathlib/Data/Nat/Factors.lean
+++ b/LeanCamCombi/Mathlib/Data/Nat/Factors.lean
@@ -1,9 +1 @@
-import Mathlib.Data.Nat.Factors
-
-namespace Nat
-variable {p n : ℕ}
-
-@[simp] lemma mem_factors' : p ∈ n.factors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
-  cases n <;> simp [mem_factors, *]
-
-end Nat
+-- TODO: Rename `Nat.factors` to `Nat.primeFactorsList`
diff --git a/LeanCamCombi/Mathlib/Data/Nat/Squarefree.lean b/LeanCamCombi/Mathlib/Data/Nat/Squarefree.lean
index 2849eb6c15..d1851a91c9 100644
--- a/LeanCamCombi/Mathlib/Data/Nat/Squarefree.lean
+++ b/LeanCamCombi/Mathlib/Data/Nat/Squarefree.lean
@@ -1,5 +1,4 @@
 import Mathlib.Data.Nat.Squarefree
-import LeanCamCombi.Mathlib.Data.Nat.Factorization.Basic
 import LeanCamCombi.Mathlib.Data.Nat.Order.Lemmas
 
 open Finset
diff --git a/LeanCamCombi/Mathlib/Data/Set/Equitable.lean b/LeanCamCombi/Mathlib/Data/Set/Equitable.lean
deleted file mode 100644
index 74d2a7602a..0000000000
--- a/LeanCamCombi/Mathlib/Data/Set/Equitable.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-import Mathlib.Data.Set.Equitable
-
-namespace Set
-variable {α β : Type*} [LinearOrder β] [Add β] [One β] {s : Set α} {f : α → β}
-
-@[simp]
-lemma not_equitableOn : ¬s.EquitableOn f ↔ ∃ a ∈ s, ∃ b ∈ s, f b + 1 < f a := by
-  simp [EquitableOn]; aesop
-
-end Set
diff --git a/LeanCamCombi/Mathlib/Data/Sym/Sym2.lean b/LeanCamCombi/Mathlib/Data/Sym/Sym2.lean
deleted file mode 100644
index 9d5a04aaf6..0000000000
--- a/LeanCamCombi/Mathlib/Data/Sym/Sym2.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-import Mathlib.Data.Sym.Sym2
-
-open Function
-
-variable {α β : Type*} {e : Sym2 α} {f : α → β}
-
-namespace Sym2
-
-protected lemma IsDiag.map : e.IsDiag → (e.map f).IsDiag := Sym2.ind (fun _ _ ↦ congr_arg f) e
-
-lemma isDiag_map (hf : Injective f) : (e.map f).IsDiag ↔ e.IsDiag :=
-  Sym2.ind (fun _ _ ↦ hf.eq_iff) e
-
-end Sym2
diff --git a/LeanCamCombi/Mathlib/GroupTheory/Torsion.lean b/LeanCamCombi/Mathlib/GroupTheory/Torsion.lean
deleted file mode 100644
index ac43dfc182..0000000000
--- a/LeanCamCombi/Mathlib/GroupTheory/Torsion.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-import Mathlib.GroupTheory.Torsion
-
-namespace Monoid
-variable {α : Type*} [Monoid α]
-
-@[to_additive (attr := simp)]
-lemma isTorsionFree_of_subsingleton [Subsingleton α] : IsTorsionFree α :=
-  fun _a ha _ => ha <| Subsingleton.elim _ _
-
-end Monoid
diff --git a/LeanCamCombi/Mathlib/Order/Disjoint.lean b/LeanCamCombi/Mathlib/Order/Disjoint.lean
deleted file mode 100644
index e23a21532a..0000000000
--- a/LeanCamCombi/Mathlib/Order/Disjoint.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-import Mathlib.Order.Disjoint
-
-section Lattice
-variable {α : Type*} [Lattice α] [BoundedOrder α] {a b : α}
-
-lemma isCompl_comm : IsCompl a b ↔ IsCompl b a := ⟨IsCompl.symm, IsCompl.symm⟩
-
-end Lattice
diff --git a/LeanCamCombi/Mathlib/Order/Partition/Equipartition.lean b/LeanCamCombi/Mathlib/Order/Partition/Equipartition.lean
deleted file mode 100644
index 7de6ec71c2..0000000000
--- a/LeanCamCombi/Mathlib/Order/Partition/Equipartition.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-import Mathlib.Order.Partition.Equipartition
-import LeanCamCombi.Mathlib.Data.Set.Equitable
-
-namespace Finpartition
-variable {α : Type*} [DecidableEq α] {s : Finset α} {P : Finpartition s}
-
-@[simp]
-lemma not_isEquipartition :
-    ¬P.IsEquipartition ↔ ∃ a ∈ P.parts, ∃ b ∈ P.parts, Finset.card b + 1 < Finset.card a :=
-  Set.not_equitableOn
-
-end Finpartition
diff --git a/LeanCamCombi/VanDenBergKesten.lean b/LeanCamCombi/VanDenBergKesten.lean
index 27ddbef4fc..ae55eedd84 100644
--- a/LeanCamCombi/VanDenBergKesten.lean
+++ b/LeanCamCombi/VanDenBergKesten.lean
@@ -7,7 +7,6 @@ import Mathlib.Data.Finset.Sort
 import Mathlib.Data.Finset.Sups
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Order.UpperLower.Basic
-import LeanCamCombi.Mathlib.Order.Disjoint
 
 /-!
 # Set family certificates
diff --git a/lake-manifest.json b/lake-manifest.json
index 8999ff07f8..8c18567fa0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "874ff0574c19582d3d275d1c803846549cd53dce",
+    "rev": "9e03d9ced7ba4d2bf95f9ed7da0e3a3ffbc81d9e",
     "opts": {},
     "name": "mathlib",
     "inputRev?": null,
@@ -12,7 +12,7 @@
   {"git":
    {"url": "https://github.com/leanprover/doc-gen4",
     "subDir?": null,
-    "rev": "8bccb92b531248af1b6692d65486e8640c8bcd10",
+    "rev": "e859e2f777521f82050b8f28e0205491a4ead0f5",
     "opts": {},
     "name": "«doc-gen4»",
     "inputRev?": "main",
@@ -20,7 +20,7 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "9bfbd2a12ee9cf2e159a8a6b4d1ef6c149728f66",
+    "rev": "fb07d160aff0e8bdf403a78a5167fc7acf9c8227",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
@@ -28,11 +28,19 @@
   {"git":
    {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "396201245bf244f9d78e9007a02dd1c388193d27",
+    "rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39",
     "opts": {},
     "name": "Qq",
     "inputRev?": "master",
     "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/aesop",
+    "subDir?": null,
+    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
@@ -49,14 +57,6 @@
     "name": "proofwidgets",
     "inputRev?": "v0.0.21",
     "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/aesop",
-    "subDir?": null,
-    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
-    "inherited": true}},
   {"git":
    {"url": "https://github.com/xubaiw/CMark.lean",
     "subDir?": null,
@@ -68,9 +68,9 @@
   {"git":
    {"url": "https://github.com/fgdorais/lean4-unicode-basic",
     "subDir?": null,
-    "rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32",
+    "rev": "4ecf4f1f98d14d03a9e84fa1c082630fa69df88b",
     "opts": {},
-    "name": "«lean4-unicode-basic»",
+    "name": "UnicodeBasic",
     "inputRev?": "main",
     "inherited": true}},
   {"git":