feat: Composition.blocksFun_le (#16814)

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

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