chore(Data/Nat/Choose/Multinomial): Golf (#9534)

and `n ! ≤ n ^ n`

From LeanAPAP

Mathlib/Data/Nat/Choose/Multinomial.lean

@@ -27,10 +27,8 @@ This file defines the multinomial coefficient and several small lemma's for mani
 
 -/
 
-
-open BigOperators Nat
-
-open BigOperators
+open Finset
+open scoped BigOperators Nat
 
 namespace Nat
 
@@ -60,9 +58,21 @@ theorem multinomial_nil : multinomial ∅ f = 1 := by
   rfl
 #align nat.multinomial_nil Nat.multinomial_nil
 
+lemma multinomial_cons (ha : a ∉ s) :
+    multinomial (s.cons a ha) f = (f a + ∑ i in s, f i).choose (f a) * multinomial s f := by
+  rw [multinomial, Nat.div_eq_iff_eq_mul_left _ (prod_factorial_dvd_factorial_sum _ _), prod_cons,
+    multinomial, mul_assoc, mul_left_comm _ (f a)!,
+    Nat.div_mul_cancel (prod_factorial_dvd_factorial_sum _ _), ← mul_assoc, Nat.choose_symm_add,
+    Nat.add_choose_mul_factorial_mul_factorial, Finset.sum_cons]
+  exact prod_pos fun i _ ↦ by positivity
+
+lemma multinomial_insert [DecidableEq α] (ha : a ∉ s) :
+    multinomial (insert a s) f = (f a + ∑ i in s, f i).choose (f a) * multinomial s f := by
+  rw [← cons_eq_insert _ _ ha, multinomial_cons]
+#align nat.multinomial_insert Nat.multinomial_insert
+
 @[simp]
-theorem multinomial_singleton : multinomial {a} f = 1 := by
-  simp [multinomial, Nat.div_self (factorial_pos (f a))]
+lemma multinomial_singleton : multinomial {a} f = 1 := by rw [← cons_empty, multinomial_cons]; simp
 #align nat.multinomial_singleton Nat.multinomial_singleton
 
 @[simp]
@@ -74,17 +84,6 @@ theorem multinomial_insert_one [DecidableEq α] (h : a ∉ s) (h₁ : f a = 1) :
   rw [Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _)]
 #align nat.multinomial_insert_one Nat.multinomial_insert_one
 
-theorem multinomial_insert [DecidableEq α] (h : a ∉ s) :
-    multinomial (insert a s) f = (f a + s.sum f).choose (f a) * multinomial s f := by
-  rw [choose_eq_factorial_div_factorial (le.intro rfl)]
-  simp only [multinomial, Nat.add_sub_cancel_left, Finset.sum_insert h, Finset.prod_insert h,
-    Function.comp_apply]
-  rw [div_mul_div_comm ((f a).factorial_mul_factorial_dvd_factorial_add (s.sum f))
-      (prod_factorial_dvd_factorial_sum _ _),
-    mul_comm (f a)! (s.sum f)!, mul_assoc, mul_comm _ (s.sum f)!,
-    Nat.mul_div_mul_left _ _ (factorial_pos _)]
-#align nat.multinomial_insert Nat.multinomial_insert
-
 theorem multinomial_congr {f g : α → ℕ} (h : ∀ a ∈ s, f a = g a) :
     multinomial s f = multinomial s g := by
   simp only [multinomial]; congr 1
@@ -249,7 +248,7 @@ theorem sum_pow_of_commute [Semiring R] (x : α → R)
       convert @Nat.cast_one R _
     · rw [_root_.pow_succ, zero_mul]
       -- Porting note : Lean cannot infer this instance by itself
-      haveI : IsEmpty (Finset.sym (∅ : Finset α) (succ n)) := Finset.instIsEmpty
+      haveI : IsEmpty (Finset.sym (∅ : Finset α) n.succ) := Finset.instIsEmpty
       apply (Fintype.sum_empty _).symm
   intro n; specialize ih (hc.mono <| s.subset_insert a)
   rw [sum_insert ha, (Commute.sum_right s _ _ _).add_pow, sum_range]; swap

Mathlib/Data/Nat/Factorial/Basic.lean

@@ -207,6 +207,14 @@ theorem factorial_mul_pow_sub_le_factorial {n m : ℕ} (hnm : n ≤ m) : n ! * n
     _ ≤ _ := by simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)
 #align nat.factorial_mul_pow_sub_le_factorial Nat.factorial_mul_pow_sub_le_factorial
 
+lemma factorial_le_pow : ∀ n, n ! ≤ n ^ n
+  | 0 => le_rfl
+  | n + 1 =>
+    calc
+      _ ≤ (n + 1) * n ^ n := mul_le_mul_left' n.factorial_le_pow _
+      _ ≤ (n + 1) * (n + 1) ^ n := mul_le_mul_left' (Nat.pow_le_pow_left n.le_succ _) _
+      _ = _ := by rw [pow_succ']
+
 end Factorial
 
 /-! ### Ascending and descending factorials -/