diff --git a/pyproject.toml b/pyproject.toml
index 0b315c6..44a3bba 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -18,7 +18,7 @@ packages = ["src/clever_bench"]
 
 [project]
 name = "clever-bench"
-version = "1.6.0"
+version = "1.7.0"
 authors = [
   { name="Amitayush Thakur", email="amitayush@utexas.edu" },
 ]
diff --git a/src/lean4/Imports/AllImports.lean b/src/lean4/Imports/AllImports.lean
index 9c3ec14..7eb4cbd 100644
--- a/src/lean4/Imports/AllImports.lean
+++ b/src/lean4/Imports/AllImports.lean
@@ -72,15 +72,11 @@ sample_problems:
 def string_eq_iff_data_eq (s1: String) (s2: String)
 : s1.data = s2.data ↔ s1 = s2 :=
 by
-  apply Iff.intro
-  intro h
-  cases s1
-  cases s2
-  simp at h
-  simp [h]
-  intro h
-  apply String.data_eq_of_eq
-  exact h
+  constructor
+  · intro h
+    exact String.ext h
+  · intro h
+    exact congrArg String.data h
 -- end_def helper_definitions
 
 -- start_def helper_definitions
@@ -104,29 +100,22 @@ if paren_string.isEmpty then
 else
   let c := paren_string.get! 0
   if c == '(' then
-    string_is_paren_balanced_helper (paren_string.drop 1) (num_open + 1)
+    string_is_paren_balanced_helper (String.ofList (paren_string.toList.drop 1)) (num_open + 1)
   else if c == ')' then
-    string_is_paren_balanced_helper (paren_string.drop 1) (num_open - 1)
+    string_is_paren_balanced_helper (String.ofList (paren_string.toList.drop 1)) (num_open - 1)
   else
-    string_is_paren_balanced_helper (paren_string.drop 1) num_open
+    string_is_paren_balanced_helper (String.ofList (paren_string.toList.drop 1)) num_open
 termination_by paren_string.length
 decreasing_by
   all_goals
   {
-    rename_i h_non_empty_string
-    rw [String.drop_eq, String.length]
-    simp
+    simp only [String.length_ofList, List.length_drop]
+    have h_non_empty_string : ¬ paren_string.isEmpty = true := by assumption
     rw [String.isEmpty_iff] at h_non_empty_string
-    by_cases h_paren_nil : paren_string.length ≤ 0
-    rw [Nat.le_zero_eq] at h_paren_nil
-    rw [←string_eq_iff_data_eq] at h_non_empty_string
-    have h_temp : "".data = [] := by simp
-    rw [h_temp] at h_non_empty_string
-    rw [String.length] at h_paren_nil
-    rw [List.length_eq_zero_iff] at h_paren_nil
-    contradiction
-    have h_temp : paren_string.length > 0 := by linarith
-    assumption
+    have hne : paren_string.toList ≠ [] := by simpa using h_non_empty_string
+    have hpos : 0 < paren_string.toList.length := List.length_pos_of_ne_nil hne
+    have hlen : paren_string.length = paren_string.toList.length := by simp
+    omega
   }
 -- end_def helper_definitions
 
@@ -182,31 +171,24 @@ if paren_string.isEmpty then
 else
   let c := paren_string.get! 0
   if c == '(' then
-    count_paren_groups_helper (paren_string.drop 1) (num_open + 1) num_groups
+    count_paren_groups_helper (String.ofList (paren_string.toList.drop 1)) (num_open + 1) num_groups
   else if c == ')' then
     let new_num_groups :=
     if num_open == 1 then num_groups + 1 else num_groups
-    count_paren_groups_helper (paren_string.drop 1) (num_open - 1) new_num_groups
+    count_paren_groups_helper (String.ofList (paren_string.toList.drop 1)) (num_open - 1) new_num_groups
   else
-    count_paren_groups_helper (paren_string.drop 1) num_open num_groups
+    count_paren_groups_helper (String.ofList (paren_string.toList.drop 1)) num_open num_groups
 termination_by paren_string.length
 decreasing_by
   all_goals
   {
-    rename_i h_non_empty_string
-    rw [String.drop_eq, String.length]
-    simp
+    simp only [String.length_ofList, List.length_drop]
+    have h_non_empty_string : ¬ paren_string.isEmpty = true := by assumption
     rw [String.isEmpty_iff] at h_non_empty_string
-    by_cases h_paren_nil : paren_string.length ≤ 0
-    rw [Nat.le_zero_eq] at h_paren_nil
-    rw [←string_eq_iff_data_eq] at h_non_empty_string
-    have h_temp : "".data = [] := by simp
-    rw [h_temp] at h_non_empty_string
-    rw [String.length] at h_paren_nil
-    rw [List.length_eq_zero_iff] at h_paren_nil
-    contradiction
-    have h_temp : paren_string.length > 0 := by linarith
-    assumption
+    have hne : paren_string.toList ≠ [] := by simpa using h_non_empty_string
+    have hpos : 0 < paren_string.toList.length := List.length_pos_of_ne_nil hne
+    have hlen : paren_string.length = paren_string.toList.length := by simp
+    omega
   }
 -- end_def helper_definitions
 
@@ -241,29 +223,22 @@ else
   let c := paren_string.get! 0
   if c == '(' then
     let new_num_open := num_open + 1
-    count_max_paren_depth_helper (paren_string.drop 1) (new_num_open) (max_depth.max new_num_open.toNat)
+    count_max_paren_depth_helper (String.ofList (paren_string.toList.drop 1)) (new_num_open) (max_depth.max new_num_open.toNat)
   else if c == ')' then
-    count_max_paren_depth_helper (paren_string.drop 1) (num_open - 1) max_depth
+    count_max_paren_depth_helper (String.ofList (paren_string.toList.drop 1)) (num_open - 1) max_depth
   else
-    count_max_paren_depth_helper (paren_string.drop 1) num_open max_depth
+    count_max_paren_depth_helper (String.ofList (paren_string.toList.drop 1)) num_open max_depth
 termination_by paren_string.length
 decreasing_by
   all_goals
   {
-    rename_i h_non_empty_string
-    rw [String.drop_eq, String.length]
-    simp
+    simp only [String.length_ofList, List.length_drop]
+    have h_non_empty_string : ¬ paren_string.isEmpty = true := by assumption
     rw [String.isEmpty_iff] at h_non_empty_string
-    by_cases h_paren_nil : paren_string.length ≤ 0
-    rw [Nat.le_zero_eq] at h_paren_nil
-    rw [←string_eq_iff_data_eq] at h_non_empty_string
-    have h_temp : "".data = [] := by simp
-    rw [h_temp] at h_non_empty_string
-    rw [String.length] at h_paren_nil
-    rw [List.length_eq_zero_iff] at h_paren_nil
-    contradiction
-    have h_temp : paren_string.length > 0 := by linarith
-    assumption
+    have hne : paren_string.toList ≠ [] := by simpa using h_non_empty_string
+    have hpos : 0 < paren_string.toList.length := List.length_pos_of_ne_nil hne
+    have hlen : paren_string.length = paren_string.toList.length := by simp
+    omega
   }
 -- end_def helper_definitions
 
diff --git a/src/lean4/human_eval/problem_0.lean b/src/lean4/human_eval/problem_0.lean
index 6bd3386..10e1b64 100644
--- a/src/lean4/human_eval/problem_0.lean
+++ b/src/lean4/human_eval/problem_0.lean
@@ -22,7 +22,7 @@ def problem_spec
 -- spec
 let numbers_within_threshold :=
 (∃ i j, i < numbers.length ∧ j < numbers.length ∧
-i ≠ j ∧ |numbers.get! i - numbers.get! j| < threshold);
+i ≠ j ∧ |numbers[i]! - numbers[j]!| < threshold);
 let spec (res: Bool) :=
 numbers.length > 1 →
 if res then numbers_within_threshold else ¬numbers_within_threshold;
@@ -273,14 +273,12 @@ by_cases h_1_lt_tail : 1 < tail.length
 simp [h_1_lt_tail] at ih
 obtain ⟨ i, h_i_lt_tail_len, h_i_in_threshold ⟩ := ih
 use i + 1
-have h_i_lt_tail_len' : i + 1 < tail.length + 1 := by linarith
-simp [h_i_lt_tail_len']
+refine ⟨by omega, ?_⟩
 obtain ⟨ j, h_j_lt_tail_len, h_i_neq_j, h_j_in_threshold ⟩ := h_i_in_threshold
-use j + 1
-simp [h_j_lt_tail_len]
-simp [h_i_neq_j]
-simp [h_i_lt_tail_len, h_j_lt_tail_len] at h_j_in_threshold
-assumption
+refine ⟨j + 1, by omega, ?_, ?_⟩
+· simp [h_i_neq_j]
+· simp [h_i_lt_tail_len, h_j_lt_tail_len] at h_j_in_threshold ⊢
+  exact h_j_in_threshold
 use 0
 simp
 use 1
@@ -292,7 +290,7 @@ simp [h_tail_empty] at h_tail_has_close_elements
 simp at h_1_lt_tail
 have h_0_lt_tail_len : tail.length = 1 := by linarith
 have h_tail_singleton: ∃ x, tail = [x] := by
-  rw [List.length_eq_one] at h_0_lt_tail_len
+  rw [List.length_eq_one_iff] at h_0_lt_tail_len
   assumption
 obtain ⟨ x, h_tail_singleton ⟩ := h_tail_singleton
 simp [h_0_lt_tail_len]
diff --git a/src/lean4/human_eval/problem_101.lean b/src/lean4/human_eval/problem_101.lean
index 5ab68b7..e7444c0 100644
--- a/src/lean4/human_eval/problem_101.lean
+++ b/src/lean4/human_eval/problem_101.lean
@@ -24,9 +24,9 @@ def problem_spec
 let spec (result: List String) :=
   let chars := s.toList;
   let trimmed := String.mk (chars.dropWhile (fun c => c = ' ' ∨ c = ','));
-  let first := trimmed.takeWhile (fun c => c ≠ ',' ∧ c ≠ ' ');
+  let first := (trimmed.takeWhile (fun c => c ≠ ',' ∧ c ≠ ' ')).toString;
   (result = [] ↔ (∀ x ∈ chars, x = ' ' ∨ x = ',') ∨ s = "") ∧
-  (result ≠ [] ↔ result = [first] ++ (implementation (trimmed.drop (first.length + 1))))
+  (result ≠ [] ↔ result = [first] ++ (implementation (trimmed.drop (first.length + 1)).toString))
 
 -- program termination
 ∃ result, implementation s = result ∧
@@ -59,7 +59,7 @@ def implementation (s: String) : List String :=
 -- end_def implementation_signature
 -- start_def implementation
   let normalized := String.mk (s.toList.map (fun c => if c = ',' then ' ' else c))
-  normalized.split (· == ' ') |>.filter (fun w => w ≠ "")
+  normalized.splitToList (· == ' ') |>.filter (fun w => w ≠ "")
 -- end_def implementation
 
 -- Uncomment the following test cases after implementing the function
diff --git a/src/lean4/human_eval/problem_103.lean b/src/lean4/human_eval/problem_103.lean
index 37cc1d8..80f607c 100644
--- a/src/lean4/human_eval/problem_103.lean
+++ b/src/lean4/human_eval/problem_103.lean
@@ -36,7 +36,7 @@ let spec (result: Option String) :=
     let xs := List.Ico n (m+1);
     let avg := xs.sum / xs.length;
     (val.take 2 = "0b") ∧
-    (Nat.ofDigits 2 ((val.drop 2).toList.map (fun c => c.toNat - '0'.toNat)).reverse = avg)))
+    (Nat.ofDigits 2 ((val.drop 2).toString.toList.map (fun c => c.toNat - '0'.toNat)).reverse = avg)))
 -- program termination
 ∃ result, implementation n m = result ∧
 spec result
diff --git a/src/lean4/human_eval/problem_11.lean b/src/lean4/human_eval/problem_11.lean
index ff3c4f0..2516832 100644
--- a/src/lean4/human_eval/problem_11.lean
+++ b/src/lean4/human_eval/problem_11.lean
@@ -28,9 +28,8 @@ let spec (result: String) :=
   result.length = a.length ∧
   result.all (fun c => c = '0' ∨ c = '1') ∧
   (∀ i, i < a.length →
-  let i_pos := String.Pos.mk i;
-  (a.get i_pos = b.get i_pos → result.get i_pos = '0') ∧
-  (a.get i_pos ≠ b.get i_pos → result.get i_pos = '1'));
+  (a.data[i]! = b.data[i]! → result.data[i]! = '0') ∧
+  (a.data[i]! ≠ b.data[i]! → result.data[i]! = '1'));
 -- program termination
 ∃ result, implementation a b = result ∧
 spec result
diff --git a/src/lean4/human_eval/problem_110.lean b/src/lean4/human_eval/problem_110.lean
index d7443c4..2663e9c 100644
--- a/src/lean4/human_eval/problem_110.lean
+++ b/src/lean4/human_eval/problem_110.lean
@@ -37,11 +37,11 @@ let spec (result : String) :=
     lst1_idxs.Nodup ∧
     lst2_idxs.Nodup ∧
     ∀ i, i < lst1.length →
-      (i ∉ lst1_idxs → Even (lst1.get! i)) ∧
+      (i ∉ lst1_idxs → Even (lst1[i]!)) ∧
       (i ∈ lst1_idxs →
         -- find the (a, b) in exchange where a = i
         let i_idx := (lst1_idxs.indexesOf i).head!
-        Even (lst2.get! (lst2_idxs.get! i_idx)))
+        Even (lst2[lst2_idxs[i_idx]!]!))
   (bool_result → result = "YES") ∧
   (result = "NO" → ¬ bool_result) ∧
   (result ≠ "YES" ∧ result ≠ "NO" → False)
diff --git a/src/lean4/human_eval/problem_112.lean b/src/lean4/human_eval/problem_112.lean
index 32d62b1..f3bdcb4 100644
--- a/src/lean4/human_eval/problem_112.lean
+++ b/src/lean4/human_eval/problem_112.lean
@@ -35,7 +35,7 @@ let spec (result : String × Bool) :=
     result_str =
     (implementation
       (String.join ((s.data.filter (fun x => x ≠ c.data.head!)).map (fun c => String.mk [c])))
-      (c.drop 1)).fst)
+      (c.drop 1).toString).fst)
 
 -- program termination
 ∃ result,
diff --git a/src/lean4/human_eval/problem_116.lean b/src/lean4/human_eval/problem_116.lean
index 7652be7..6f4f878 100644
--- a/src/lean4/human_eval/problem_116.lean
+++ b/src/lean4/human_eval/problem_116.lean
@@ -26,8 +26,8 @@ let spec (result : List Nat) :=
   ∀ x : Nat, lst.count x = result.count x ∧
   result.length = lst.length ∧
   (∀ i j : Nat, i < j → j < result.length →
-    Nat.digits 2 (result.get! i) < Nat.digits 2 (result.get! j) ∨
-    (Nat.digits 2 (result.get! i) = Nat.digits 2 (result.get! j) ∧ result.get! i < result.get! j))
+    Nat.digits 2 (result[i]!) < Nat.digits 2 (result[j]!) ∨
+    (Nat.digits 2 (result[i]!) = Nat.digits 2 (result[j]!) ∧ result[i]! < result[j]!))
 -- program termination
 ∃ result,
   implementation lst = result ∧
diff --git a/src/lean4/human_eval/problem_125.lean b/src/lean4/human_eval/problem_125.lean
index c0b1c1b..24c7beb 100644
--- a/src/lean4/human_eval/problem_125.lean
+++ b/src/lean4/human_eval/problem_125.lean
@@ -41,24 +41,24 @@ def problem_spec
 -- spec
 let lexographically_less (a b: List Nat) : Prop :=
   a.length = b.length ∧ a.length = k ∧
-  (∃ i, i < k ∧ a.get! i < b.get! i ∧
-  (∀ j, j < i → a.get! j = b.get! j));
+  (∃ i, i < k ∧ a[i]! < b[i]! ∧
+  (∀ j, j < i → a[j]! = b[j]!));
 let rec is_valid_path (k': Nat) (path: List Nat) (grid: List (List Nat)) : Prop :=
   let n := grid.length;
   path.length = k' →
   (∃ i j,
-    (i < n ∧ j < n ∧ path.get! 0 = (grid.get! i).get! j) ∧
+    (i < n ∧ j < n ∧ path[0]! = (grid[i]!)[j]!) ∧
     (1 < path.length →
       ( ∃ i' j', i' < n ∧ j' < n ∧
-        (path.get! 1 = (grid.get! i').get! j') ∧
+        (path[1]! = (grid[i']!)[j']!) ∧
         ((abs ((i: Int) - (i': Int)) = 1 ∧ j = j') ∨
          (abs ((j: Int) - (j': Int)) = 1 ∧ i = i'))) ∧
       (is_valid_path (k' - 1) (path.drop 1) grid))
   );
 let spec (result: List Nat) :=
   let n := grid.length;
-  (∀ i, i < n → (grid.get! i).length = n) →
-  (∀ i j, i < n → j < n ↔ ((grid.get! i).get! j) ∈ [1, n^2]) →
+  (∀ i, i < n → (grid[i]!).length = n) →
+  (∀ i j, i < n → j < n ↔ ((grid[i]!)[j]!) ∈ [1, n^2]) →
   is_valid_path k result grid ∧ (∀ path, is_valid_path k path grid → lexographically_less result path);
 -- program terminates
 ∃ result, impl grid k = result ∧
diff --git a/src/lean4/human_eval/problem_129.lean b/src/lean4/human_eval/problem_129.lean
index 7eda708..5e1def1 100644
--- a/src/lean4/human_eval/problem_129.lean
+++ b/src/lean4/human_eval/problem_129.lean
@@ -34,11 +34,11 @@ let spec (result: Option (List String) × Option Nat) :=
     (words = none ↔ ∀ ch, ch ∈ text.toList →  (ch = ',' ∨ ch = ' ')) ∧
     (∀ num, ord = some num → (text.get! 0).toNat = num) ∧
     (∀ lst, words = some lst → ∀ i, i < lst.length →
-      let str := lst.get! i;
+      let str := lst[i]!;
       text.containsSubstr str) ∧
     (∀ lst, words = some lst →
-      let first := text.takeWhile (fun c => c ≠ ',' ∧ c ≠ ' ');
-      let nextImpl := impl (text.drop (first.length + 1));
+      let first := (text.takeWhile (fun c => c ≠ ',' ∧ c ≠ ' ')).toString;
+      let nextImpl := impl ((text.drop (first.length + 1)).toString);
       let nextWords := nextImpl.fst;
       (∃ nextLst, nextWords = some nextLst ∧
         lst = [first] ++ nextLst))
diff --git a/src/lean4/human_eval/problem_140.lean b/src/lean4/human_eval/problem_140.lean
index a29037e..5305aa0 100644
--- a/src/lean4/human_eval/problem_140.lean
+++ b/src/lean4/human_eval/problem_140.lean
@@ -36,8 +36,8 @@ let spec (result: String) :=
     ∨
     (∃ pref s : String, text = pref ++ s ∧ pref ≠ "" ∧ (∀ ch, ch ∈ pref.toList → ch = ' ')
       ∧ let k := pref.length;
-        (k ≤ 2 → result = (String.replicate k '_') ++ (impl (text.drop k)))
-      ∧ (2 < k → result = "-" ++ (impl (text.drop k)))) )
+        (k ≤ 2 → result = (String.replicate k '_') ++ (impl (text.drop k).toString))
+      ∧ (2 < k → result = "-" ++ (impl (text.drop k).toString))) )
   )
 -- program termination
 ∃ result, impl text = result ∧
diff --git a/src/lean4/human_eval/problem_153.lean b/src/lean4/human_eval/problem_153.lean
index 8e9d66d..597d5ba 100644
--- a/src/lean4/human_eval/problem_153.lean
+++ b/src/lean4/human_eval/problem_153.lean
@@ -40,8 +40,8 @@ let last_pos := result.revPosOf '.';
 0 < extensions.length ∧ extensions.all (fun x => 0 < x.length) ∧ 0 < class_name.length →
 0 < result.length ∧
 last_pos.isSome ∧
-let class_name' := result.take (last_pos.get!).byteIdx;
-let extension_name := result.drop ((last_pos.get!).byteIdx + 1);
+let class_name' := (result.take (last_pos.get!).byteIdx).toString;
+let extension_name := (result.drop ((last_pos.get!).byteIdx + 1)).toString;
 class_name' = class_name ∧
 extension_name ∈ extensions ∧
 let strength_of_extensions := extensions.map (fun ext => strength ext);
diff --git a/src/lean4/human_eval/problem_154.lean b/src/lean4/human_eval/problem_154.lean
index da90dbc..c2d429e 100644
--- a/src/lean4/human_eval/problem_154.lean
+++ b/src/lean4/human_eval/problem_154.lean
@@ -33,7 +33,7 @@ let spec (result: Bool) :=
 (0 < b.length →
 result ↔ ((b.length ≤ a.length) ∧
   (∃ i : Nat, i < b.length ∧
-  let b_rotation := b.drop i ++ b.take i;
+  let b_rotation := (b.drop i).toString ++ (b.take i).toString;
   a.containsSubstr b_rotation)));
 -- program terminates
 ∃ result, impl a b = result ∧
diff --git a/src/lean4/human_eval/problem_158.lean b/src/lean4/human_eval/problem_158.lean
index 5ebcd25..20f87b7 100644
--- a/src/lean4/human_eval/problem_158.lean
+++ b/src/lean4/human_eval/problem_158.lean
@@ -26,7 +26,7 @@ def problem_spec
 (words: List String) :=
 let unique_chars (string: String) :=
   let string_idx := {i: Nat | i < string.length}.toFinset;
-  let characters := string_idx.image (fun i => string.toList.get! i);
+  let characters := string_idx.image (fun i => string.toList[i]!);
   characters.card;
 -- spec
 let spec (result: String) :=
diff --git a/src/lean4/human_eval/problem_16.lean b/src/lean4/human_eval/problem_16.lean
index ff46184..f7640fc 100644
--- a/src/lean4/human_eval/problem_16.lean
+++ b/src/lean4/human_eval/problem_16.lean
@@ -22,7 +22,7 @@ def problem_spec
 -- spec
 let spec (result: Nat) :=
 let string_idx := {i: Nat | i < string.length}.toFinset
-let characters := string_idx.image (fun i => string.toList.get! i)
+let characters := string_idx.image (fun i => string.toList[i]!)
 let lowercase_characters := characters.image (fun c => c.toLower)
 result = lowercase_characters.card;
 -- program termination
@@ -80,17 +80,12 @@ simp [result]
 simp [implementation]
 rcases string with ⟨data⟩
 induction data
-simp
+try simp
 have h1: "".toLower = "" := by
   unfold String.toLower
   unfold Char.toLower
   unfold String.map
   unfold String.mapAux
   simp
-simp [h1]
-rename_i head tail ih
-unfold String.toLower
-rw [String.map_eq]
-simp
 sorry
 -- end_def correctness_proof
diff --git a/src/lean4/human_eval/problem_17.lean b/src/lean4/human_eval/problem_17.lean
index 8243c4a..2a9858a 100644
--- a/src/lean4/human_eval/problem_17.lean
+++ b/src/lean4/human_eval/problem_17.lean
@@ -33,7 +33,7 @@ let not_map := fun
 let spec (result: List Nat) :=
 let space_split := string.splitOn " ";
 space_split.length = result.length ∧
-∀ i < result.length, not_map (space_split.get! i) = result.get! i;
+∀ i < result.length, not_map (space_split[i]!) = result[i]!;
 -- program termination
 ∃ result, implementation string = result ∧
 spec result
diff --git a/src/lean4/human_eval/problem_23.lean b/src/lean4/human_eval/problem_23.lean
index 5d663f7..fd6dc8a 100644
--- a/src/lean4/human_eval/problem_23.lean
+++ b/src/lean4/human_eval/problem_23.lean
@@ -23,7 +23,7 @@ def problem_spec
 let spec (result: Nat) :=
 -- every character in the string is counted once
 result = 0 ↔ string.isEmpty ∧
-(0 < result → result - 1 = implementation (string.drop 1))
+(0 < result → result - 1 = implementation (string.drop 1).toString)
 -- program termination
 ∃ result, implementation string = result ∧
 spec result
diff --git a/src/lean4/human_eval/problem_27.lean b/src/lean4/human_eval/problem_27.lean
index 9c47fd2..982df02 100644
--- a/src/lean4/human_eval/problem_27.lean
+++ b/src/lean4/human_eval/problem_27.lean
@@ -23,8 +23,8 @@ let chars_in_result := result.toList;
 let chars_in_string := string.toList;
 chars_in_result.length = string.length ∧
 (∀ i, i < chars_in_result.length →
-  let c := chars_in_result.get! i;
-  let c' := chars_in_string.get! i;
+  let c := chars_in_result[i]!;
+  let c' := chars_in_string[i]!;
   (c.isUpper → c'.isLower) ∧
   (c.isLower → c'.isUpper) ∧
   ((¬ c.isUpper ∧ ¬ c.isLower) → c = c')
diff --git a/src/lean4/human_eval/problem_28.lean b/src/lean4/human_eval/problem_28.lean
index 8eafb5b..3f5ba02 100644
--- a/src/lean4/human_eval/problem_28.lean
+++ b/src/lean4/human_eval/problem_28.lean
@@ -24,7 +24,7 @@ let spec (result: String) :=
 let result_chars := result.toList;
 result_chars.length = (strings.map (λ s => s.length)).sum ∧
 ∀ i, i < strings.length →
-(let string_in_result := strings.get! i;
+(let string_in_result := strings[i]!;
 let end_idx := ((strings.take (i + 1)).map (λ s => s.length)).sum;
 let start_idx := end_idx - string_in_result.length;
 let corresponding_string_in_result := ((result_chars.take end_idx).drop start_idx).asString;
diff --git a/src/lean4/human_eval/problem_33.lean b/src/lean4/human_eval/problem_33.lean
index 88ff637..c1e5516 100644
--- a/src/lean4/human_eval/problem_33.lean
+++ b/src/lean4/human_eval/problem_33.lean
@@ -25,9 +25,9 @@ def problem_spec
 let spec (result: List Int) :=
   l.length = result.length ∧
   let every_third_idx := (List.range l.length).filter (λ i => i % 3 = 0);
-  let every_third_val_in_result := every_third_idx.map (λ i => result.get! i);
-  let every_third_val := every_third_idx.map (λ i => l.get! i);
-  (∀ i, i < l.length → (i % 3 ≠ 0 → l.get! i = result.get! i)) ∧
+  let every_third_val_in_result := every_third_idx.map (λ i => result[i]!);
+  let every_third_val := every_third_idx.map (λ i => l[i]!);
+  (∀ i, i < l.length → (i % 3 ≠ 0 → l[i]! = result[i]!)) ∧
   List.Sorted Int.le every_third_val_in_result ∧
   every_third_val.all (λ x => every_third_val_in_result.count x = every_third_val.count x);
 -- program termination
@@ -61,10 +61,10 @@ def implementation (l: List Int) : List Int :=
 -- end_def implementation_signature
 -- start_def implementation
 let every_third_idx := (List.range l.length).filter (λ i => i % 3 = 0);
-let every_third_val := every_third_idx.map (λ i => l.get! i);
+let every_third_val := every_third_idx.map (λ i => l[i]!);
 let every_third_val_sorted := List.mergeSort every_third_val;
 let result := l.mapIdx (λ i v =>
-  if i % 3 = 0 then every_third_val_sorted.get! (i / 3)
+  if i % 3 = 0 then every_third_val_sorted[i / 3]!
   else v);
 result
 -- end_def implementation
diff --git a/src/lean4/human_eval/problem_35.lean b/src/lean4/human_eval/problem_35.lean
index afa66ea..ec86e68 100644
--- a/src/lean4/human_eval/problem_35.lean
+++ b/src/lean4/human_eval/problem_35.lean
@@ -22,8 +22,8 @@ def problem_spec
 -- spec
 let spec (result: Int) :=
   l.length > 0 →
-  ((∀ i, i < l.length → l.get! i ≤ result) ∧
-  (∃ i, i < l.length ∧ l.get! i = result));
+  ((∀ i, i < l.length → l[i]! ≤ result) ∧
+  (∃ i, i < l.length ∧ l[i]! = result));
 -- program termination
 ∃ result, implementation l = result ∧
 spec result
diff --git a/src/lean4/human_eval/problem_37.lean b/src/lean4/human_eval/problem_37.lean
index 2c6e9b1..f611a78 100644
--- a/src/lean4/human_eval/problem_37.lean
+++ b/src/lean4/human_eval/problem_37.lean
@@ -25,9 +25,9 @@ def problem_spec
 let spec (result: List Int) :=
   l.length = result.length ∧
   let even_idx := (List.range l.length).filter (λ i => i % 2 = 0);
-  let even_val_in_result := even_idx.map (λ i => result.get! i);
-  let even_val := even_idx.map (λ i => l.get! i);
-  (∀ i, i < l.length → (i % 2 ≠ 0 → l.get! i = result.get! i)) ∧
+  let even_val_in_result := even_idx.map (λ i => result[i]!);
+  let even_val := even_idx.map (λ i => l[i]!);
+  (∀ i, i < l.length → (i % 2 ≠ 0 → l[i]! = result[i]!)) ∧
   List.Sorted Int.le even_val_in_result ∧
   even_val.all (λ x => even_val_in_result.count x = even_val.count x);
 -- program termination
@@ -61,10 +61,10 @@ def implementation (l: List Int) : List Int :=
 -- end_def implementation_signature
 -- start_def implementation
 let even_idx := (List.range l.length).filter (λ i => i % 2 = 0);
-let even_val := even_idx.map (λ i => l.get! i);
+let even_val := even_idx.map (λ i => l[i]!);
 let even_val_sorted := List.mergeSort even_val;
 let result := l.mapIdx (λ i v =>
-  if i % 2 = 0 then even_val_sorted.get! (i / 2)
+  if i % 2 = 0 then even_val_sorted[i / 2]!
   else v);
 result
 -- end_def implementation
diff --git a/src/lean4/human_eval/problem_38.lean b/src/lean4/human_eval/problem_38.lean
index f04c928..aa13c2a 100644
--- a/src/lean4/human_eval/problem_38.lean
+++ b/src/lean4/human_eval/problem_38.lean
@@ -30,7 +30,7 @@ let spec (result: String) :=
   encoded_chars.length = n ∧
   (∀ i : ℕ, i * 3 + 3 ≤ n →
     extract encoded_chars (i * 3) (i * 3 + 2) =
-      [original_chars.get! (i * 3 + 1), original_chars.get! (i * 3 + 2), original_chars.get! (i * 3)]) ∧
+      [original_chars[i * 3 + 1]!, original_chars[i * 3 + 2]!, original_chars[i * 3]!]) ∧
   (n % 3 ≠ 0 → extract encoded_chars (n - n % 3) (n - 1) =
     extract original_chars (n - n % 3) (n - 1));
 -- program termination
diff --git a/src/lean4/human_eval/problem_4.lean b/src/lean4/human_eval/problem_4.lean
index 74afb1b..aa560f2 100644
--- a/src/lean4/human_eval/problem_4.lean
+++ b/src/lean4/human_eval/problem_4.lean
@@ -94,8 +94,7 @@ simp [h]
 rename_i h
 simp at h
 have h1: 0 < numbers.length := by
-  by_contra
-  rename_i h2
+  by_contra h2
   simp at h2
   contradiction
 simp [h1]
diff --git a/src/lean4/human_eval/problem_6.lean b/src/lean4/human_eval/problem_6.lean
index da7cb76..bfc530f 100644
--- a/src/lean4/human_eval/problem_6.lean
+++ b/src/lean4/human_eval/problem_6.lean
@@ -22,7 +22,7 @@ def problem_spec
 :=
 -- spec
 let spec (result: List Nat) :=
-let paren_space_split := paren_string.split (fun x => x = ' ');
+let paren_space_split := paren_string.splitToList (fun x => x = ' ');
 result.length = paren_space_split.length ∧
 ∀ i, i < result.length →
 let group := paren_space_split[i]!;
@@ -58,7 +58,7 @@ sorry
 def implementation (paren_string: String) : List Nat :=
 -- end_def implementation_signature
 -- start_def implementation
-(paren_string.split (fun x => x = ' ')).map (fun x => count_max_paren_depth x)
+(paren_string.splitToList (fun x => x = ' ')).map (fun x => count_max_paren_depth x)
 -- end_def implementation
 
 -- Uncomment the following test cases after implementing the function
diff --git a/src/lean4/human_eval/problem_64.lean b/src/lean4/human_eval/problem_64.lean
index 5659f9b..cea8d87 100644
--- a/src/lean4/human_eval/problem_64.lean
+++ b/src/lean4/human_eval/problem_64.lean
@@ -32,7 +32,7 @@ string.data.all (fun c => c.isAlpha) →
 if string.length = 1 then
   result = if isVowel string.data[0]! ∨ isY string.data[0]! then 1 else 0
 else
-  result = (if isVowel string.data[0]! then 1 else 0) + implementation (string.drop 1);
+  result = (if isVowel string.data[0]! then 1 else 0) + implementation (string.drop 1).toString;
 -- program termination
 ∃ result, implementation string = result ∧
 spec result
diff --git a/src/lean4/human_eval/problem_66.lean b/src/lean4/human_eval/problem_66.lean
index 3532ef8..d0f8740 100644
--- a/src/lean4/human_eval/problem_66.lean
+++ b/src/lean4/human_eval/problem_66.lean
@@ -29,7 +29,7 @@ let spec (result: Nat) :=
 if string.length = 1 then
   result = if isUpper string.data[0]! then string.data[0]!.toNat else 0
 else
-  result = (if isUpper string.data[0]! then string.data[0]!.toNat else 0) + implementation (string.drop 1);
+  result = (if isUpper string.data[0]! then string.data[0]!.toNat else 0) + implementation (string.drop 1).toString;
 -- program termination
 ∃ result, implementation string = result ∧
 spec result
diff --git a/src/lean4/human_eval/problem_78.lean b/src/lean4/human_eval/problem_78.lean
index 6ec035d..17aa19e 100644
--- a/src/lean4/human_eval/problem_78.lean
+++ b/src/lean4/human_eval/problem_78.lean
@@ -47,10 +47,10 @@ let spec (result: Int) :=
     let char_val := num_val num.toList[0]!;
     let is_prime_hex := Nat.Prime char_val ∧ char_val ≤ 15;
     (is_prime_hex →
-      (1 < num.length → result = 1 + implementation (num.drop 1)) ∧
+      (1 < num.length → result = 1 + implementation (num.drop 1).toString) ∧
       (1 = num.length → result = 1)) ∧
     (¬is_prime_hex →
-      (1 < num.length → result = implementation (num.drop 1)) ∧
+      (1 < num.length → result = implementation (num.drop 1).toString) ∧
       (1 = num.length → result = 0))
   )
 -- program termination
diff --git a/src/lean4/human_eval/problem_80.lean b/src/lean4/human_eval/problem_80.lean
index 51f2e89..38ed8d7 100644
--- a/src/lean4/human_eval/problem_80.lean
+++ b/src/lean4/human_eval/problem_80.lean
@@ -31,7 +31,7 @@ def problem_spec
 let spec (result : Bool) :=
   result ↔
   (3 ≤ s.length) ∧
-  ¬ (∃ i j, i < j ∧ j < s.length ∧ j - i ≤ 2 ∧ s.data.get! i = s.data.get! j)
+  ¬ (∃ i j, i < j ∧ j < s.length ∧ j - i ≤ 2 ∧ s.data[i]! = s.data[j]!)
 -- program termination
 ∃ result,
   implementation s = result ∧
diff --git a/src/lean4/human_eval/problem_86.lean b/src/lean4/human_eval/problem_86.lean
index 3adbeca..41a567d 100644
--- a/src/lean4/human_eval/problem_86.lean
+++ b/src/lean4/human_eval/problem_86.lean
@@ -29,8 +29,8 @@ def problem_spec
 -- spec
 let spec (result : String) :=
   result.length = s.length ∧
-  let words := result.split (fun c => c = ' ');
-  let s_words := s.split (fun c => c = ' ');
+  let words := result.splitToList (fun c => c = ' ');
+  let s_words := s.splitToList (fun c => c = ' ');
   s_words.length = words.length ∧
   ∀ i, i < words.length →
     words[i]!.length = s_words[i]!.length ∧
diff --git a/src/lean4/human_eval/problem_90.lean b/src/lean4/human_eval/problem_90.lean
index e0f56c3..13a4992 100644
--- a/src/lean4/human_eval/problem_90.lean
+++ b/src/lean4/human_eval/problem_90.lean
@@ -34,11 +34,11 @@ def problem_spec
 -- spec
 let spec (result : Option Int) :=
   match result with
-  | none => ¬ (∃ i j, i < lst.length ∧ j < lst.length ∧ i ≠ j ∧ lst.get! i < lst.get! j)
+  | none => ¬ (∃ i j, i < lst.length ∧ j < lst.length ∧ i ≠ j ∧ lst[i]! < lst[j]!)
   | some result =>
     let smaller_els := lst.filter (· < result);
     0 < smaller_els.length ∧
-    smaller_els.all (λ x => x = smaller_els.get! 0);
+    smaller_els.all (λ x => x = smaller_els[0]!);
 -- program termination
 ∃ result,
   implementation lst = result ∧
diff --git a/src/lean4/human_eval/problem_91.lean b/src/lean4/human_eval/problem_91.lean
index 87c2b0c..f9a9d4c 100644
--- a/src/lean4/human_eval/problem_91.lean
+++ b/src/lean4/human_eval/problem_91.lean
@@ -28,7 +28,7 @@ let spec (result : Nat) :=
   match s.data.findIdx? (λ c => c = '.' ∨ c = '?' ∨ c = '!') with
   | some i =>
     let j := i + 1;
-    let substring := s.drop j;
+    let substring := (s.drop j).toString;
     result = (if is_sentence_is_boredom substring then 1 else 0) + implementation substring
   | none =>
     result = if is_sentence_is_boredom s then 1 else 0
diff --git a/src/lean4/human_eval/problem_93.lean b/src/lean4/human_eval/problem_93.lean
index 40632f7..a0de91d 100644
--- a/src/lean4/human_eval/problem_93.lean
+++ b/src/lean4/human_eval/problem_93.lean
@@ -28,8 +28,8 @@ let spec (result : String) :=
   s.data.all (λ c => c.isAlpha) →
   result.length = s.length ∧
   (∀ i, i < s.length →
-    let c := s.data.get! i;
-    let c' := result.data.get! i;
+    let c := s.data[i]!;
+    let c' := result.data[i]!;
     match c with
     | 'a' | 'e' | 'i' | 'o' | 'u' | 'A' | 'E' | 'I' | 'O' | 'U' =>
       c.isUpper → c'.val = c.toLower.val + 2 ∧
diff --git a/src/lean4/human_eval/problem_94.lean b/src/lean4/human_eval/problem_94.lean
index 8854658..fb5b627 100644
--- a/src/lean4/human_eval/problem_94.lean
+++ b/src/lean4/human_eval/problem_94.lean
@@ -32,9 +32,9 @@ def problem_spec
 -- spec
 let spec (result : Nat) :=
   lst.any (fun num => Nat.Prime num) →
-    result > 0 ∧ ∃ i, i < lst.length ∧ Prime (lst.get! i) ∧
-    (∀ j, j < lst.length ∧ Prime (lst.get! j) → lst.get! i ≤ lst.get! j) ∧
-    result = (Nat.digits 10 (lst.get! i)).sum
+    result > 0 ∧ ∃ i, i < lst.length ∧ Prime (lst[i]!) ∧
+    (∀ j, j < lst.length ∧ Prime (lst[j]!) → lst[i]! ≤ lst[j]!) ∧
+    result = (Nat.digits 10 (lst[i]!)).sum
 -- program termination
 ∃ result,
   implementation lst = result ∧
diff --git a/src/lean4/human_eval/problem_96.lean b/src/lean4/human_eval/problem_96.lean
index 42f151e..7b77591 100644
--- a/src/lean4/human_eval/problem_96.lean
+++ b/src/lean4/human_eval/problem_96.lean
@@ -32,7 +32,7 @@ def problem_spec
 let spec (result : List Nat) :=
   match n with
   | 0 => result = []
-  | n => n > 0 → (∀ i, i < result.length → (Nat.Prime (result.get! i)) ∧ (result.get! i) < n) ∧
+  | n => n > 0 → (∀ i, i < result.length → (Nat.Prime (result[i]!)) ∧ (result[i]!) < n) ∧
          (∀ i : Nat, i < n → Nat.Prime i → i ∈ result)
 -- program termination
 ∃ result,
diff --git a/src/lean4/human_eval/problem_99.lean b/src/lean4/human_eval/problem_99.lean
index c0b9378..b39e4f8 100644
--- a/src/lean4/human_eval/problem_99.lean
+++ b/src/lean4/human_eval/problem_99.lean
@@ -33,10 +33,10 @@ let is_valid_string :=
 let spec (result : Option Int) := match result with
   | some result =>
     is_valid_string ∧
-    let parts := s.split (fun c => c = '.')
+    let parts := s.splitToList (fun c => c = '.')
     (parts.length = 1 → result = s.toInt!) ∧
     (parts.length = 2 →
-      let integer_part := parts.get! 0
+      let integer_part := parts[0]!
       let is_negative := s.data.head! = '-'
       |((integer_part.toInt! - result) : ℚ)| ≤ 0.5 ∧
       (is_negative → |((integer_part.toInt! - result) : ℚ)| = 0.5 → integer_part.toInt? < result) ∧
diff --git a/src/lean4/lake-manifest.json b/src/lean4/lake-manifest.json
index 94c89bd..764c94d 100644
--- a/src/lean4/lake-manifest.json
+++ b/src/lean4/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7",
+   "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.24.0",
+   "inputRev": "v4.27.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805",
+   "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d768126816be17600904726ca7976b185786e6b9",
+   "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "556caed0eadb7901e068131d1be208dd907d07a2",
+   "rev": "c04225ee7c0585effbd933662b3151f01b600e40",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.74",
+   "inputRev": "v0.0.85",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
+   "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c",
+   "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "rev": "55c37290ff6186e2e965d68cf853a57c0702db82",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.27.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "clever",
diff --git a/src/lean4/lakefile.lean b/src/lean4/lakefile.lean
index a4064c4..752ab96 100644
--- a/src/lean4/lakefile.lean
+++ b/src/lean4/lakefile.lean
@@ -6,7 +6,7 @@ package «clever» where
   leanOptions := #[
     ⟨`autoImplicit, false⟩
   ]
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.24.0"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.27.0"
 
 @[default_target]
 lean_lib «clever» where
diff --git a/src/lean4/lean-toolchain b/src/lean4/lean-toolchain
index c00a535..5249182 100644
--- a/src/lean4/lean-toolchain
+++ b/src/lean4/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.27.0
diff --git a/src/lean4/sample_examples/problem_1.lean b/src/lean4/sample_examples/problem_1.lean
index 2dfc690..4e1babc 100644
--- a/src/lean4/sample_examples/problem_1.lean
+++ b/src/lean4/sample_examples/problem_1.lean
@@ -801,8 +801,7 @@ exact h_stop
 -- Case 2: where implementation.loop score_changes threshold 0 0 ≠ 0
 simp [h_implementation_stop]
 have h_implementation_stop': 0 < implementation.loop score_changes threshold 0 0 := by
-  by_contra
-  rename_i h_implementation_stop_false
+  by_contra h_implementation_stop_false
   simp at h_implementation_stop_false
   contradiction
 have h_continue := implementation_loop_invariant_continue score_changes threshold 0 0 h_rounds_played h_implementation_stop'