Update Std/Data/List/Lemmas.lean

Co-authored-by: Kim Morrison <kim@tqft.net>

Std/Data/List/Lemmas.lean

@@ -365,7 +365,7 @@ theorem exists_of_mem_join : a ∈ join L → ∃ l, l ∈ L ∧ a ∈ l := mem_
 
 theorem mem_join_of_mem (lL : l ∈ L) (al : a ∈ l) : a ∈ join L := mem_join.2 ⟨l, lL, al⟩
 
-theorem length_join (l : List (List α)) : (join l).length = Nat.sum (l.map length) := by
+theorem length_join (l : List (List α)) : (join l).length = (l.map length).sum := by
   induction l <;> simp [*]
 
 /-! ### bind -/