diff --git a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
index e22240be06..b3b2127eac 100644
--- a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
+++ b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
@@ -101,7 +101,7 @@ def mkZModAux {ι : Type} [DecidableEq ι] (n : ι → ℕ) (u : ∀ i, ZMod (n
 
 lemma mkZModAux_injective {ι : Type} [DecidableEq ι] {n : ι → ℕ} (hn : ∀ i, n i ≠ 0) :
     Injective (mkZModAux n) :=
-  AddChar.directSum_injective.comp fun f g h ↦ by simpa [Function.funext_iff, hn] using h
+  AddChar.directSum_injective.comp fun f g h ↦ by simpa [funext_iff, hn] using h
 
 /-- The circle-valued characters of a finite abelian group are the same as its complex-valued
 characters. -/
diff --git a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean
index bbc1199109..93525080d4 100644
--- a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean
+++ b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean
@@ -126,7 +126,7 @@ variable [OrderedSemiring β] {s : Finset α}
 @[simp] lemma indicate_nonneg : 0 ≤ 𝟭_[β] s := fun a ↦ by rw [indicate_apply]; split_ifs <;> simp
 
 @[simp] lemma indicate_pos [Nontrivial β] : 0 < 𝟭_[β] s ↔ s.Nonempty := by
-  simp [indicate_apply, Pi.lt_def, Function.funext_iff, lt_iff_le_and_ne, @eq_comm β 0,
+  simp [indicate_apply, Pi.lt_def, funext_iff, lt_iff_le_and_ne, @eq_comm β 0,
     Finset.Nonempty]
 
 protected alias ⟨_, Finset.Nonempty.indicate_pos⟩ := indicate_pos
@@ -166,7 +166,7 @@ variable [CharZero β] {a : α}
 lemma mu_apply_ne_zero : μ_[β] s a ≠ 0 ↔ a ∈ s := mu_apply_eq_zero.not_left
 
 @[simp] lemma mu_eq_zero : μ_[β] s = 0 ↔ s = ∅ := by
-  simp [Function.funext_iff, eq_empty_iff_forall_not_mem]
+  simp [funext_iff, eq_empty_iff_forall_not_mem]
 
 lemma mu_ne_zero : μ_[β] s ≠ 0 ↔ s.Nonempty := mu_eq_zero.not.trans nonempty_iff_ne_empty.symm
 
diff --git a/lake-manifest.json b/lake-manifest.json
index d9cf40a63c..142b4d053a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cc0bc876eeef0518ddc1c8d3bd6f48cc83e68901",
+   "rev": "c521f0185f4dd42b6aa4898010d5ba5357c57c9f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d951eef6bb39b3b78cbd1fba9c515c3770a9d20a",
+   "rev": "3f297f53816d8a85d03f8c08b3a7d475dfa51a6b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,