refactor(data/nat/choose): reduce assumptions on lemmas (#8508)

- rename `nat.choose_eq_factorial_div_factorial'` to `nat.cast_choose`
- change the cast from `ℚ` to any `char_zero` field
- get rid of the cast in `nat.choose_mul`. Generalization ensues.

src/data/nat/choose/basic.lean

@@ -108,6 +108,27 @@ begin
   { simp [hk₁, mul_comm, choose, nat.sub_self] }
 end
 
+lemma choose_mul {n k s : ℕ} (hkn : k ≤ n) (hsk : s ≤ k) :
+  n.choose k * k.choose s = n.choose s * (n - s).choose (k - s) :=
+begin
+  have h : 0 < (n - k)! * (k - s)! * s! :=
+    mul_pos (mul_pos (factorial_pos _) (factorial_pos _)) (factorial_pos _),
+  refine eq_of_mul_eq_mul_right h _,
+  calc
+    n.choose k * k.choose s * ((n - k)! * (k - s)! * s!)
+        = n.choose k * (k.choose s * s! * (k - s)!) * (n - k)!
+        : by rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc _ s!, mul_assoc, mul_comm (n - k)!,
+              mul_comm s!]
+    ... = n!
+        : by rw [choose_mul_factorial_mul_factorial hsk, choose_mul_factorial_mul_factorial hkn]
+    ... = n.choose s * s! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!)
+        : by rw [choose_mul_factorial_mul_factorial (nat.sub_le_sub_right hkn _),
+              choose_mul_factorial_mul_factorial (hsk.trans hkn)]
+    ... = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s!)
+        : by rw [sub_sub_sub_cancel_right hsk, mul_assoc, mul_left_comm s!, mul_assoc,
+              mul_comm (k - s)!, mul_comm s!, mul_right_comm, ←mul_assoc]
+end
+
 theorem choose_eq_factorial_div_factorial {n k : ℕ} (hk : k ≤ n) :
   choose n k = n! / (k! * (n - k)!) :=
 begin

src/data/nat/choose/dvd.lean

@@ -5,7 +5,7 @@ Authors: Chris Hughes, Patrick Stevens
 -/
 import data.nat.choose.basic
 import data.nat.prime
-import data.rat.floor
+
 /-!
 # Divisibility properties of binomial coefficients
 -/
@@ -38,22 +38,14 @@ end
 
 end prime
 
-lemma choose_eq_factorial_div_factorial' {a b : ℕ}
-  (hab : a ≤ b) : (b.choose a : ℚ) = b! / (a! * (b - a)!) :=
-begin
-  field_simp [mul_ne_zero, factorial_ne_zero], norm_cast,
-  rw ← choose_mul_factorial_mul_factorial hab, ring,
-end
-
-lemma choose_mul {n k s : ℕ} (hn : k ≤ n) (hs : s ≤ k) :
-  (n.choose k : ℚ) * k.choose s = n.choose s * (n - s).choose (k - s) :=
+lemma cast_choose {α : Type*} [field α] [char_zero α] {a b : ℕ} (hab : a ≤ b) :
+  (b.choose a : α) = b! / (a! * (b - a)!) :=
 begin
-  rw [choose_eq_factorial_div_factorial' hn, choose_eq_factorial_div_factorial' hs,
-      choose_eq_factorial_div_factorial' (le_trans hs hn), choose_eq_factorial_div_factorial' ],
-  swap,
-  { exact nat.sub_le_sub_right hn s, },
-  { field_simp [mul_ne_zero, factorial_ne_zero],
-    rw sub_sub_sub_cancel_right hs, ring, },
+  rw [eq_comm, div_eq_iff],
+  norm_cast,
+  rw [←mul_assoc, choose_mul_factorial_mul_factorial hab],
+  { exact mul_ne_zero (nat.cast_ne_zero.2 $ factorial_ne_zero _)
+    (nat.cast_ne_zero.2 $ factorial_ne_zero _) }
 end
 
 end nat

src/number_theory/bernoulli_polynomials.lean

@@ -100,9 +100,9 @@ begin
   simp_rw [polynomial.smul_monomial, mul_comm (bernoulli _) _, smul_eq_mul, ←mul_assoc],
   conv_lhs { apply_congr, skip, conv
     { apply_congr, skip,
-      rw [choose_mul ((nat.le_sub_left_iff_add_le (mem_range_le H)).1 (mem_range_le H_1))
-        (le.intro rfl), add_comm x x_1, nat.add_sub_cancel, mul_assoc, mul_comm, ←smul_eq_mul,
-        ←polynomial.smul_monomial], },
+      rw [← nat.cast_mul, choose_mul ((nat.le_sub_left_iff_add_le $ mem_range_le H).1
+        $ mem_range_le H_1) (le.intro rfl), nat.cast_mul, add_comm x x_1, nat.add_sub_cancel,
+        mul_assoc, mul_comm, ←smul_eq_mul, ←polynomial.smul_monomial] },
     rw [←sum_smul], },
   rw [sum_range_succ_comm],
   simp only [add_right_eq_self, cast_succ, mul_one, cast_one, cast_add, nat.add_sub_cancel_left,
@@ -164,9 +164,8 @@ begin
   -- The rest is just trivialities, hampered by the fact that we're coercing
   -- factorials and binomial coefficients between ℕ and ℚ and A.
   intros i hi,
-  -- NB prime.choose_eq_factorial_div_factorial' is in the wrong namespace
   -- deal with coefficients of e^X-1
-  simp only [choose_eq_factorial_div_factorial' (mem_range_le hi), coeff_mk,
+  simp only [nat.cast_choose (mem_range_le hi), coeff_mk,
     if_neg (mem_range_sub_ne_zero hi), one_div, alg_hom.map_smul, coeff_one, units.coe_mk,
     coeff_exp, sub_zero, linear_map.map_sub, algebra.smul_mul_assoc, algebra.smul_def,
     mul_right_comm _ ((aeval t) _), ←mul_assoc, ← ring_hom.map_mul, succ_eq_add_one],