Update Mathlib/Data/Nat/Factorial/BigOperators.lean

Co-authored-by: Thomas Browning <[email protected]>

Mathlib/Data/Nat/Factorial/BigOperators.lean

@@ -52,25 +52,13 @@ private lemma factorial_coe_dvd_prod_of_nonneg (k : ℕ) (n : ℤ) (hn : 0 ≤ n
 
 /-- `k!` divides the product of any `k` successive integers. -/
 lemma factorial_coe_dvd_prod (k : ℕ) (n : ℤ) : (k ! : ℤ) ∣ ∏ i ∈ range k, (n + i) := by
-  by_cases hn : n < 0
-  · by_cases hnk : 0 < n + k
-    · have : ∏ i ∈ range k, (n + ↑i) = 0 := prod_eq_zero_iff.mpr <| by
-        use n.natAbs
-        simp [abs_of_nonpos, hn.le, ← Int.ofNat_lt, hnk, neg_lt_iff_pos_add, add_comm]
-      rw [this]
-      exact (k ! : ℤ).dvd_zero
-    · have prod_eq : ∏ x ∈ range k, |n + ↑x| = ∏ x ∈ range k, -(n + ↑x) := by
-        refine prod_congr rfl fun _ hx ↦ ?_
-        rw [mem_range] at hx
-        rw [abs_of_neg]
-        linarith
-      rw [← dvd_abs, abs_prod, prod_eq, ← prod_range_reflect]
-      simp_rw [neg_add_rev, add_comm]
-      rw [show ∏ j ∈ range k, (-n + -↑(k - 1 - j)) = ∏ j ∈ range k, (-n + -↑(k - 1) + j) from ?_]
-      · exact factorial_coe_dvd_prod_of_nonneg k (-n + -↑(k - 1)) (by omega)
-      · refine prod_congr rfl fun _ ↦ ?_
-        rw [mem_range]
-        omega
-  · exact factorial_coe_dvd_prod_of_nonneg k n <| not_lt.mp hn
+  rw [Int.dvd_iff_emod_eq_zero, Finset.prod_int_mod]
+  simp_rw [← Int.emod_add_emod n]
+  rw [← Finset.prod_int_mod, ← Int.dvd_iff_emod_eq_zero]
+  have hn : 0 ≤ n % k ! := Int.emod_nonneg n <| Int.natCast_ne_zero.mpr k.factorial_ne_zero
+  obtain ⟨x, hx⟩ := Int.eq_ofNat_of_zero_le hn
+  have hdivk := x.factorial_dvd_ascFactorial k
+  zify [x.ascFactorial_eq_prod_range k] at hdivk
+  rwa [hx]
 
 end Nat