diff --git a/LeanSAT/AIG/Basic.lean b/LeanSAT/AIG/Basic.lean
index a7f6e1c0..4efb5ada 100644
--- a/LeanSAT/AIG/Basic.lean
+++ b/LeanSAT/AIG/Basic.lean
@@ -108,11 +108,12 @@ theorem Cache.get?_bounds {decls : Array (Decl α)} {idx : Nat} (c : Cache α de
     simp only [HashMap.getElem?_insert] at hfound
     match heq:decl == decl' with
     | true =>
-      simp only [heq, cond_true, Option.some.injEq] at hfound
+      simp only [beq_iff_eq] at heq
+      simp only [heq, beq_self_eq_true, ↓reduceIte, Option.some.injEq] at hfound
       simp
       omega
     | false =>
-      simp only [heq, cond_false] at hfound
+      simp only [BEq.symm_false heq, Bool.false_eq_true, ↓reduceIte] at hfound
       specialize ih hfound
       simp
       omega
@@ -143,11 +144,12 @@ theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α
     . simp only [HashMap.getElem?_insert] at hfound
       match heq:decl == decl' with
       | true =>
+        simp only [beq_iff_eq] at heq
         simp [heq] at hfound
         omega
       | false =>
         apply ih
-        simpa [heq] using hfound
+        simpa [BEq.symm_false heq] using hfound
     . next hbounds =>
       simp only [HashMap.getElem?_insert] at hfound
       match heq:decl == decl' with
@@ -157,7 +159,7 @@ theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α
       | false =>
         exfalso
         apply hbounds
-        simp only [heq, cond_false] at hfound
+        simp only [BEq.symm_false heq, cond_false] at hfound
         specialize ih _ hfound
         apply Array.lt_of_get
         assumption
diff --git a/LeanSAT/AIG/RelabelNat.lean b/LeanSAT/AIG/RelabelNat.lean
index 8cb5d685..34156a21 100644
--- a/LeanSAT/AIG/RelabelNat.lean
+++ b/LeanSAT/AIG/RelabelNat.lean
@@ -38,10 +38,11 @@ theorem Inv1.lt_of_get?_eq_some [EquivBEq α] {n m : Nat} (map : HashMap α Nat)
     rw [Std.HashMap.getElem?_insert]
     match hx : x == y with
     | true =>
-      simp [hx]
+      simp only [beq_iff_eq] at hx
+      simp only [hx, beq_self_eq_true, ↓reduceIte, Option.some.injEq]
       omega
     | false =>
-      simp [hx]
+      simp [BEq.symm_false hx]
       intro h
       specialize ih3 h
       omega
@@ -57,28 +58,31 @@ theorem Inv1.property [EquivBEq α] {n m : Nat} (x y : α) (map : HashMap α Nat
     rename_i z
     rw [HashMap.getElem?_insert] at hfound1
     rw [HashMap.getElem?_insert] at hfound2
-    match hx : x == z with
+    match hx : z == x with
     | false =>
-      rw [hx, cond_false] at hfound1
-      match hy : y == z with
+      simp only [beq_eq_false_iff_ne, ne_eq] at hx
+      simp only [beq_iff_eq, hx, ↓reduceIte] at hfound1
+      match hy : z == y with
       | false =>
-        rw [hy, cond_false] at hfound2
+        simp only [beq_eq_false_iff_ne, ne_eq] at hy
+        simp only [beq_iff_eq, hy, ↓reduceIte] at hfound2
         exact ih3 hfound1 hfound2
       | true =>
-        simp only [hy, cond_true, Option.some.injEq] at hfound2
+        simp only [hy, ↓reduceIte, Option.some.injEq] at hfound2
         have := Inv1.lt_of_get?_eq_some _ _ ih1 hfound1
         omega
     | true =>
-      rw [hx, cond_true] at hfound1
+      simp only [hx, ↓reduceIte, Option.some.injEq] at hfound1
       rcases hfound1 with ⟨rfl⟩
-      match hy : y == z with
+      match hy : z == y with
       | false =>
-        rw [hy, cond_false] at hfound2
+        simp only [beq_eq_false_iff_ne, ne_eq] at hy
+        simp only [beq_iff_eq, hy, ↓reduceIte] at hfound2
         have := Inv1.lt_of_get?_eq_some _ _ ih1 hfound2
         omega
       | true =>
         simp only [beq_iff_eq] at hx hy
-        simp [hx, hy]
+        simp only [←hx, hy]
 
 /--
 This invariant says that we have already visited and inserted all nodes up to a certain index.
@@ -112,22 +116,21 @@ theorem Inv2.property (decls : Array (Decl α)) (idx upper : Nat) (map : HashMap
   | empty => omega
   | newAtom ih1 ih2 ih3 ih4 ih5 =>
     next idx' _ a' _ =>
+    replace hidx : idx ≤ idx' := by omega
     rw [HashMap.getElem?_insert]
-    match heq2 : a == a' with
+    match heq2 : a' == a with
     | false =>
-      simp only [cond_false]
-      replace hidx : idx ≤ idx' := by omega
+      simp only [Bool.false_eq_true, ↓reduceIte]
       cases Nat.eq_or_lt_of_le hidx with
       | inl hidxeq =>
         subst hidxeq
-        exfalso
-        simp only [beq_eq_false_iff_ne, ne_eq] at heq2
-        apply heq2
-        apply Eq.symm
-        simpa [ih3] using heq
-      | inr hlt => apply ih5 <;> assumption
-    | true => simp [heq2]
+        simp_all only [beq_eq_false_iff_ne, Decl.atom.injEq]
+      | inr hlt =>
+        exact ih5 hlt heq
+    | true =>
+      exact Option.isSome_iff_exists.mp rfl
   | oldAtom ih1 ih2 ih3 ih4 ih5 =>
+    simp_all only [true_implies]
     next idx' _ _ _ =>
     replace hidx : idx ≤ idx' := by omega
     cases Nat.eq_or_lt_of_le hidx with
@@ -141,7 +144,7 @@ theorem Inv2.property (decls : Array (Decl α)) (idx upper : Nat) (map : HashMap
     next idx' _ _ =>
     replace hidx : idx ≤ idx' := by omega
     cases Nat.eq_or_lt_of_le hidx with
-    | inl hidxeq => simp [hidxeq, ih3] at heq
+    | inl hidxeq => simp only [hidxeq, ih3] at heq
     | inr hlt => apply ih4 <;> assumption
   | gate ih1 ih2 ih3 ih4 =>
     next idx' _ _ _ _ _ =>
@@ -384,4 +387,3 @@ theorem relabelNat_unsat_iff {entry : Entrypoint α} [Nonempty α]
 
 end Entrypoint
 end AIG
-
diff --git a/LeanSAT/CNF/Basic.lean b/LeanSAT/CNF/Basic.lean
index 64a93929..59d745e2 100644
--- a/LeanSAT/CNF/Basic.lean
+++ b/LeanSAT/CNF/Basic.lean
@@ -3,21 +3,10 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import LeanSAT.CNF.ForStd
 import LeanSAT.Sat
 
 open Sat
 
--- Lemmas from Mathlib, to move to Lean:
-@[simp] theorem exists_or_eq_left (y : α) (p : α → Prop) : ∃ x : α, x = y ∨ p x := ⟨y, .inl rfl⟩
-@[simp] theorem exists_or_eq_right (y : α) (p : α → Prop) : ∃ x : α, p x ∨ x = y := ⟨y, .inr rfl⟩
-@[simp] theorem exists_or_eq_left' (y : α) (p : α → Prop) : ∃ x : α, y = x ∨ p x := ⟨y, .inl rfl⟩
-@[simp] theorem exists_or_eq_right' (y : α) (p : α → Prop) : ∃ x : α, p x ∨ y = x := ⟨y, .inr rfl⟩
-
-@[simp] theorem List.isEmpty_false_iff_exists_mem (xs : List α) :
-    (List.isEmpty xs = false) ↔ ∃ x, x ∈ xs := by
-  cases xs <;> simp
-
 set_option linter.missingDocs false
 
 /--
diff --git a/LeanSAT/CNF/ForStd.lean b/LeanSAT/CNF/ForStd.lean
deleted file mode 100644
index 4fbe481e..00000000
--- a/LeanSAT/CNF/ForStd.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
--/
-
-@[simp] theorem List.all_append {x y : List α} : (x ++ y).all f = (x.all f && y.all f) := by
-  induction x with
-  | nil => rfl
-  | cons h t ih => simp_all [Bool.and_assoc]
diff --git a/lean-toolchain b/lean-toolchain
index f1a1c64a..d4c3ecf0 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1,2 +1,2 @@
-leanprover/lean4:nightly-2024-07-11
+leanprover/lean4:nightly-2024-07-25