merge bump/nightly-2025-11-17

Author: kim-em

Batteries/Data/String/Lemmas.lean

@@ -956,7 +956,8 @@ theorem get : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s → s.get ⟨utf8Len m
 theorem next : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s →
     s.next ⟨utf8Len m₁⟩ = ⟨utf8Len m₁ + c.utf8Size⟩
   | _, ⟨⟩ => by
-    simp only [Substring.Raw.next, utf8Len_append, utf8Len_cons, List.append_assoc, List.cons_append]
+    simp only [Substring.Raw.next, utf8Len_append, utf8Len_cons, List.append_assoc,
+      List.cons_append]
     rw [if_neg (mt Pos.Raw.ext_iff.1 ?a)]
     case a =>
       simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using

Batteries/Data/String/Matcher.lean

@@ -52,7 +52,8 @@ partial def Matcher.findAll (m : Matcher) (s : Substring.Raw) : Array Substring.
   loop s m.toMatcher #[]
 where
   /-- Accumulator loop for `String.Matcher.findAll` -/
-  loop (s : Substring.Raw) (am : Array.Matcher Char) (occs : Array Substring.Raw) : Array Substring.Raw :=
+  loop (s : Substring.Raw) (am : Array.Matcher Char) (occs : Array Substring.Raw) :
+      Array Substring.Raw :=
     match am.next? s with
     | none => occs
     | some (s, am) =>