diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
index 52f43a4..9b43e03 100644
--- a/Lampe/Lampe.lean
+++ b/Lampe/Lampe.lean
@@ -74,7 +74,7 @@ nr_def simple_if<>(x : Field, y : Field) -> Field {
 example {p Γ x y} : STHoare p Γ ⟦⟧ (simple_if.fn.body _ h![] |>.body h![x, y])
     fun v => v = y := by
   simp only [simple_if]
-  steps <;> tauto
+  steps <;> try tauto
   . sl
   . sl
     simp_all
@@ -91,10 +91,10 @@ example {p Γ x y} : STHoare p Γ ⟦⟧ (simple_if_else.fn.body _ h![] |>.body
     fun v => v = x := by
   simp only [simple_if_else]
   steps
-  . simp only [decide_True, exists_const]
+  . simp only [decide_true, exists_const]
     sl
     contradiction
-  . simp_all [decide_True, exists_const]
+  . simp_all [decide_true, exists_const]
 
 nr_def simple_lambda<>(x : Field, y : Field) -> Field {
   let add = |a : Field, b : Field| -> Field { #fAdd(a, b) : Field };
@@ -155,7 +155,7 @@ example {p} {arg : Tp.denote p Tp.field} :
     sl
     tauto
     try_impls_all [] simpleTraitEnv
-    all_goals tauto
+    all_goals try tauto
     simp only
     steps
     simp_all only [exists_const, SLP.true_star]
@@ -255,7 +255,7 @@ example : STHoare p ⟨[(add_two_fields.name, add_two_fields.fn)], []⟩ ⟦⟧
   . sl
     tauto
   on_goal 3 => exact add_two_fields.fn
-  all_goals tauto
+  all_goals try tauto
   on_goal 3 => exact fun v => v = 3
   . simp only [add_two_fields]
     steps
@@ -296,7 +296,7 @@ nr_def simple_array<>() -> Field {
 example : STHoare p Γ ⟦⟧ (simple_array.fn.body _ h![] |>.body h![])
     fun (v : Tp.denote p .field) => v = 2 := by
   simp only [simple_array, Expr.mkArray]
-  steps <;> tauto
+  steps <;> try tauto
   aesop
 
 nr_def tuple_lens<>() -> Field {
@@ -380,12 +380,12 @@ example : STHoare p ⟨[(simple_func.name, simple_func.fn), (call.name, call.fn)
   steps
   . apply STHoare.callDecl_intro
     sl
-    all_goals tauto
+    all_goals try tauto
     simp only [call]
     steps
     . apply STHoare.callDecl_intro
       sl
-      all_goals tauto
+      all_goals try tauto
       simp only [simple_func]
       steps
       on_goal 2 => exact fun v => v = 10
diff --git a/Lampe/Lampe/Builtin/Array.lean b/Lampe/Lampe/Builtin/Array.lean
index 828d36b..ba0e50e 100644
--- a/Lampe/Lampe/Builtin/Array.lean
+++ b/Lampe/Lampe/Builtin/Array.lean
@@ -12,9 +12,9 @@ lemma Fin.n_is_non_zero {h : Fin n} : n ≠ 0 := by
   contradiction
   simp
 
-lemma Mathlib.Vector.get_after_erase {idx : Nat} {vec : Mathlib.Vector α n} {h₁ h₂ h₃} :
-  (Mathlib.Vector.eraseIdx ⟨idx, h₁⟩ vec).get ⟨idx, h₂⟩ = Mathlib.Vector.get vec ⟨idx + 1, h₃⟩ := by
-  unfold Mathlib.Vector.get Mathlib.Vector.eraseIdx
+lemma List.Vector.get_after_erase {idx : Nat} {vec : List.Vector α n} {h₁ h₂ h₃} :
+  (List.Vector.eraseIdx ⟨idx, h₁⟩ vec).get ⟨idx, h₂⟩ = List.Vector.get vec ⟨idx + 1, h₃⟩ := by
+  unfold List.Vector.get List.Vector.eraseIdx
   cases vec
   simp_all only [Fin.cast_mk, List.get_eq_getElem]
   rename List _ => l
@@ -41,12 +41,12 @@ lemma Mathlib.Vector.get_after_erase {idx : Nat} {vec : Mathlib.Vector α n} {h
       . aesop
 
 @[simp]
-lemma Mathlib.Vector.get_after_insert {idx : Nat} {vec : Mathlib.Vector α n} {h} :
-  (Mathlib.Vector.insertNth v ⟨idx, h⟩ vec).get ⟨idx, h⟩ = v := by
-  unfold Mathlib.Vector.insertNth Mathlib.Vector.get
+lemma List.Vector.get_after_insert {idx : Nat} {vec : List.Vector α n} {h} :
+  (List.Vector.insertIdx v ⟨idx, h⟩ vec).get ⟨idx, h⟩ = v := by
+  unfold List.Vector.insertIdx List.Vector.get
   cases vec
   simp_all only [List.get_eq_getElem, Fin.coe_cast]
-  apply List.get_insertNth_self
+  apply List.get_insertIdx_self
   subst_vars
   linarith
 
@@ -54,7 +54,7 @@ namespace Lampe.Builtin
 
 @[reducible]
 def replaceArray' (arr : Tp.denote p (.array tp n)) (idx : Fin n.toNat) (v : Tp.denote p tp) : Tp.denote p (.array tp n) :=
-  let arr' := (arr.insertNth v ⟨idx.val + 1, by aesop⟩)
+  let arr' := (arr.insertIdx v ⟨idx.val + 1, by aesop⟩)
   arr'.eraseIdx ⟨idx.val, by cases idx; tauto⟩
 
 example {p} : (replaceArray' (p := p) (n := ⟨3, by aesop⟩) (tp := .bool) ⟨[false, false, false], (by rfl)⟩ ⟨1, by tauto⟩ true).get ⟨1, by tauto⟩ = true := by rfl
@@ -65,10 +65,10 @@ theorem index_replaced_arr {n : U 32} {idx : Fin n.toNat} {arr} :
   unfold replaceArray'
   cases em (n.toNat > 0)
   . simp_all only [gt_iff_lt, eq_mp_eq_cast]
-    generalize h₁ : (Mathlib.Vector.insertNth _ _ _) = arr₁
+    generalize h₁ : (List.Vector.insertIdx _ _ _) = arr₁
     cases idx
-    rw [Mathlib.Vector.get_after_erase, ←h₁]
-    apply Mathlib.Vector.get_after_insert
+    rw [List.Vector.get_after_erase, ←h₁]
+    apply List.Vector.get_after_insert
   . simp_all only [gt_iff_lt, not_lt, nonpos_iff_eq_zero, lt_self_iff_false, dite_false]
     rename_i h
     rw [h] at idx
diff --git a/Lampe/Lampe/Builtin/Basic.lean b/Lampe/Lampe/Builtin/Basic.lean
index d6a42c5..d5121ad 100644
--- a/Lampe/Lampe/Builtin/Basic.lean
+++ b/Lampe/Lampe/Builtin/Basic.lean
@@ -37,7 +37,7 @@ lemma HList.toList_length_is_n (h_same : tps = List.replicate n tp) :
   rfl
 
 @[reducible]
-def HList.toVec (l : HList rep tps) (h_same : tps = List.replicate n tp) : Mathlib.Vector (rep tp) n :=
+def HList.toVec (l : HList rep tps) (h_same : tps = List.replicate n tp) : List.Vector (rep tp) n :=
   ⟨HList.toList l h_same, by apply HList.toList_length_is_n⟩
 
 @[reducible]
diff --git a/Lampe/Lampe/Builtin/BigInt.lean b/Lampe/Lampe/Builtin/BigInt.lean
index f9cd520..55c66b9 100644
--- a/Lampe/Lampe/Builtin/BigInt.lean
+++ b/Lampe/Lampe/Builtin/BigInt.lean
@@ -72,7 +72,7 @@ Converts a list `l` to a vector of size `n`s.
 - If `n < l.length`, then the output is truncated from the end.
 - If `n > l.length`, then the higher indices are populated with `zero`.
 -/
-def listToVec (l : List α) (zero : α) : Mathlib.Vector α n :=
+def listToVec (l : List α) (zero : α) : List.Vector α n :=
   ⟨l.takeD n zero, List.takeD_length _ _ _⟩
 
 /--
diff --git a/Lampe/Lampe/Builtin/Helpers.lean b/Lampe/Lampe/Builtin/Helpers.lean
index 5f0a110..bc499b0 100644
--- a/Lampe/Lampe/Builtin/Helpers.lean
+++ b/Lampe/Lampe/Builtin/Helpers.lean
@@ -6,6 +6,7 @@ namespace Lampe
 def extList (lst : List α) (len : Nat) (default : α) : List α
   := lst ++ (List.replicate (len - lst.length) default)
 
+@[reducible]
 def decomposeToRadix (r : Nat) (v : Nat) (h : r > 1) : List Nat := match v with
 | .zero => List.nil
 | v' + 1 => List.cons ((v' + 1) % r) (decomposeToRadix r ((v' + 1) / r) h)
diff --git a/Lampe/Lampe/Builtin/Lens.lean b/Lampe/Lampe/Builtin/Lens.lean
index e77e63b..80b55fe 100644
--- a/Lampe/Lampe/Builtin/Lens.lean
+++ b/Lampe/Lampe/Builtin/Lens.lean
@@ -34,12 +34,12 @@ inductive readLensOmni (lens : Lens rep tp₁ tp₂) : Omni where
     unfold omni_frame
     intros
     cases_type readLensOmni
-    . constructor <;> tauto
-      rw [Finmap.lookup_union_left] <;> tauto
+    . constructor <;> try tauto
+      rw [Finmap.lookup_union_left] <;> try tauto
       apply Finmap.mem_of_lookup_eq_some <;> tauto
       repeat apply Exists.intro <;> tauto
-    . apply readLensOmni.err <;> tauto
-      rw [Finmap.lookup_union_left] <;> tauto
+    . apply readLensOmni.err <;> try tauto
+      rw [Finmap.lookup_union_left] <;> try tauto
       apply Finmap.mem_of_lookup_eq_some <;> tauto
  }
 
@@ -69,7 +69,7 @@ inductive readLensOmni (lens : Lens rep tp₁ tp₂) : Omni where
     rename_i p st₁ st₂ hd outTp args Q _ hd
     cases_type modifyLensOmni
     . constructor
-      rw [Finmap.lookup_union_left] <;> tauto
+      rw [Finmap.lookup_union_left] <;> try tauto
       apply Finmap.mem_of_lookup_eq_some <;> tauto
       tauto
       simp only
@@ -82,14 +82,14 @@ inductive readLensOmni (lens : Lens rep tp₁ tp₂) : Omni where
       rw [←hst]
       apply And.intro
       . rw [←Finmap.insert_eq_singleton_union]
-        apply Finmap.insert_mem_disjoint <;> tauto
+        apply Finmap.insert_mem_disjoint <;> try tauto
         apply Finmap.mem_of_lookup_eq_some <;> tauto
       . apply And.intro
         . simp [Finmap.union_assoc, Finmap.insert_eq_singleton_union]
         . apply And.intro ?_ (by rfl)
           simp_all [Finmap.insert_union, Finmap.insert_eq_singleton_union]
-    . apply modifyLensOmni.err <;> tauto
-      rw [Finmap.lookup_union_left] <;> tauto
+    . apply modifyLensOmni.err <;> try tauto
+      rw [Finmap.lookup_union_left] <;> try tauto
       apply Finmap.mem_of_lookup_eq_some <;> tauto
  }
 
@@ -115,7 +115,7 @@ def getLens (lens : Lens rep tp₁ tp₂) : Builtin := {
     unfold omni_frame
     intros
     cases_type getLensOmni
-    . constructor <;> tauto
+    . constructor <;> try tauto
       repeat apply Exists.intro <;> tauto
     . apply getLensOmni.err <;> tauto
 }
diff --git a/Lampe/Lampe/Builtin/Slice.lean b/Lampe/Lampe/Builtin/Slice.lean
index 90b736f..73d09ef 100644
--- a/Lampe/Lampe/Builtin/Slice.lean
+++ b/Lampe/Lampe/Builtin/Slice.lean
@@ -4,17 +4,17 @@ namespace Lampe.Builtin
 
 @[reducible]
 def replaceSlice' (s : Tp.denote p $ .slice tp) (i : Fin s.length) (v : Tp.denote p tp) : Tp.denote p $ .slice tp :=
-  List.modifyNth (fun _ => v) i s
+  List.modify (fun _ => v) i s
 
 @[simp]
 theorem replaceSlice_length_eq_length :
     (replaceSlice' s i v).length = s.length := by
-  simp_all [List.length_modifyNth]
+  simp_all [List.length_modify]
 
 @[simp]
 theorem index_replaced_slice :
     (replaceSlice' s idx v).get ⟨idx.val, h⟩ = v := by
-  simp_all [List.modifyNth_eq_set_get?, List.getElem_eq_iff]
+  simp_all [List.modify_eq_set_get?, List.getElem_eq_iff]
 
 /--
 Defines the builtin slice constructor.
@@ -85,7 +85,7 @@ In Noir, this builtin corresponds to `fn insert(self, index: u32, elem: T) -> Se
 def sliceInsert := newGenericPureBuiltin
   (fun tp => ⟨[.slice tp, .u 32, tp], .slice tp⟩)
   (fun _ h![l, i, e] => ⟨i.toNat < l.length,
-    fun _ => l.insertNth i.toNat e⟩)
+    fun _ => l.insertIdx i.toNat e⟩)
 
 
 /--
diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean
index 044d9b3..e624a61 100644
--- a/Lampe/Lampe/Hoare/Builtins.lean
+++ b/Lampe/Lampe/Hoare/Builtins.lean
@@ -106,68 +106,68 @@ lemma pureBuiltin_intro_consequence
    tauto
 
  theorem fAdd_intro : STHoarePureBuiltin p Γ Builtin.fAdd (by tauto) h![a, b] (a := ()) := by
-   apply pureBuiltin_intro_consequence <;> tauto
+   apply pureBuiltin_intro_consequence <;> try tauto
    tauto
 
  theorem fSub_intro : STHoarePureBuiltin p Γ Builtin.fSub (by tauto) h![a, b] (a := ()) := by
-   apply pureBuiltin_intro_consequence <;> tauto
+   apply pureBuiltin_intro_consequence <;> try tauto
    tauto
 
  theorem fMul_intro : STHoarePureBuiltin p Γ Builtin.fMul (by tauto) h![a, b] (a := ()) := by
-   apply pureBuiltin_intro_consequence <;> tauto
+   apply pureBuiltin_intro_consequence <;> try tauto
    tauto
 
  theorem fDiv_intro : STHoarePureBuiltin p Γ Builtin.fDiv (by tauto) h![a, b] (a := ()) := by
-   apply pureBuiltin_intro_consequence <;> tauto
+   apply pureBuiltin_intro_consequence <;> try tauto
    tauto
 
  theorem fNeg_intro : STHoarePureBuiltin p Γ Builtin.fNeg (by tauto) h![a] (a := ()) := by
-   apply pureBuiltin_intro_consequence <;> tauto
+   apply pureBuiltin_intro_consequence <;> try tauto
    tauto
 
 -- Arrays
 
 theorem mkArray_intro {n} {argTps : List Tp} {args : HList (Tp.denote p) argTps} {_ : argTps.length = n} :
   STHoarePureBuiltin p Γ (Builtin.mkArray n) (by tauto) args (a := (argTps, tp)) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem arrayIndex_intro : STHoarePureBuiltin p Γ Builtin.arrayIndex (by tauto) h![arr, i] (a := (tp, n)) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem arrayLen_intro : STHoarePureBuiltin p Γ Builtin.arrayLen (by tauto) h![arr] (a := (tp, n)) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem arrayAsSlice_intro : STHoarePureBuiltin p Γ Builtin.arrayAsSlice (by tauto) h![arr] (a := (tp, n)) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 -- BigInt
 
 theorem bigIntEq_intro : STHoarePureBuiltin p Γ Builtin.bigIntEq (by tauto) h![a, b] (a := ()) := by
-   apply pureBuiltin_intro_consequence <;> tauto
+   apply pureBuiltin_intro_consequence <;> try tauto
    tauto
 
 theorem bigIntAdd_intro : STHoarePureBuiltin p Γ Builtin.bigIntAdd (by tauto) h![a, b] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem bigIntSub_intro : STHoarePureBuiltin p Γ Builtin.bigIntSub (by tauto) h![a, b] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem bigIntMul_intro : STHoarePureBuiltin p Γ Builtin.bigIntMul (by tauto) h![a, b] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem bigIntDiv_intro : STHoarePureBuiltin p Γ Builtin.bigIntDiv (by tauto) h![a, b] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem bigIntFromLeBytes_intro : STHoarePureBuiltin p Γ Builtin.bigIntFromLeBytes (by tauto) h![bs, mbs] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem bigIntToLeBytes_intro : STHoarePureBuiltin p Γ Builtin.bigIntToLeBytes (by tauto) h![a] (a := ()) := by
@@ -180,67 +180,67 @@ theorem bigIntToLeBytes_intro : STHoarePureBuiltin p Γ Builtin.bigIntToLeBytes
 -- Bitwise
 
 theorem bNot_intro : STHoarePureBuiltin p Γ Builtin.bNot (by tauto) h![a] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem bAnd_intro : STHoarePureBuiltin p Γ Builtin.bAnd (by tauto) h![a, b] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem bOr_intro : STHoarePureBuiltin p Γ Builtin.bOr (by tauto) h![a, b] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem bXor_intro : STHoarePureBuiltin p Γ Builtin.bXor (by tauto) h![a, b] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem uNot_intro : STHoarePureBuiltin p Γ Builtin.uNot (by tauto) h![a] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem uOr_intro : STHoarePureBuiltin p Γ Builtin.uOr (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem uAnd_intro : STHoarePureBuiltin p Γ Builtin.uAnd (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem uXor_intro : STHoarePureBuiltin p Γ Builtin.uXor (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem uShl_intro : STHoarePureBuiltin p Γ Builtin.uShl (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem uShr_intro : STHoarePureBuiltin p Γ Builtin.uShl (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem iNot_intro : STHoarePureBuiltin p Γ Builtin.iNot (by tauto) h![a] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem iAnd_intro : STHoarePureBuiltin p Γ Builtin.iAnd (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem iOr_intro : STHoarePureBuiltin p Γ Builtin.iOr (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem iXor_intro : STHoarePureBuiltin p Γ Builtin.iXor (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem iShl_intro : STHoarePureBuiltin p Γ Builtin.iShl (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem iShr_intro : STHoarePureBuiltin p Γ Builtin.iShr (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 -- Comparison
@@ -249,81 +249,81 @@ theorem unitEq_intro : STHoarePureBuiltin p Γ Builtin.unitEq (by tauto) h![a, b
    apply pureBuiltin_intro_consequence <;> tauto
 
 theorem bEq_intro : STHoarePureBuiltin p Γ Builtin.bEq (by tauto) h![a, b] (a := ()) := by
-   apply pureBuiltin_intro_consequence <;> tauto
+   apply pureBuiltin_intro_consequence <;> try tauto
    tauto
 
 theorem fEq_intro : STHoarePureBuiltin p Γ Builtin.fEq (by tauto) h![a, b] (a := ()) := by
-   apply pureBuiltin_intro_consequence <;> tauto
+   apply pureBuiltin_intro_consequence <;> try tauto
    tauto
 
 theorem uEq_intro : STHoarePureBuiltin p Γ Builtin.uEq (by tauto) h![a, b] := by
-   apply pureBuiltin_intro_consequence <;> tauto
+   apply pureBuiltin_intro_consequence <;> try tauto
    tauto
 
 theorem iEq_intro : STHoarePureBuiltin p Γ Builtin.uEq (by tauto) h![a, b] := by
-   apply pureBuiltin_intro_consequence <;> tauto
+   apply pureBuiltin_intro_consequence <;> try tauto
    tauto
 
 theorem strEq_intro : STHoarePureBuiltin p Γ Builtin.strEq (by tauto) h![a, b] := by
-   apply pureBuiltin_intro_consequence <;> tauto
+   apply pureBuiltin_intro_consequence <;> try tauto
    tauto
 
 theorem uLt_intro : STHoarePureBuiltin p Γ Builtin.uLt (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem iLt_intro : STHoarePureBuiltin p Γ Builtin.iLt (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem uGt_intro : STHoarePureBuiltin p Γ Builtin.uGt (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem iGt_intro : STHoarePureBuiltin p Γ Builtin.iGt (by tauto) h![a, b] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 -- Field misc
 
 theorem fApplyRangeConstraint_intro :
   STHoarePureBuiltin p Γ Builtin.fApplyRangeConstraint (by tauto) h![f, c] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem fModNumBits_intro : STHoarePureBuiltin p Γ Builtin.fModNumBits (by tauto) h![f] (a := ())  := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem fModLeBits_intro : STHoarePureBuiltin p Γ Builtin.fModLeBits (by tauto) h![f] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem fModBeBits_intro : STHoarePureBuiltin p Γ Builtin.fModLeBits (by tauto) h![f] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem fModLeBytes_intro : STHoarePureBuiltin p Γ Builtin.fModLeBytes (by tauto) h![f] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem fModBeBytes_intro : STHoarePureBuiltin p Γ Builtin.fModLeBytes (by tauto) h![f] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem uFromField_intro : STHoarePureBuiltin p Γ Builtin.uFromField (by tauto) h![f] (a := s) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem iFromField_intro : STHoarePureBuiltin p Γ Builtin.iFromField (by tauto) h![f] (a := s) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 -- Slice
 
 theorem mkSlice_intro {n} {argTps : List Tp} {args : HList (Tp.denote p) argTps} {_ : argTps.length = n} :
   STHoarePureBuiltin p Γ (Builtin.mkSlice n) (by tauto) args (a := (argTps, tp)) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem sliceLen_intro : STHoarePureBuiltin p Γ Builtin.sliceLen (by tauto) h![s] := by
@@ -361,7 +361,7 @@ theorem sliceRemove_intro : STHoarePureBuiltin p Γ Builtin.sliceRemove (by taut
 -- String
 
 theorem strAsBytes_intro : STHoarePureBuiltin p Γ Builtin.strAsBytes (by tauto) h![s] := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 -- Memory
@@ -459,11 +459,11 @@ theorem writeRef_intro :
 -- Struct/tuple
 
 theorem mkTuple_intro : STHoarePureBuiltin p Γ Builtin.mkTuple (by tauto) fieldExprs (a := (name, fieldTps)) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem projectTuple_intro : STHoarePureBuiltin p Γ (Builtin.projectTuple mem) (by tauto) h![tpl] (a := name) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 -- Lens
@@ -477,10 +477,10 @@ theorem readLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
   intros H st h
   constructor
   cases hl : (lens.get s)
-  . apply Builtin.readLensOmni.err <;> tauto
+  . apply Builtin.readLensOmni.err <;> try tauto
     unfold SLP.star State.valSingleton at *
     aesop
-  . apply Builtin.readLensOmni.ok <;> tauto
+  . apply Builtin.readLensOmni.ok <;> try tauto
     . unfold SLP.star State.valSingleton at *
       aesop
     . unfold mapToValHeapCondition
@@ -497,10 +497,10 @@ theorem readLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
   intros H st h
   constructor
   cases hl : (lens.modify s v)
-  . apply Builtin.modifyLensOmni.err <;> tauto
+  . apply Builtin.modifyLensOmni.err <;> try tauto
     unfold SLP.star State.valSingleton at *
     aesop
-  . apply Builtin.modifyLensOmni.ok <;> tauto
+  . apply Builtin.modifyLensOmni.ok <;> try tauto
     . unfold SLP.star State.valSingleton at *
       aesop
     . unfold mapToValHeapCondition
@@ -535,7 +535,7 @@ theorem getLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
   constructor
   cases hl : (lens.get s)
   . apply Builtin.getLensOmni.err <;> tauto
-  . apply Builtin.getLensOmni.ok <;> tauto
+  . apply Builtin.getLensOmni.ok <;> try tauto
     . unfold mapToValHeapCondition
       simp_all only [Option.map_some', SLP.true_star, SLP.star_assoc]
       apply SLP.ent_star_top at h
@@ -544,7 +544,7 @@ theorem getLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
 -- Misc
 
 theorem assert_intro : STHoarePureBuiltin p Γ Builtin.assert (by tauto) h![a] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
+  apply pureBuiltin_intro_consequence <;> try tauto
   tauto
 
 theorem cast_intro [Builtin.CastTp tp tp'] : STHoare p Γ ⟦⟧ (.callBuiltin [tp] tp' .cast h![v])
diff --git a/Lampe/Lampe/Hoare/SepTotal.lean b/Lampe/Lampe/Hoare/SepTotal.lean
index 08fb103..d88a643 100644
--- a/Lampe/Lampe/Hoare/SepTotal.lean
+++ b/Lampe/Lampe/Hoare/SepTotal.lean
@@ -347,7 +347,8 @@ theorem callLambda_intro {lambdaBody} {P : SLP $ State p}
     simp only [SLP.star, SLP.exists', SLP.lift] at h
     tauto
   obtain ⟨r, _⟩ := h₁
-  apply Omni.callLambda <;> tauto
+  apply Omni.callLambda (ref := r) (lambdaBody := lambdaBody)
+  · tauto
   . obtain ⟨st₁, st₂, _, _, ⟨_, _, _, _, _, _, _, _, _, _, ⟨_, _⟩, _⟩, _⟩ := h
     subst_vars
     simp_all only [FuncRef.lambda.injEq]
@@ -361,7 +362,7 @@ theorem callLambda_intro {lambdaBody} {P : SLP $ State p}
       simp_all only
       tauto
     . simp_all
-  apply STHoare.consequence_frame_left <;> tauto
+  · apply STHoare.consequence_frame_left <;> tauto
 
 theorem callDecl_intro {fnRef : Tp.denote p (.fn argTps outTp)}
     {href : H ⊢ ⟦fnRef = (.decl fnName kinds generics)⟧ ⋆ (⊤ : SLP $ State p)}
diff --git a/Lampe/Lampe/Lens.lean b/Lampe/Lampe/Lens.lean
index 213537b..b7e6caf 100644
--- a/Lampe/Lampe/Lens.lean
+++ b/Lampe/Lampe/Lens.lean
@@ -33,9 +33,9 @@ theorem Access.modify_get {acc : Access (Tp.denote p) tp₁ tp₂} {h : acc.modi
   case slice =>
     rename_i idx
     cases em (idx.toNat < s.length)
-    . simp_all only [reduceDIte, Option.some.injEq, List.get_eq_getElem, dite_some_none_eq_some]
+    . simp_all only [reduceDIte, Option.some.injEq, List.get_eq_getElem, Option.dite_none_right_eq_some]
       subst h
-      simp_all only [List.length_modifyNth, exists_true_left]
+      simp_all only [List.length_modify, exists_true_left]
       apply Builtin.index_replaced_slice
     . aesop
 
diff --git a/Lampe/Lampe/Semantics.lean b/Lampe/Lampe/Semantics.lean
index 69586bb..d834927 100644
--- a/Lampe/Lampe/Semantics.lean
+++ b/Lampe/Lampe/Semantics.lean
@@ -160,11 +160,6 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
     intro hd
     apply Omni.callLambda <;> try tauto
     simp_all
-    simp only [LawfulHeap.disjoint] at hd
-    rw [Finmap.lookup_union_left]
-    tauto
-    rw [Finmap.mem_iff]
-    tauto
   | callBuiltin hq =>
     rename Builtin => b
     intros
diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean
index 3be2229..7d1c5d7 100644
--- a/Lampe/Lampe/Tactic/SeparationLogic.lean
+++ b/Lampe/Lampe/Tactic/SeparationLogic.lean
@@ -212,36 +212,36 @@ def isIte (e : Expr) : Bool := e.isAppOf `Lampe.Expr.ite
 partial def parseSLExpr (e: Expr): TacticM SLTerm := do
   if e.isAppOf ``SLP.star then
     let args := e.getAppArgs
-    let fst ← parseSLExpr (←args[2]?)
-    let snd ← parseSLExpr (←args[3]?)
+    let fst ← parseSLExpr (←liftOption args[2]?)
+    let snd ← parseSLExpr (←liftOption args[3]?)
     return SLTerm.star e fst snd
   if e.isAppOf ``State.valSingleton then
     let args := e.getAppArgs
-    let fst ← args[1]?
-    let snd ← args[2]?
+    let fst ← liftOption args[1]?
+    let snd ← liftOption args[2]?
     return SLTerm.singleton fst snd
   else if e.isAppOf ``State.lmbSingleton then
     let args := e.getAppArgs
-    let fst ← args[1]?
-    let snd ← args[2]?
+    let fst ← liftOption args[1]?
+    let snd ← liftOption args[2]?
     return SLTerm.lmbSingleton fst snd
   else if e.isAppOf ``SLP.top then
     return SLTerm.top
   else if e.isAppOf ``SLP.lift then
     let args := e.getAppArgs
-    return SLTerm.lift (←args[2]?)
+    return SLTerm.lift (←liftOption args[2]?)
   else if e.getAppFn.isMVar then
     return SLTerm.mvar e
   else if e.isAppOf ``SLP.forall' then
     let args := e.getAppArgs
-    return SLTerm.all (←args[3]?)
+    return SLTerm.all (←liftOption args[3]?)
   else if e.isAppOf ``SLP.exists' then
     let args := e.getAppArgs
-    return SLTerm.exi (←args[3]?)
+    return SLTerm.exi (←liftOption args[3]?)
   else if e.isAppOf ``SLP.wand then
     let args := e.getAppArgs
-    let lhs ← parseSLExpr (←args[2]?)
-    let rhs ← parseSLExpr (←args[3]?)
+    let lhs ← parseSLExpr (←liftOption args[2]?)
+    let rhs ← parseSLExpr (←liftOption args[3]?)
     return SLTerm.wand lhs rhs
   -- else if e.isAppOf ``SLTerm.lift then
   --   let args := e.getAppArgs
@@ -257,8 +257,8 @@ partial def parseSLExpr (e: Expr): TacticM SLTerm := do
 partial def parseEntailment (e: Expr): TacticM (SLTerm × SLTerm) := do
   if e.isAppOf ``SLP.entails then
     let args := e.getAppArgs
-    let pre ← parseSLExpr (←args[2]?)
-    let post ← parseSLExpr (←args[3]?)
+    let pre ← parseSLExpr (←liftOption args[2]?)
+    let post ← parseSLExpr (←liftOption args[3]?)
     return (pre, post)
   else throwError "not an entailment {e}"
 
@@ -390,7 +390,7 @@ partial def solveSingletonStarMV (goal : MVarId) (lhs : SLTerm) (rhs : Expr): Ta
   | SLTerm.singleton v _ =>
     if v == rhs then
       let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``singleton_congr_mv)
-      let newGoal ← newGoals[0]?
+      let newGoal ← liftOption newGoals[0]?
       let newGoal ← try newGoal.refl; pure []
         catch _ => pure [newGoal]
       pure $ newGoal ++ newGoals
@@ -398,7 +398,7 @@ partial def solveSingletonStarMV (goal : MVarId) (lhs : SLTerm) (rhs : Expr): Ta
   | SLTerm.lmbSingleton v _ =>
     if v == rhs then
       let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``lmbSingleton_congr_mv)
-      let newGoal ← newGoals[0]?
+      let newGoal ← liftOption newGoals[0]?
       let newGoal ← try newGoal.refl; pure []
         catch _ => pure [newGoal]
       pure $ newGoal ++ newGoals
@@ -409,37 +409,37 @@ partial def solveSingletonStarMV (goal : MVarId) (lhs : SLTerm) (rhs : Expr): Ta
       if v == rhs then
         -- [TODO] This should use EQ, not ent_self
         let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``singleton_star_congr)
-        let newGoal ← newGoals[0]?
+        let newGoal ← liftOption newGoals[0]?
         let newGoal ← try newGoal.refl; pure []
           catch _ => pure [newGoal]
         pure $ newGoal ++ newGoals
       else
         let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``use_right)
-        let newGoal ← newGoals[0]?
+        let newGoal ← liftOption newGoals[0]?
         let new' ← solveSingletonStarMV newGoal r rhs
         return new' ++ newGoals
     | SLTerm.lmbSingleton v _ => do
       if v == rhs then
         -- [TODO] This should use EQ, not ent_self as well
         let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``lmbSingleton_star_congr)
-        let newGoal ← newGoals[0]?
+        let newGoal ← liftOption newGoals[0]?
         let newGoal ← try newGoal.refl; pure []
           catch _ => pure [newGoal]
         pure $ newGoal ++ newGoals
       else
         let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``use_right)
-        let newGoal ← newGoals[0]?
+        let newGoal ← liftOption newGoals[0]?
         let new' ← solveSingletonStarMV newGoal r rhs
         return new' ++ newGoals
     | SLTerm.lift _ =>
       let goals ← goal.apply (←mkConstWithFreshMVarLevels ``pure_star_H_ent_pure_star_mv)
-      let g ← goals[0]?
+      let g ← liftOption goals[0]?
       let (_, g) ← g.intro1
       let ng ← solveSingletonStarMV g r rhs
       return ng ++ goals
     | _ =>
       let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``use_right)
-      let newGoal ← newGoals[0]?
+      let newGoal ← liftOption newGoals[0]?
       let new' ← solveSingletonStarMV newGoal r rhs
       return new' ++ newGoals
   | _ => throwError "not a singleton {lhs}"
@@ -451,13 +451,13 @@ partial def solvePureStarMV (goal : MVarId) (lhs : SLTerm): TacticM (List MVarId
     match l with
     | .lift _ =>
       let goals ← goal.apply (←mkConstWithFreshMVarLevels ``pure_star_H_ent_pure_star_mv)
-      let g ← goals[0]?
+      let g ← liftOption goals[0]?
       let (_, g) ← g.intro1
       let ng ← solvePureStarMV g r
       return ng ++ goals
     | _ =>
       let goals ← goal.apply (←mkConstWithFreshMVarLevels ``skip_left_ent_star_mv)
-      let g ← goals[0]?
+      let g ← liftOption goals[0]?
       let ng ← solvePureStarMV g l
       return ng ++ goals
   | .singleton _ _ =>
@@ -475,14 +475,14 @@ partial def solveStarMV (goal : MVarId) (lhs : SLTerm) (rhsNonMv : SLTerm): Tact
 
 partial def solveEntailment (goal : MVarId): TacticM (List MVarId) := do
   let newGoal ← evalTacticAt (←`(tactic|h_norm)) goal
-  let goal ← newGoal[0]?
+  let goal ← liftOption newGoal[0]?
   let target ← goal.instantiateMVarsInType
   let (pre, post) ← parseEntailment target
 
   match pre with
   | SLTerm.exi _ => do
     let newGoals ← goal.apply (←mkConstWithFreshMVarLevels ``exi_prop_l)
-    let newGoal ← newGoals[0]?
+    let newGoal ← liftOption newGoals[0]?
     let (_, newGoal) ← newGoal.intro1
     let gls ← solveEntailment newGoal
     return gls ++ newGoals
@@ -500,7 +500,7 @@ partial def solveEntailment (goal : MVarId): TacticM (List MVarId) := do
       return newGoals
     else if r.isTop then
       let g ← goal.apply (←mkConstWithFreshMVarLevels ``star_top_of_star_mvar)
-      let g' ← g[0]?
+      let g' ← liftOption g[0]?
       let ng ← solveEntailment g'
       pure $ ng ++ g
     else if r.isForAll then
@@ -511,18 +511,18 @@ partial def solveEntailment (goal : MVarId): TacticM (List MVarId) := do
     goal.apply (←mkConstWithFreshMVarLevels ``SLP.entails_self)
   | SLTerm.all _ => do
     let new ← goal.apply (←mkConstWithFreshMVarLevels ``SLP.forall_right)
-    let new' ← new[0]?
+    let new' ← liftOption new[0]?
     let (_, g) ← new'.intro1
     solveEntailment g
   | SLTerm.wand _ _ =>
     let new ← goal.apply (←mkConstWithFreshMVarLevels ``SLP.wand_intro)
-    let new' ← new[0]?
+    let new' ← liftOption new[0]?
     solveEntailment new'
   | SLTerm.exi _ =>
     -- [TODO] this only works for prop existential - make the others an error
     let new ← goal.apply (←mkConstWithFreshMVarLevels ``exi_prop)
-    let newL ← solveEntailment (←new[0]?)
-    let (_, newR) ← (←new[1]?).intro1
+    let newL ← solveEntailment (←liftOption new[0]?)
+    let (_, newR) ← (←liftOption new[1]?).intro1
     let newR ← solveEntailment newR
     return newL ++ newR
   | _ => throwError "unknown rhs {post}"
diff --git a/Lampe/Lampe/Tp.lean b/Lampe/Lampe/Tp.lean
index 81a9f57..9228267 100644
--- a/Lampe/Lampe/Tp.lean
+++ b/Lampe/Lampe/Tp.lean
@@ -54,10 +54,10 @@ def Tp.denote : Tp → Type
 | .bi => Int
 | .bool => Bool
 | .unit => Unit
-| .str n => Mathlib.Vector Char n.toNat
+| .str n => List.Vector Char n.toNat
 | .field => Fp p
 | .slice tp => List (denote tp)
-| .array tp n => Mathlib.Vector (denote tp) n.toNat
+| .array tp n => List.Vector (denote tp) n.toNat
 | .ref _ => Ref
 | .tuple _ fields => Tp.denoteArgs fields
 | .fn argTps outTp => FuncRef argTps outTp
diff --git a/Lampe/lake-manifest.json b/Lampe/lake-manifest.json
index 27c12b4..877a8f7 100644
--- a/Lampe/lake-manifest.json
+++ b/Lampe/lake-manifest.json
@@ -1,85 +1,95 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
-   "name": "batteries",
+   "rev": "e9ae2a61ef5c99d6edac84f0d04f6324c5d97f67",
+   "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
+   "inputRev": "v4.15.0-patch1",
+   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
-   "name": "Qq",
+   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.15.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa",
-   "name": "aesop",
+   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
+   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.42",
+   "inputRev": "v0.0.48",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
-   "name": "Cli",
+   "scope": "leanprover-community",
+   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
-   "name": "importGraph",
+   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
-   "name": "LeanSearchClient",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a",
-   "name": "mathlib",
+   "scope": "leanprover",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.12.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "Lampe",
  "lakeDir": ".lake"}
diff --git a/Lampe/lakefile.lean b/Lampe/lakefile.lean
index 993711c..13eba5e 100644
--- a/Lampe/lakefile.lean
+++ b/Lampe/lakefile.lean
@@ -8,7 +8,7 @@ package «Lampe» where
   ]
   -- add any additional package configuration options here
 
-require "leanprover-community" / "mathlib" @ git "v4.12.0"
+require "leanprover-community" / "mathlib" @ git "v4.15.0-patch1"
 
 @[default_target]
 lean_lib «Lampe» where
diff --git a/Lampe/lean-toolchain b/Lampe/lean-toolchain
index 8998520..d0eb99f 100644
--- a/Lampe/lean-toolchain
+++ b/Lampe/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.15.0