diff --git a/Std/Data/String/Lemmas.lean b/Std/Data/String/Lemmas.lean
index 3bede5e5c9..85fb0bdd3a 100644
--- a/Std/Data/String/Lemmas.lean
+++ b/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