diff --git a/Cslib/Computability/Languages/MyhillNerode.lean b/Cslib/Computability/Languages/MyhillNerode.lean
index 87a3a61a7..fc9220a34 100644
--- a/Cslib/Computability/Languages/MyhillNerode.lean
+++ b/Cslib/Computability/Languages/MyhillNerode.lean
@@ -74,7 +74,7 @@ variable {l : Language α}
 theorem nerodeCongruenceDA_language_eq (l : Language α) :
     language (l.NerodeCongruenceDA) = l := by
   ext x
-  simp only [NerodeCongruenceDA, language, Acceptor.Accepts, congr_mtr_eq, Set.mem_image]
+  simp only [NerodeCongruenceDA, language, Acceptor.Accepts, congr_mtr_eq]
   constructor
   · rintro ⟨y, hy, heq⟩
     have h1 := Quotient.eq.mp heq []
diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean
index 8b5fbb45c..566db21c9 100644
--- a/Cslib/Computability/Languages/OmegaLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaLanguage.lean
@@ -278,7 +278,8 @@ theorem hmul_bot : l * (⊥ : ωLanguage α) = ⊥ := by
 
 @[simp, scoped grind =]
 theorem one_hmul : (1 : Language α) * p = p := by
-  simp [hmul_def, Language.one_def, Language.toSet]
+  simp [hmul_def]
+  simp [Language.one_def, Language.toSet]
 
 theorem hmul_sup : l * (p ⊔ q) = l * p ⊔ l * q := by
   ext : 1
@@ -458,8 +459,10 @@ theorem omegaLim_zero : (0 : Language α)↗ω = ⊥ := by
   simp [omegaLim_def, bot_def]
 
 @[simp, scoped grind =]
-theorem map_id (p : ωLanguage α) : map id p = p :=
-  by simp [map]
+theorem map_id (p : ωLanguage α) : map id p = p := by
+  unfold map
+  change { toSet := id '' p.toSet } = p
+  simp
 
 @[scoped grind =]
 theorem map_map (g : β → γ) (f : α → β) (p : ωLanguage α) : map g (map f p) = map (g ∘ f) p := by
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
index 79c4ae530..29f379d5a 100644
--- a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
+++ b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
@@ -318,8 +318,7 @@ private theorem map_toCompCfg_right_step :
   cases cfg2 with
   | mk state BiTape =>
     cases state with
-    | none =>
-      simp only [step, toCompCfg_right, Option.map_none, compComputer]
+    | none => rfl
     | some q =>
       generalize hM : tm2.tr q BiTape.head = result
       obtain ⟨⟨wr, dir⟩, nextState⟩ := result
diff --git a/Cslib/Computability/URM/StandardForm.lean b/Cslib/Computability/URM/StandardForm.lean
index f1abcf344..51a288b6b 100644
--- a/Cslib/Computability/URM/StandardForm.lean
+++ b/Cslib/Computability/URM/StandardForm.lean
@@ -217,8 +217,9 @@ theorem eval_toStandardForm {p : Program} {inputs : List ℕ} :
   · simp only [Part.map_Dom]
     exact Halts.toStandardForm_iff
   · intro hp hq
-    simp only [Part.map_get, Function.comp_apply, Regs.output,
-               evalState_toStandardForm_regs hp hq]
+    have := Part.map_get (fun x : State => x.regs.output) (evalState p inputs) hp
+    have := Part.map_get (fun x : State => x.regs.output) (evalState p.toStandardForm inputs) hq
+    simp_all [Function.comp_def, evalState_toStandardForm_regs hp hq]
 
 /-- A program is equivalent to its standard form. -/
 theorem toStandardForm_equiv (p : Program) : p.toStandardForm ≈ p :=
diff --git a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean
index 9aa98ab04..1148ef3ef 100644
--- a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean
+++ b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean
@@ -109,11 +109,8 @@ private lemma Proof.expand_onlyAtomicAxioms_dual {a : Proposition Atom} :
   induction a with
   | one => simp +contextual [dual, expand, onlyAtomicAxioms]
   | bot =>
-    intro h
-    rw [←h]
-    congr 1
-    · grind
-    · simp [dual, expand, rwConclusion, Logic.InferenceSystem.rwConclusion]
+    #adaptation_note /-- see https://github.com/leanprover/lean4/pull/13484/ -/
+    grind [expand, dual.eq_def]
   | _ => grind [Proposition.expand, Proposition.dual_inj]
 
 open Proposition Proof in
diff --git a/CslibTests/DFA.lean b/CslibTests/DFA.lean
index 09ccd69d7..c48ee1c1b 100644
--- a/CslibTests/DFA.lean
+++ b/CslibTests/DFA.lean
@@ -15,12 +15,12 @@ open Cslib.Automata
 inductive Floor where
 | one
 | two
-deriving DecidableEq, Fintype
+deriving DecidableEq
 
 inductive Direction where
 | up
 | down
-deriving DecidableEq, Fintype
+deriving DecidableEq
 
 def elevator : DA Floor Direction where
   tr
diff --git a/lake-manifest.json b/lake-manifest.json
index 4e0d2864a..ffd2fd7da 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ce52fd18b8ecea2a6268f6973e3ca54f687a01c1",
+   "rev": "de3a9cf33016bbb6d15880d7680643f7ca2d25ba",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2026-07-03",
+   "inputRev": "nightly-testing-2026-07-07",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -45,10 +45,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "85bb7e7637e84a7d9803be7d954579fdae42c64b",
+   "rev": "b312c33e8df8a2c453e9557a29b17ed24f31d1c4",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.100",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "347e896e4df17535bd50d051f147b07095649d0c",
+   "rev": "e00cb0b633f502b579f676782d5516f1f508173a",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8fb9f43f0c722dffce4a00b38adf12a5043a4936",
+   "rev": "44bdf79647d66b4d5c21af02d3e3b9658d60bec8",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lakefile.toml b/lakefile.toml
index 05e5b8e9b..786589103 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4-nightly-testing"
-rev = "nightly-testing-2026-07-03"
+rev = "nightly-testing-2026-07-07"
 
 [[lean_lib]]
 name = "Cslib"
diff --git a/lean-toolchain b/lean-toolchain
index 4f88fc749..3afd63df9 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-07-03
+leanprover/lean4:nightly-2026-07-07