chore: Rearrange arguments to Nat.multinomial_insert (#9562)

and a few other `multinomial` lemmas

Mathlib/Data/Nat/Choose/Multinomial.lean

@@ -58,21 +58,23 @@ theorem multinomial_nil : multinomial ∅ f = 1 := by
   rfl
 #align nat.multinomial_nil Nat.multinomial_nil
 
-lemma multinomial_cons (ha : a ∉ s) :
+variable {s f}
+
+lemma multinomial_cons (ha : a ∉ s) (f : α → ℕ) :
     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) :
+lemma multinomial_insert [DecidableEq α] (ha : a ∉ s) (f : α → ℕ) :
     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]
-lemma multinomial_singleton : multinomial {a} f = 1 := by rw [← cons_empty, multinomial_cons]; simp
+@[simp] lemma multinomial_singleton (a : α) (f : α → ℕ) : multinomial {a} f = 1 := by
+  rw [← cons_empty, multinomial_cons]; simp
 #align nat.multinomial_singleton Nat.multinomial_singleton
 
 @[simp]
@@ -106,7 +108,7 @@ theorem binomial_eq [DecidableEq α] (h : a ≠ b) :
 
 theorem binomial_eq_choose [DecidableEq α] (h : a ≠ b) :
     multinomial {a, b} f = (f a + f b).choose (f a) := by
-  simp [binomial_eq _ h, choose_eq_factorial_div_factorial (Nat.le_add_right _ _)]
+  simp [binomial_eq h, choose_eq_factorial_div_factorial (Nat.le_add_right _ _)]
 #align nat.binomial_eq_choose Nat.binomial_eq_choose
 
 theorem binomial_spec [DecidableEq α] (hab : a ≠ b) :
@@ -117,7 +119,7 @@ theorem binomial_spec [DecidableEq α] (hab : a ≠ b) :
 @[simp]
 theorem binomial_one [DecidableEq α] (h : a ≠ b) (h₁ : f a = 1) :
     multinomial {a, b} f = (f b).succ := by
-  simp [multinomial_insert_one {b} f (Finset.not_mem_singleton.mpr h) h₁]
+  simp [multinomial_insert_one (Finset.not_mem_singleton.mpr h) h₁]
 #align nat.binomial_one Nat.binomial_one
 
 theorem binomial_succ_succ [DecidableEq α] (h : a ≠ b) :
@@ -134,7 +136,7 @@ theorem binomial_succ_succ [DecidableEq α] (h : a ≠ b) :
 theorem succ_mul_binomial [DecidableEq α] (h : a ≠ b) :
     (f a + f b).succ * multinomial {a, b} f =
       (f a).succ * multinomial {a, b} (Function.update f a (f a).succ) := by
-  rw [binomial_eq_choose _ h, binomial_eq_choose _ h, mul_comm (f a).succ, Function.update_same,
+  rw [binomial_eq_choose h, binomial_eq_choose h, mul_comm (f a).succ, Function.update_same,
     Function.update_noteq (ne_comm.mp h)]
   rw [succ_mul_choose_eq (f a + f b) (f a), succ_add (f a) (f b)]
 #align nat.succ_mul_binomial Nat.succ_mul_binomial
@@ -179,11 +181,10 @@ theorem multinomial_update (a : α) (f : α →₀ ℕ) :
   simp only [multinomial_eq]
   classical
     by_cases h : a ∈ f.support
-    · rw [← Finset.insert_erase h, Nat.multinomial_insert _ f (Finset.not_mem_erase a _),
+    · rw [← Finset.insert_erase h, Nat.multinomial_insert (Finset.not_mem_erase a _),
         Finset.add_sum_erase _ f h, support_update_zero]
       congr 1
-      exact
-        Nat.multinomial_congr _ fun _ h => (Function.update_noteq (Finset.mem_erase.1 h).1 0 f).symm
+      exact Nat.multinomial_congr fun _ h ↦ (Function.update_noteq (mem_erase.1 h).1 0 f).symm
     rw [not_mem_support_iff] at h
     rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
 #align finsupp.multinomial_update Finsupp.multinomial_update