From 95af9be74f8b9d98505d9900fe8f563a89e5e667 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 18 Sep 2024 17:04:01 +0000
Subject: [PATCH] feat: Composition.blocksFun_le (#16814)

---
 .../Algebra/Order/BigOperators/Group/List.lean   | 16 +++++++++++++++-
 .../Combinatorics/Enumerative/Composition.lean   |  6 ++++++
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Order/BigOperators/Group/List.lean b/Mathlib/Algebra/Order/BigOperators/Group/List.lean
index 7872ed429ca63..3d5a671d2a7f8 100644
--- a/Mathlib/Algebra/Order/BigOperators/Group/List.lean
+++ b/Mathlib/Algebra/Order/BigOperators/Group/List.lean
@@ -143,7 +143,8 @@ lemma one_lt_prod_of_one_lt [OrderedCommMonoid M] :
     · exact hl₁.2.1
     · exact hl₁.2.2 _ ‹_›
 
-@[to_additive]
+/-- See also `List.le_prod_of_mem`. -/
+@[to_additive "See also `List.le_sum_of_mem`."]
 lemma single_le_prod [OrderedCommMonoid M] {l : List M} (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) :
     ∀ x ∈ l, x ≤ l.prod := by
   induction l
@@ -174,5 +175,18 @@ variable [CanonicallyOrderedCommMonoid M] {l : List M}
     exact le_self_mul
   · simp [take_of_length_le h, take_of_length_le (le_trans h (Nat.le_succ _))]
 
+/-- See also `List.single_le_prod`. -/
+@[to_additive "See also `List.single_le_sum`."]
+theorem le_prod_of_mem {xs : List M} {x : M} (h₁ : x ∈ xs) : x ≤ xs.prod := by
+  induction xs with
+  | nil => simp at h₁
+  | cons y ys ih =>
+    simp only [mem_cons] at h₁
+    rcases h₁ with (rfl | h₁)
+    · simp
+    · specialize ih h₁
+      simp only [List.prod_cons]
+      exact le_mul_left ih
+
 end CanonicallyOrderedCommMonoid
 end List
diff --git a/Mathlib/Combinatorics/Enumerative/Composition.lean b/Mathlib/Combinatorics/Enumerative/Composition.lean
index a7e73aefb67e9..917e4a7e41dbc 100644
--- a/Mathlib/Combinatorics/Enumerative/Composition.lean
+++ b/Mathlib/Combinatorics/Enumerative/Composition.lean
@@ -168,6 +168,12 @@ theorem blocks_pos' (i : ℕ) (h : i < c.length) : 0 < c.blocks[i] :=
 theorem one_le_blocksFun (i : Fin c.length) : 1 ≤ c.blocksFun i :=
   c.one_le_blocks (c.blocksFun_mem_blocks i)
 
+theorem blocksFun_le {n} (c : Composition n) (i : Fin c.length) :
+    c.blocksFun i ≤ n := by
+  have := c.blocks_sum
+  have := List.le_sum_of_mem (c.blocksFun_mem_blocks i)
+  simp_all
+
 theorem length_le : c.length ≤ n := by
   conv_rhs => rw [← c.blocks_sum]
   exact length_le_sum_of_one_le _ fun i hi => c.one_le_blocks hi