From f09da0af9240ea856f4dd300be5141249bb9cf55 Mon Sep 17 00:00:00 2001
From: tjf801 <47402907+tjf801@users.noreply.github.com>
Date: Fri, 3 May 2024 00:53:22 -0400
Subject: [PATCH 1/2] Add String.length_join and List.length_join

---
 Std/Data/List/Lemmas.lean   | 4 ++++
 Std/Data/String/Lemmas.lean | 5 +++++
 2 files changed, 9 insertions(+)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 45a56ba558..d9950b4e79 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -5,6 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 import Std.Control.ForInStep.Lemmas
 import Std.Data.List.Basic
+import Std.Data.Nat
 import Std.Tactic.Init
 import Std.Tactic.Alias
 
@@ -365,6 +366,9 @@ 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
+  induction l <;> simp [*]
+
 /-! ### bind -/
 
 theorem mem_bind {f : α → List β} {b} {l : List α} : b ∈ l.bind f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
diff --git a/Std/Data/String/Lemmas.lean b/Std/Data/String/Lemmas.lean
index 28f9c76ad4..a3eb3ff513 100644
--- a/Std/Data/String/Lemmas.lean
+++ b/Std/Data/String/Lemmas.lean
@@ -516,6 +516,11 @@ 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 length_data (s : String) : s.data.length = s.length := rfl
+
+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
 
 @[simp] theorem data_singleton (c : Char) : (singleton c).data = [c] := rfl

From bd9d0c3d9532e4090c131ddfff9991991ebff50a Mon Sep 17 00:00:00 2001
From: tjf801 <47402907+tjf801@users.noreply.github.com>
Date: Fri, 3 May 2024 07:44:15 -0400
Subject: [PATCH 2/2] fix import

---
 Std/Data/List/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index d9950b4e79..47302b7cc1 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -5,7 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 import Std.Control.ForInStep.Lemmas
 import Std.Data.List.Basic
-import Std.Data.Nat
+import Std.Data.Nat.Lemmas
 import Std.Tactic.Init
 import Std.Tactic.Alias