chore: upstream List.length_flatMap

src/Init/Data/List/Count.lean

@@ -162,6 +162,10 @@ theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : List α)
 
 @[deprecated countP_flatten (since := "2024-10-14")] abbrev countP_join := @countP_flatten
 
+theorem countP_flatMap (p : β → Bool) (l : List α) (f : α → List β) :
+    countP p (l.flatMap f) = sum (map (countP p ∘ f) l) := by
+  rw [List.flatMap, countP_flatten, map_map]
+
 @[simp] theorem countP_reverse (l : List α) : countP p l.reverse = countP p l := by
   simp [countP_eq_length_filter, filter_reverse]
 
@@ -326,6 +330,9 @@ theorem count_filterMap {α} [BEq β] (b : β) (f : α → Option β) (l : List
   · simp
   · simp
 
+theorem count_flatMap {α} [BEq β] (l : List α) (f : α → List β) (x : β) :
+    count x (l.flatMap f) = sum (map (count x ∘ f) l) := countP_flatMap _ _ _
+
 theorem count_erase (a b : α) :
     ∀ l : List α, count a (l.erase b) = count a l - if b == a then 1 else 0
   | [] => by simp

src/Init/Data/List/Lemmas.lean

@@ -2213,6 +2213,11 @@ theorem flatMap_def (l : List α) (f : α → List β) : l.flatMap f = flatten (
 
 @[simp] theorem flatMap_id (l : List (List α)) : List.flatMap l id = l.flatten := by simp [flatMap_def]
 
+@[simp]
+theorem length_flatMap (l : List α) (f : α → List β) :
+    length (l.flatMap f) = sum (map (length ∘ f) l) := by
+  rw [List.flatMap, length_flatten, map_map]
+
 @[simp] theorem mem_flatMap {f : α → List β} {b} {l : List α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
   simp [flatMap_def, mem_flatten]
   exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩