Update Std/Data/String/Lemmas.lean

Co-authored-by: Kim Morrison <[email protected]>

Std/Data/String/Lemmas.lean

@@ -501,7 +501,7 @@ theorem join_eq (ss : List String) : join ss = ⟨(ss.map data).join⟩ := go ss
 
 @[simp] theorem comp_length_data : List.length ∘ String.data = String.length := rfl
 
-theorem length_join (l : List String) : (String.join l).length = Nat.sum (l.map String.length) := by
+theorem length_join (l : List String) : (String.join l).length = (l.map String.length).sum := by
   simp [length, List.length_join, List.map_map]
 
 theorem singleton_eq (c : Char) : singleton c = ⟨[c]⟩ := rfl