diff --git a/LeanSAT/AIG/CNF.lean b/LeanSAT/AIG/CNF.lean
index 5911f949..57c54c36 100644
--- a/LeanSAT/AIG/CNF.lean
+++ b/LeanSAT/AIG/CNF.lean
@@ -55,7 +55,7 @@ theorem atomToCNF_eval :
     (atomToCNF output a).eval assign
       =
     (assign output == assign a) := by
-  simp only [atomToCNF, CNF.eval_succ, CNF.Clause.eval_succ, Bool.beq_true, Bool.beq_false,
+  simp only [atomToCNF, CNF.eval_succ, CNF.Clause.eval_succ, beq_true, beq_false,
     CNF.Clause.eval_nil, Bool.or_false, CNF.eval_nil, Bool.and_true]
   cases assign output <;> cases assign a <;> decide
 
diff --git a/LeanSAT/AIG/CachedLemmas.lean b/LeanSAT/AIG/CachedLemmas.lean
index 06e0f631..e592f4d0 100644
--- a/LeanSAT/AIG/CachedLemmas.lean
+++ b/LeanSAT/AIG/CachedLemmas.lean
@@ -298,7 +298,7 @@ theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput ai
       simp_all [denote_idx_const heq]
     . split
       . next hif =>
-        simp only [Bool.beq_false, Bool.and_eq_true, beq_iff_eq, Bool.not_eq_true'] at hif
+        simp only [beq_false, Bool.and_eq_true, beq_iff_eq, Bool.not_eq_true'] at hif
         rcases hif with ⟨⟨hifeq, hlinv⟩, hrinv⟩
         replace hifeq : input.lhs.ref = input.rhs.ref := by
           rcases input with ⟨⟨⟨_, _⟩, _⟩, ⟨⟨_, _⟩, _⟩⟩
diff --git a/LeanSAT/Reflect/Tactics/Normalize/Bool.lean b/LeanSAT/Reflect/Tactics/Normalize/Bool.lean
index 99ed685d..e855770a 100644
--- a/LeanSAT/Reflect/Tactics/Normalize/Bool.lean
+++ b/LeanSAT/Reflect/Tactics/Normalize/Bool.lean
@@ -19,11 +19,7 @@ attribute [bv_normalize] Bool.true_and
 attribute [bv_normalize] Bool.and_false
 attribute [bv_normalize] Bool.false_and
 attribute [bv_normalize] beq_self_eq_true'
-attribute [bv_normalize] Bool.not_beq_false
-attribute [bv_normalize] Bool.not_beq_true
-attribute [bv_normalize] Bool.beq_true
 attribute [bv_normalize] Bool.true_beq
-attribute [bv_normalize] Bool.beq_false
 attribute [bv_normalize] Bool.false_beq
 attribute [bv_normalize] Bool.beq_not_self
 attribute [bv_normalize] Bool.not_beq_self
diff --git a/LeanSAT/Reflect/Tactics/Normalize/Equal.lean b/LeanSAT/Reflect/Tactics/Normalize/Equal.lean
index 8dcd3849..25f6f785 100644
--- a/LeanSAT/Reflect/Tactics/Normalize/Equal.lean
+++ b/LeanSAT/Reflect/Tactics/Normalize/Equal.lean
@@ -8,9 +8,9 @@ import LeanSAT.Reflect.Tactics.Attr
 namespace BVDecide
 namespace Normalize
 
-attribute [bv_normalize] Bool.beq_true
+attribute [bv_normalize] beq_true
 attribute [bv_normalize] Bool.true_beq
-attribute [bv_normalize] Bool.beq_false
+attribute [bv_normalize] beq_false
 attribute [bv_normalize] Bool.false_beq
 attribute [bv_normalize] beq_self_eq_true
 attribute [bv_normalize] beq_self_eq_true'
diff --git a/lake-manifest.json b/lake-manifest.json
index 2299c4f3..ff9bdd38 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries.git",
    "type": "git",
    "subDir": null,
-   "rev": "b24f8d9e82cf133812e74df1adb6d049de74eeb0",
+   "scope": "",
+   "rev": "4e1d17623329b6a46bd6007f031d28119f59d0d1",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lean-toolchain b/lean-toolchain
index 571e4126..86a76398 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1,2 +1,2 @@
-leanprover/lean4:nightly-2024-06-28
+leanprover/lean4:nightly-2024-07-03