@[simp]

theorem String.length_eq_zero_iff {s : String} : s.length = 0 ↔ s = ""

@[simp]

theorem String.length_map {f : Char → Char} {s : String} : (map f s).length = s.length

@[simp]

theorem String.length_join {l : List String} : (join l).length = (List.map length l).sum