Update Std/Data/List/Lemmas.lean

Update Std/Data/String/Lemmas.lean

Co-Authored-By: Kim Morrison <kim@tqft.net>

Std/Data/String/Lemmas.lean

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