diff --git a/Algorithm/Algebra/BigOperators/DFinsupp'.lean b/Algorithm/Algebra/BigOperators/DFinsupp'.lean
index d0ed13e..03e7ef0 100644
--- a/Algorithm/Algebra/BigOperators/DFinsupp'.lean
+++ b/Algorithm/Algebra/BigOperators/DFinsupp'.lean
@@ -152,13 +152,15 @@ variable {R S : Type*}
 variable [∀ (i) (x : β i), Decidable (x ≠ d i)]
 
 @[to_additive (attr := simp, norm_cast)]
-theorem coe_dfinsupp'_prod [Monoid R] [CommMonoid S] (f : Π₀' i, [β i, d i]) (g : ∀ i, β i → R →* S) :
+theorem coe_dfinsupp'_prod [Monoid R] [CommMonoid S]
+    (f : Π₀' i, [β i, d i]) (g : ∀ i, β i → R →* S) :
     ⇑(f.prod g) = f.prod fun a b => ⇑(g a b) :=
   coe_finset_prod _ _
 
 @[to_additive]
-theorem dfinsupp'_prod_apply [Monoid R] [CommMonoid S] (f : Π₀' i, [β i, d i]) (g : ∀ i, β i → R →* S)
-    (r : R) : (f.prod g) r = f.prod fun a b => (g a b) r :=
+theorem dfinsupp'_prod_apply [Monoid R] [CommMonoid S]
+    (f : Π₀' i, [β i, d i]) (g : ∀ i, β i → R →* S) (r : R) :
+    (f.prod g) r = f.prod fun a b => (g a b) r :=
   finset_prod_apply _ _ _
 
 end MonoidHom
diff --git a/Algorithm/Data/Classes/IndexedMinHeap.lean b/Algorithm/Data/Classes/IndexedMinHeap.lean
index 82e0556..d933f03 100644
--- a/Algorithm/Data/Classes/IndexedMinHeap.lean
+++ b/Algorithm/Data/Classes/IndexedMinHeap.lean
@@ -6,6 +6,7 @@ Authors: Yuyang Zhao
 import Algorithm.Data.Classes.AssocArray
 import Algorithm.Data.Classes.MinHeap
 import Algorithm.Data.Classes.ToList
+import Mathlib.Data.Finset.Lattice.Fold
 import Mathlib.Data.Prod.Lex
 
 class IndexedMinHeap (C : Type*) [Inhabited C] (ι : outParam Type*)
diff --git a/Algorithm/Data/Classes/MinHeap.lean b/Algorithm/Data/Classes/MinHeap.lean
index e0bdef4..7958e2b 100644
--- a/Algorithm/Data/Classes/MinHeap.lean
+++ b/Algorithm/Data/Classes/MinHeap.lean
@@ -77,8 +77,8 @@ lemma coe_eq_head?_of_forall_le (p : α → Prop) (hc : ¬isEmpty c) (pc : p (he
     (x : α) (hx : x ∈ c) (h : ∀ y ∈ c, p y → y ≠ x → x < y) :
     x = head? c := by
   contrapose! h
-  exact ⟨head c (ToMultiset.not_isEmpty_of_mem hx), MinHeap.head_mem _ _, pc, by intro h'; simp [← h'] at h,
-    fun h' ↦ (h'.trans_le (head_le c _ hx)).ne rfl⟩
+  exact ⟨head c (ToMultiset.not_isEmpty_of_mem hx), MinHeap.head_mem _ _, pc,
+    by intro h'; simp [← h'] at h, fun h' ↦ (h'.trans_le (head_le c _ hx)).ne rfl⟩
 
 lemma eq_head_of_forall_le (p : α → Prop) (hc : ¬isEmpty c) (pc : p (head c hc))
     (x : α) (hx : x ∈ c) (h : ∀ y ∈ c, p y → y ≠ x → x < y) :
diff --git a/Algorithm/Data/DFinsupp'/Basic.lean b/Algorithm/Data/DFinsupp'/Basic.lean
index 0a61ca2..ab00348 100644
--- a/Algorithm/Data/DFinsupp'/Basic.lean
+++ b/Algorithm/Data/DFinsupp'/Basic.lean
@@ -245,13 +245,14 @@ def comapDomain' (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h'
         (s.prop (h x)).imp_left fun hx => Multiset.mem_map.mpr ⟨_, hx, hh' _⟩⟩
 
 @[simp]
-theorem comapDomain'_apply (h : κ → ι) {h' : ι → κ}
-    (hh' : Function.LeftInverse h' h) (f : Π₀' i, [β i, d i]) (k : κ) : comapDomain' h hh' f k = f (h k) :=
+theorem comapDomain'_apply (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h)
+    (f : Π₀' i, [β i, d i]) (k : κ) :
+    comapDomain' h hh' f k = f (h k) :=
   rfl
 
 @[simp]
-theorem comapDomain'_default (h : κ → ι) {h' : ι → κ}
-    (hh' : Function.LeftInverse h' h) : comapDomain' h hh' (default : Π₀' i, [β i, d i]) = default := by
+theorem comapDomain'_default (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) :
+    comapDomain' h hh' (default : Π₀' i, [β i, d i]) = default := by
   ext
   rw [default_apply, comapDomain'_apply, default_apply]
 
diff --git a/Algorithm/Data/DFinsupp'/Defs.lean b/Algorithm/Data/DFinsupp'/Defs.lean
index 4efabe8..596db2b 100644
--- a/Algorithm/Data/DFinsupp'/Defs.lean
+++ b/Algorithm/Data/DFinsupp'/Defs.lean
@@ -4,7 +4,7 @@ Copyright (c) 2024 Yuyang Zhao. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuyang Zhao
 -/
-import Mathlib.Data.Set.Finite
+import Mathlib.Data.Set.Finite.Basic
 
 /-!
 Modified from `Mathlib.Data.DFinsupp.Basic`
@@ -276,9 +276,8 @@ theorem single_eq_of_ne {i i' b} (h : i ≠ i') : single d i b i' = d i' := by
 theorem single_injective {i} : Function.Injective (single d i) := fun _ _ H =>
   Function.update_injective _ i <| DFunLike.coe_injective.eq_iff.mpr H
 
-/-- Like `Finsupp'.single_eq_single_iff`, but with a `HEq` due to dependent types -/
 theorem single_eq_single_iff (i j : ι) (xi : β i) (xj : β j) :
-    DFinsupp'.single d i xi = DFinsupp'.single d j xj ↔ i = j ∧ HEq xi xj ∨ xi = d i ∧ xj = d j := by
+    single d i xi = single d j xj ↔ i = j ∧ HEq xi xj ∨ xi = d i ∧ xj = d j := by
   constructor
   · intro h
     by_cases hij : i = j
@@ -314,14 +313,14 @@ theorem single_eq_of_sigma_eq {i j} {xi : β i} {xj : β j} (h : (⟨i, xi⟩ :
 
 @[simp]
 theorem equivFunOnFintype_single [Fintype ι] (i : ι) (m : β i) :
-    (@DFinsupp'.equivFunOnFintype ι β _ _) (DFinsupp'.single d i m) = Function.update d i m := by
+    DFinsupp'.equivFunOnFintype (DFinsupp'.single d i m) = Function.update d i m := by
   ext x
   dsimp [Pi.single, Function.update]
   simp [DFinsupp'.single_eq_functionUpdate, @eq_comm _ i]
 
 @[simp]
 theorem equivFunOnFintype_symm_single [Fintype ι] (i : ι) (m : β i) :
-    (@DFinsupp'.equivFunOnFintype ι β _ _).symm (Function.update d i m) = DFinsupp'.single d i m := by
+    DFinsupp'.equivFunOnFintype.symm (Function.update d i m) = DFinsupp'.single d i m := by
   ext i'
   simp only [← single_eq_functionUpdate, equivFunOnFintype_symm_coe]
 
@@ -605,9 +604,9 @@ theorem support_erase (i : ι) (f : Π₀' i, [β i, d i]) :
     (f.erase i).support = f.support.erase i := by
   ext j
   by_cases h1 : j = i
-  simp only [h1, mem_support_toFun, erase_apply, ite_true, ne_eq, not_true, not_not,
+  · simp only [h1, mem_support_toFun, erase_apply, ite_true, ne_eq, not_true, not_not,
     Finset.mem_erase, false_and]
-  by_cases h2 : f j ≠ d j <;> simp at h2 <;> simp [h1, h2]
+  · by_cases h2 : f j ≠ d j <;> simp at h2 <;> simp [h1, h2]
 
 theorem support_update_ne (f : Π₀' i, [β i, d i]) (i : ι) {b : β i} (h : b ≠ d i) :
     support (f.update i b) = insert i f.support := by
diff --git a/Algorithm/Data/DFinsupp'/Fintype.lean b/Algorithm/Data/DFinsupp'/Fintype.lean
index e27c640..80ba9f3 100644
--- a/Algorithm/Data/DFinsupp'/Fintype.lean
+++ b/Algorithm/Data/DFinsupp'/Fintype.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuyang Zhao
 -/
 import Algorithm.Data.DFinsupp'.Defs
-import Mathlib.Data.Fintype.Basic
+import Mathlib.Data.Fintype.Pi
 
 /-!
 Modified from `Mathlib.Data.DFinsupp.Basic`
diff --git a/Algorithm/Data/Graph/IsDFSForest.lean b/Algorithm/Data/Graph/IsDFSForest.lean
index 0db3e87..cd17b19 100644
--- a/Algorithm/Data/Graph/IsDFSForest.lean
+++ b/Algorithm/Data/Graph/IsDFSForest.lean
@@ -73,7 +73,8 @@ lemma sound (hf : g..IsDFSForest i o f) :
     rintro w (rfl | hw | hw)
     · exact ⟨w, .inl rfl, .refl _ _⟩
     · obtain ⟨r, hr, hrw⟩ := ihc w hw
-      exact ⟨_, .inl rfl, (mem_succSet_singleton_iff.mp (roots_subset_succ hr)).to_reachable.trans hrw⟩
+      exact ⟨_, .inl rfl,
+        (mem_succSet_singleton_iff.mp (roots_subset_succ hr)).to_reachable.trans hrw⟩
     · obtain ⟨r, hr, hrw⟩ := ihs w hw
       exact ⟨r, .inr hr, hrw⟩
 
diff --git a/Algorithm/Data/PairingHeap.lean b/Algorithm/Data/PairingHeap.lean
index 07f566a..a8f6a13 100644
--- a/Algorithm/Data/PairingHeap.lean
+++ b/Algorithm/Data/PairingHeap.lean
@@ -246,3 +246,5 @@ instance [Preorder α] [IsTotal α (· ≤ ·)] [DecidableRel (α := α) (· ≤
       change _ = Multiset.erase _ a
       simp
   deleteMin_def x := by match x with | ⟨.nil, _⟩ | ⟨.node _ _ _, _⟩ => rfl
+
+end Batteries.PairingHeap
diff --git a/Algorithm/Graph/DFS.lean b/Algorithm/Graph/DFS.lean
index e56df72..9adb2b1 100644
--- a/Algorithm/Graph/DFS.lean
+++ b/Algorithm/Graph/DFS.lean
@@ -323,3 +323,5 @@ lemma dfsTR_spec (g : G)
   trans g..traversal {v | (g..dfsTR vs (default : BoolArray))[v]} ∅
   · convert g..dfsTR_spec' vs (default : BoolArray) <;> aesop
   · simp
+
+end AdjListClass
diff --git a/Algorithm/Graph/Dijkstra.lean b/Algorithm/Graph/Dijkstra.lean
index 23f8eab..7fe1c13 100644
--- a/Algorithm/Graph/Dijkstra.lean
+++ b/Algorithm/Graph/Dijkstra.lean
@@ -444,7 +444,7 @@ lemma dijkstraStep_fst_getElem' (g : G) (c : Info → CostType)
       decreaseKeysD_getElem, toMultiset_list, ← Multiset.filterMap_coe, coe_toList, ne_eq]
   split_ifs with h
   · simp? [Function.update_apply] says
-      simp only [Function.update_apply, min_eq_top, ite_eq_left_iff, Multiset.inf_eq_top,
+      simp only [Function.update_apply, inf_eq_top_iff, ite_eq_left_iff, Multiset.inf_eq_top,
         Multiset.mem_filterMap, mem_toMultiset, Option.ite_none_right_eq_some, Option.some.injEq,
         Prod.exists, Prod.mk.injEq, exists_eq_right_right, exists_eq_right, forall_exists_index,
         and_imp]
@@ -506,7 +506,7 @@ lemma dijkstraStep_fst_getElem_eq_top (g : G) (c : Info → CostType)
   dsimp
   rw [dijkstraStep_fst_getElem (spec₁ := spec₁)]
   simp? [hMinIdx, - not_or] says
-    simp only [ne_eq, ite_eq_left_iff, min_eq_top, Finset.inf_eq_top_iff, Finset.mem_univ,
+    simp only [ne_eq, ite_eq_left_iff, inf_eq_top_iff, Finset.inf_eq_top_iff, Finset.mem_univ,
       WithTop.add_eq_top, hMinIdx, WithTop.coe_ne_top, or_self, imp_false, not_true_eq_false,
       succSet_singleton, Set.mem_setOf_eq]
   rw [← or_iff_not_imp_right]
@@ -682,7 +682,8 @@ def dijkstra (g : G) (c : Info → CostType)
   (go init default spec_init).val.2
 where
   go (heap : DistHeap) (res : DistArray) (spec : dijkstraStep.Spec g c init heap res) :
-      { hr : DistHeap × DistArray // dijkstraStep.Spec g c init hr.1 hr.2 ∧ hr.1[minIdx hr.1] = ⊤ } :=
+      { hr : DistHeap × DistArray //
+        dijkstraStep.Spec g c init hr.1 hr.2 ∧ hr.1[minIdx hr.1] = ⊤ } :=
     if hh : heap[minIdx heap] = ⊤ then
       ⟨(heap, res), spec, hh⟩
     else
@@ -691,7 +692,8 @@ where
         letI : DecidableEq V := by classical infer_instance
         simp only [dijkstraStep_snd_getElem_eq_top, ne_eq, Set.coe_setOf, Set.mem_setOf_eq, hr]
         exact Fintype.card_lt_of_injective_of_not_mem (fun ⟨v, hv⟩ ↦ ⟨v, hv.2⟩)
-          (by intro ⟨v, hv⟩ ⟨w, hw⟩; simp) (b := ⟨minIdx heap, (spec.1 _).resolve_left hh⟩) (by simp)
+          (by intro ⟨v, hv⟩ ⟨w, hw⟩; simp)
+          (b := ⟨minIdx heap, (spec.1 _).resolve_left hh⟩) (by simp)
       go hr.1 hr.2 (g..dijkstraStep_spec c init heap res spec hh)
 termination_by Fintype.card {v : V | res[v] = ⊤}
   spec_init : dijkstraStep.Spec g c init init default := by
diff --git a/lake-manifest.json b/lake-manifest.json
index 7e060d2..666cb06 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "401646a0c432318bd679969e8870c9331bf7e37b",
+   "rev": "c933dd9b00271d869e22b802a015092d1e8e454a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "93bcfd774f89d3874903cab06abfbf69f327cbd9",
+   "rev": "de91b59101763419997026c35a41432ac8691f15",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ac7b989cbf99169509433124ae484318e953d201",
+   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4c285ebed4a964dcac8e9cf809143ca52f8d93f9",
+   "rev": "698148763dd29cf98dd2c56b8a44ac8e825461ae",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
diff --git a/lakefile.lean b/lakefile.lean
index 707eb56..827aaff 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,17 +1,29 @@
 import Lake
 open Lake DSL
 
-package algorithm where
-  leanOptions := #[
+abbrev algorithmOnlyLinters : Array LeanOption := #[
+  ⟨`linter.hashCommand, true⟩,
+  ⟨`linter.oldObtain, true,⟩,
+  ⟨`linter.refine, true⟩,
+  ⟨`linter.style.cdot, true⟩,
+  ⟨`linter.style.dollarSyntax, true⟩,
+  ⟨`linter.style.header, true⟩,
+  ⟨`linter.style.lambdaSyntax, true⟩,
+  ⟨`linter.style.longLine, true⟩,
+  ⟨`linter.style.longFile, .ofNat 1500⟩,
+  -- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
+  ⟨`linter.style.missingEnd, true⟩,
+  ⟨`linter.style.multiGoal, true⟩,
+  ⟨`linter.style.setOption, true⟩
+]
+
+abbrev algorithmLeanOptions := #[
     ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
-    ⟨`pp.proofs.withType, false⟩,
-    ⟨`autoImplicit, false⟩,
-    ⟨`relaxedAutoImplicit, false⟩
-  ]
-  moreLinkArgs := #[
-    "-L./.lake/build/lib",
-    "-lstdc++"
-  ]
+    ⟨`autoImplicit, false⟩
+  ] ++ -- options that are used in `lake build`
+    algorithmOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name }
+
+package algorithm where
 
 require "leanprover-community" / "mathlib" @ git "master"
 require "leanprover" / "doc-gen4" @ git "main"
@@ -22,7 +34,13 @@ lean_lib Mutable where
 
 @[default_target]
 lean_lib Algorithm where
-  roots := #[`Algorithm]
+  leanOptions := algorithmLeanOptions
+  -- Mathlib also enforces these linter options, which are not active by default.
+  moreServerOptions := algorithmOnlyLinters
+  moreLinkArgs := #[
+    "-L./.lake/build/lib",
+    "-lstdc++"
+  ]
 
 target ffi.o pkg : System.FilePath := do
   let oFile := pkg.buildDir / "cpp" / "ffi.o"
diff --git a/lean-toolchain b/lean-toolchain
index 0bef727..57a4710 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4:v4.14.0-rc2