diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean
index 5b29b79..e8309a5 100644
--- a/Auto/EvaluateAuto/TestAuto.lean
+++ b/Auto/EvaluateAuto/TestAuto.lean
@@ -164,18 +164,18 @@ def readRunAutoOnConstsResult (resultFile : String) : CoreM (Array (Name × Resu
 where
   analyzeLine (fileName line : String) : CoreM (Name × Result × Nat × Nat) := do
     let line := (line.dropWhile (fun c => c != ' ')).drop 1
-    let s := line.takeWhile (fun c => c != ' ')
+    let s := (line.takeWhile (fun c => c != ' ')).toString
     let .some res := Result.ofConcise? s
       | throwError s!"{decl_name%} :: In file {fileName}, {s} is not a concise representation of a `Result`"
-    let line := (line.dropWhile (fun c => c != ' ')).drop 1
-    let s := line.takeWhile (fun c => c != ' ')
+    let line := ((line.dropWhile (fun c => c != ' ')).drop 1).toString
+    let s := (line.takeWhile (fun c => c != ' ')).toString
     let .some time := String.toNat? s
       | throwError s!"{decl_name%} :: In file {fileName}, {s} is not a string representation of a Nat"
-    let line := (line.dropWhile (fun c => c != ' ')).drop 1
-    let s := line.takeWhile (fun c => c != ' ')
+    let line := ((line.dropWhile (fun c => c != ' ')).drop 1).toString
+    let s := (line.takeWhile (fun c => c != ' ')).toString
     let .some hb := String.toNat? s
       | throwError s!"{decl_name%} :: In file {fileName}, {s} is not a string representation of a Nat"
-    let line := (line.dropWhile (fun c => c != ' ')).drop 1
+    let line := ((line.dropWhile (fun c => c != ' ')).drop 1).toString
     let name := Name.parseUniqRepr line
     return (name, res, time, hb)
 
@@ -332,7 +332,7 @@ def readEATAResult (config : EvalAutoAsyncConfig) :
   let allFiles := (← System.FilePath.readDir resultFolder).map IO.FS.DirEntry.path
   let mut ret := #[]
   for file in allFiles do
-    if !(← System.FilePath.isDir file) && file.toString.takeRight 7 == ".result" then
+    if !(← System.FilePath.isDir file) && file.toString.takeEnd 7 == ".result" then
       ret := ret.append (← readRunAutoOnConstsResult file.toString)
   return ret
 
diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean
index 9240817..73f49cb 100644
--- a/Auto/EvaluateAuto/TestTactics.lean
+++ b/Auto/EvaluateAuto/TestTactics.lean
@@ -335,14 +335,14 @@ def readEvalTacticsAtModuleResult (resultFile : String) : CoreM (Array (Name ×
 where
   analyzeLine (fileName line : String) : CoreM (Name × Array (Result × Nat × Nat)) := do
     let line := (line.dropWhile (fun c => c != ' ')).drop 3
-    let tr := (line.takeWhile (fun c => c != ']')).splitOn ", "
-    let tr : Array (Result × Nat × Nat) ← (Array.mk tr).mapM (fun s => do
+    let tr := ((line.takeWhile (fun c => c != ']')).split ", ").toStringArray
+    let tr : Array (Result × Nat × Nat) ← tr.mapM (fun s => do
       let [sr, st, sh] := s.splitOn " "
         | throwError "s!{decl_name%} :: In file {fileName}, {s} is not of the form `<result> <time> <heartbeats>`"
       match Result.ofConcise? sr, String.toNat? st, String.toNat? sh with
       | .some r, .some t, .some h => return (r, t, h)
       | _, _, _ => throwError s!"{decl_name%} :: In file {fileName}, {s} is not of the form `<result> <time> <heartbeats>`")
-    let line := (line.dropWhile (fun c => c != ']')).drop 2
+    let line := ((line.dropWhile (fun c => c != ']')).drop 2).toString
     let name := Name.parseUniqRepr line
     return (name, tr)
 
@@ -493,10 +493,10 @@ def readETMHTResult (config : EvalTacticOnMathlibConfig) :
   let allPaths ← System.FilePath.walkDir resultFolder
   let mut ret := #[]
   for path in allPaths do
-    if !(← System.FilePath.isDir path) && path.toString.takeRight 7 == ".result" then
+    if !(← System.FilePath.isDir path) && path.toString.takeEnd 7 == ".result" then
       let content ← readEvalTacticsAtModuleResult path.toString
-      let suffix := (path.toString.drop (resultFolder.length + 1)).dropRight 7
-      let modName := (suffix.splitOn "/").foldl (fun a b => Name.str a b) .anonymous
+      let suffix := (path.toString.drop (resultFolder.length + 1)).dropEnd 7
+      let modName := (suffix.split "/").toStringArray.foldl (fun a b => Name.str a b) .anonymous
       ret := ret.push (modName, content)
   return ret
 
@@ -513,14 +513,14 @@ def readETMHTResultAllowNonRet (config : EvalTacticOnMathlibConfig) :
   let mut ret := #[]
   let mut nonRet := #[]
   for path in allPaths do
-    if !(← System.FilePath.isDir path) && path.toString.takeRight 7 == ".result" then
+    if !(← System.FilePath.isDir path) && path.toString.takeEnd 7 == ".result" then
       let raw ← IO.FS.readFile path
       if raw.length == 0 then
-        nonRet := nonRet.push (path.toString.dropRight 7)
+        nonRet := nonRet.push (path.toString.dropEnd 7).toString
         continue
       let content ← readEvalTacticsAtModuleResult path.toString
-      let suffix := (path.toString.drop (resultFolder.length + 1)).dropRight 7
-      let modName := (suffix.splitOn "/").foldl (fun a b => Name.str a b) .anonymous
+      let suffix := (path.toString.drop (resultFolder.length + 1)).dropEnd 7
+      let modName := (suffix.split "/").toStringArray.foldl (fun a b => Name.str a b) .anonymous
       ret := ret.push (modName, content)
   return (nonRet, ret)
 
@@ -579,7 +579,7 @@ def readETMHTEvaluateFiles (config : EvalTacticOnMathlibConfig) : CoreM (Array N
     if line.contains ':' then
       let [name, retCode] := line.splitOn ":"
         | throwError "{decl_name%} :: Unexpected line format, line content : `{line}`"
-      let name := name.dropRight 1
+      let name := (name.dropEnd 1).toString
       let retCode := retCode.drop 1
       let some retCode := retCode.toNat?
         | throwError "{decl_name%} :: Unexpected line format, line content : `{line}`"
diff --git a/Auto/EvaluateAuto/TestTranslation.lean b/Auto/EvaluateAuto/TestTranslation.lean
index b490a12..1d6b2df 100644
--- a/Auto/EvaluateAuto/TestTranslation.lean
+++ b/Auto/EvaluateAuto/TestTranslation.lean
@@ -104,7 +104,7 @@ where analyzeLine (line : String) : CoreM (Name × Nat × Option Nat) := do
   let .some rawSize := rawSizeStr.toNat?
     | throwError "{decl_name%} :: {rawSizeStr} is not a string representation of a Nat"
   let monoSizeStr := line.takeWhile (fun c => c != ' ')
-  let line := (line.dropWhile (fun c => c != ' ')).drop 1
+  let line := ((line.dropWhile (fun c => c != ' ')).drop 1).toString
   let mut monoSize? : Option Nat := .none
   if monoSizeStr != "N" then
     let .some monoSize := monoSizeStr.toNat?
diff --git a/Auto/IR/SMT.lean b/Auto/IR/SMT.lean
index 550f442..63f8a7c 100644
--- a/Auto/IR/SMT.lean
+++ b/Auto/IR/SMT.lean
@@ -14,7 +14,7 @@ namespace IR.SMT
 def isSimpleSymbol (s : String) : Bool :=
   let symbSpecials := "~!@$%^&*_-+=<>.?/"
   let front := s.front.isAlpha || (symbSpecials.contains s.front)
-  let body := s.all (fun c => c.isAlphanum || symbSpecials.contains c)
+  let body := s.all (fun (c : Char) => c.isAlphanum || symbSpecials.contains c)
   s.length != 0 && front && body
 
 -- <index>      ::= <numeral> | <symbol>
diff --git a/Auto/Parser/SMTSexp.lean b/Auto/Parser/SMTSexp.lean
index 1052f9f..c434833 100644
--- a/Auto/Parser/SMTSexp.lean
+++ b/Auto/Parser/SMTSexp.lean
@@ -72,14 +72,14 @@ def LexVal.ofString (s : String) (attr : String) : LexVal :=
     let bdigs := s.drop 2
     .nat (bdigs.foldl (fun x c => x * 2 + c.toNat - '0'.toNat) 0)
   | "string" =>
-    let subs := ((s.drop 1).take (s.length - 2)).splitOn "\"\""
+    let subs := (((s.drop 1).take (s.length - 2)).split "\"\"").toStringList
     .str (String.intercalate "\"" subs)
   | "simplesymbol" => .symb s
-  | "quotedsymbol" => .symb ((s.drop 1).take (s.length - 2))
-  | "keyword"      => .kw (s.drop 1)
+  | "quotedsymbol" => .symb ((s.drop 1).take (s.length - 2)).toString
+  | "keyword"      => .kw (s.drop 1).toString
   | "comment"      =>
     let rn : Nat := if String.Pos.Raw.get s (String.Pos.Raw.prev s (String.Pos.Raw.prev s s.rawEndPos)) == '\r' then 1 else 0
-    .comment ((s.drop 1).take (s.length - 2 - rn))
+    .comment ((s.drop 1).take (s.length - 2 - rn)).toString
   | _              => panic! s!"LexVal.ofString :: {repr attr} is not a valid attribute"
 
 inductive Sexp where
diff --git a/Auto/Parser/TPTP.lean b/Auto/Parser/TPTP.lean
index 6eca131..61ce34a 100644
--- a/Auto/Parser/TPTP.lean
+++ b/Auto/Parser/TPTP.lean
@@ -398,7 +398,7 @@ def ident2StringConst (s : String) : Option StringConst :=
       match x, y.toNat? with
       | .some l, .some y' => .some (l.push (Char.ofNat y'))
       | _,       _        => .none
-    match s.take 9, (((s.drop 9).splitOn "d").drop 1).foldl foldFn (.some "") with
+    match s.take 9, (((s.drop 9).split "d").drop 1).toStringArray.foldl foldFn (.some "") with
     | "t_strVal_", .some s => .some (.strVal s)
     | _,         _       => .none
 
@@ -426,7 +426,7 @@ open Embedding.Lam in
 def ident2BitVecConst (s : String) : Option BitVecConst :=
   match s.take 7 with
   | "t_bvVal" =>
-    match (s.drop 7).splitOn "_" with
+    match ((s.drop 7).split "_").toList with
     | ["", ns, is] =>
       match ns.toNat?, is.toNat? with
       | .some n, .some i => .some (.bvVal n i)
@@ -548,35 +548,35 @@ def ident2BitVecConst (s : String) : Option BitVecConst :=
       | "ashr", .some n => .some (.bvsmtashr n)
       | _,      _       => .none
   | "t_bvapp" =>
-    match s.take 11, (s.drop 11).splitOn "_" with
+    match s.take 11, ((s.drop 11).split "_").toList with
     | "t_bvappend_", [ns, ms] =>
       match ns.toNat?, ms.toNat? with
       | .some n, .some m => .some (.bvappend n m)
       | _,       _       => .none
     | _,             _        => .none
   | "t_bvext" =>
-    match s.take 12, (s.drop 12).splitOn "_" with
+    match s.take 12, ((s.drop 12).split "_").toList with
     | "t_bvextract_", [ns, hs, ls] =>
       match ns.toNat?, hs.toNat?, ls.toNat? with
       | .some n, .some h, .some l => .some (.bvextract n h l)
       | _,       _,       _       => .none
     | _,              _            => .none
   | "t_bvrep" =>
-    match s.take 11, (s.drop 11).splitOn "_" with
+    match s.take 11, ((s.drop 11).split "_").toList with
     | "t_bvrepeat_", [ws, is] =>
       match ws.toNat?, is.toNat? with
       | .some w, .some i => .some (.bvrepeat w i)
       | _,       _       => .none
     | _,             _        => .none
   | "t_bvzer" =>
-    match s.take 15, (s.drop 15).splitOn "_" with
+    match s.take 15, ((s.drop 15).split "_").toList with
     | "t_bvzeroExtend_", [ws, vs] =>
       match ws.toNat?, vs.toNat? with
       | .some w, .some v => .some (.bvzeroExtend w v)
       | _,       _       => .none
     | _,             _        => .none
   | "t_bvsig" =>
-    match s.take 15, (s.drop 15).splitOn "_" with
+    match s.take 15, ((s.drop 15).split "_").toList with
     | "t_bvsignExtend_", [ws, vs] =>
       match ws.toNat?, vs.toNat? with
       | .some w, .some v => .some (.bvsignExtend w v)
diff --git a/Auto/Translation/LamFOL2SMT.lean b/Auto/Translation/LamFOL2SMT.lean
index 0326f5f..4c5d17f 100644
--- a/Auto/Translation/LamFOL2SMT.lean
+++ b/Auto/Translation/LamFOL2SMT.lean
@@ -88,7 +88,7 @@ def SMTNamingInfo.exprToSuggestion (e : Expr) : MetaM String := do
     return toString (← PrettyPrinter.formatTerm ppSyntax)
 
 def SMTNamingInfo.suggestNameForSort (sni : SMTNamingInfo) (s : LamSort) := do
-  let suggestion := ((← go s).take 1).toLower
+  let suggestion := ((← go s).take 1).toString.toLower
   trace[auto.lamFOL2SMT.nameSuggestion] "`{suggestion}` for LamSort `{s}`"
   return suggestion
 where
diff --git a/lean-toolchain b/lean-toolchain
index e59446d..5249182 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.26.0
+leanprover/lean4:v4.27.0