diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 7140dda628..d0c57cf75a 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -33,7 +33,6 @@ import LeanAPAP.Mathlib.Analysis.NormedSpace.Ray
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Data.Complex.Basic
 import LeanAPAP.Mathlib.Data.Complex.Order
-import LeanAPAP.Mathlib.Data.Finset.Basic
 import LeanAPAP.Mathlib.Data.Finset.Card
 import LeanAPAP.Mathlib.Data.Finset.Image
 import LeanAPAP.Mathlib.Data.Finset.Pi
@@ -41,7 +40,6 @@ import LeanAPAP.Mathlib.Data.Finset.Pointwise
 import LeanAPAP.Mathlib.Data.Finset.Powerset
 import LeanAPAP.Mathlib.Data.Fintype.Basic
 import LeanAPAP.Mathlib.Data.Fintype.BigOperators
-import LeanAPAP.Mathlib.Data.Fintype.Card
 import LeanAPAP.Mathlib.Data.Fintype.Lattice
 import LeanAPAP.Mathlib.Data.Fintype.Pi
 import LeanAPAP.Mathlib.Data.FunLike.Basic
diff --git a/LeanAPAP/Mathlib/Data/Finset/Basic.lean b/LeanAPAP/Mathlib/Data/Finset/Basic.lean
deleted file mode 100644
index 1c95f44889..0000000000
--- a/LeanAPAP/Mathlib/Data/Finset/Basic.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-import Mathlib.Data.Finset.Basic
-
-namespace Finset
-variable {α : Type*} {s : Finset α} {a : α}
-
-attribute [pp_dot] Finset.Nonempty
-
-@[norm_cast]
-lemma coe_subset_singleton : (s : Set α) ⊆ {a} ↔ s ⊆ {a} := by rw [←coe_subset, coe_singleton]
-
-@[norm_cast]
-lemma singleton_subset_coe : {a} ⊆ (s : Set α) ↔ {a} ⊆ s := by rw [←coe_subset, coe_singleton]
-
-end Finset
diff --git a/LeanAPAP/Mathlib/Data/Fintype/Basic.lean b/LeanAPAP/Mathlib/Data/Fintype/Basic.lean
index 471a262310..b08a6ac55e 100644
--- a/LeanAPAP/Mathlib/Data/Fintype/Basic.lean
+++ b/LeanAPAP/Mathlib/Data/Fintype/Basic.lean
@@ -7,11 +7,6 @@ namespace Finset
 @[simp]
 lemma filter_mem_univ (s : Finset α) : univ.filter (· ∈ s) = s := by simp [filter_mem_eq_inter]
 
--- @[simp] --TODO: Unsimp `finset.univ_unique`
-lemma singleton_eq_univ [Subsingleton α] (a : α) : ({a} : Finset α) = univ := by
-  ext b; simp [Subsingleton.elim a b]
+-- TODO: Unsimp `Finset.univ_unique`
 
 end Finset
-
-instance {s : Set α} [DecidablePred (· ∈ s)] : Decidable s.Subsingleton :=
-  decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, a = b) Iff.rfl
diff --git a/LeanAPAP/Mathlib/Data/Fintype/Card.lean b/LeanAPAP/Mathlib/Data/Fintype/Card.lean
deleted file mode 100644
index 7ad442cbe3..0000000000
--- a/LeanAPAP/Mathlib/Data/Fintype/Card.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-import Mathlib.Data.Fintype.Card
-
-namespace Fintype
-
-@[simp] lemma card_multiplicative (α : Type*) [Fintype α] : card (Multiplicative α) = card α :=
-  Finset.card_map _
-
-@[simp] lemma card_additive (α : Type*) [Fintype α] : card (Additive α) = card α :=
-  Finset.card_map _
-
-end Fintype
diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean
index 189d96a773..ed932605ef 100644
--- a/LeanAPAP/Prereqs/AddChar/Basic.lean
+++ b/LeanAPAP/Prereqs/AddChar/Basic.lean
@@ -293,7 +293,7 @@ noncomputable instance instFintype [Finite G] : Fintype (AddChar G R) :=
 
 @[simp] lemma card_addChar_le [Fintype G] : card (AddChar G R) ≤ card G := by
   simpa only [FiniteDimensional.finrank_fintype_fun_eq_card] using
-    FiniteDimensional.fintype_card_le_finrank_of_linearIndependent (AddChar.linearIndependent G R)
+    (AddChar.linearIndependent G R).fintype_card_le_finrank
 
 end IsROrC
 
diff --git a/LeanAPAP/Prereqs/Dissociation.lean b/LeanAPAP/Prereqs/Dissociation.lean
index 3178d9b27b..575074fb01 100644
--- a/LeanAPAP/Prereqs/Dissociation.lean
+++ b/LeanAPAP/Prereqs/Dissociation.lean
@@ -5,7 +5,6 @@ import Mathlib.Data.Fintype.Pi
 import Mathlib.Data.Set.Pointwise.Basic
 import LeanAPAP.Mathlib.Algebra.BigOperators.Basic
 import LeanAPAP.Mathlib.Algebra.GroupPower.Basic
-import LeanAPAP.Mathlib.Data.Finset.Basic
 import LeanAPAP.Mathlib.Data.Finset.Powerset
 import LeanAPAP.Mathlib.Data.Fintype.Basic
 import LeanAPAP.Mathlib.Data.Set.Function
diff --git a/lake-manifest.json b/lake-manifest.json
index 5541b9cbda..cddf9df2f9 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -49,47 +49,11 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "be0b59d276020004e21109a79cab71f259755349",
+   "rev": "7a302eb97c8a48fef146f33f55eb00fc7a5541e3",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/xubaiw/CMark.lean",
-   "type": "git",
-   "subDir": null,
-   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
-   "name": "CMark",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargonix/LeanInk",
-   "type": "git",
-   "subDir": null,
-   "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
-   "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": "86d5c219a9ad7aa686c9e0e704af030e203c63a1",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "LeanAPAP",
  "lakeDir": ".lake"}