From c96137c8d1a9caa10dade0b89200f2fe7112852d Mon Sep 17 00:00:00 2001 From: tjf801 <47402907+tjf801@users.noreply.github.com> Date: Tue, 30 Apr 2024 21:54:49 -0400 Subject: [PATCH] Update Std/Data/String/Lemmas.lean Co-authored-by: Kim Morrison --- Std/Data/String/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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