feat(Data/Nat/Choose/Lucas): add choose_mul_mul and choose_pow_mul_pow_mul modular congruence lemmas (leanprover-community#35893)

Author: b-mehta

Mathlib/Data/Nat/Choose/Lucas.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.CharP.Lemmas
 public import Mathlib.Data.ZMod.Basic
 public import Mathlib.RingTheory.Polynomial.Basic
+meta import Mathlib.Tactic.GRewrite
 
 /-!
 # Lucas's theorem
@@ -31,7 +32,7 @@ open Nat Polynomial
 
 namespace Choose
 
-variable {n k p : ℕ} [Fact p.Prime]
+variable {n k a b p : ℕ} [Fact p.Prime]
 
 /-- For primes `p`, `choose n k` is congruent to `choose (n % p) (k % p) * choose (n / p) (k / p)`
 modulo `p`. Also see `choose_modEq_choose_mod_mul_choose_div_nat` for the version with `MOD`. -/
@@ -101,4 +102,34 @@ theorem choose_modEq_prod_range_choose_nat {a : ℕ} (ha₁ : n < p ^ a) (ha₂
 alias lucas_theorem := choose_modEq_prod_range_choose
 alias lucas_theorem_nat := choose_modEq_prod_range_choose_nat
 
+/-- For primes `p`, `choose (p * a) (p * b)` is congruent to `choose a b` modulo `p`.
+Also see `choose_mul_mul_modEq_choose_nat` for the version with `MOD`. -/
+theorem choose_mul_mul_modEq_choose :
+    choose (p * a) (p * b) ≡ choose a b [ZMOD p] := by
+  grw [choose_modEq_choose_mod_mul_choose_div]
+  simp [NeZero.pos, Int.ModEq.refl]
+
+/-- For primes `p`, `choose (p * a) (p * b)` is congruent to `choose a b` modulo `p`.
+Also see `choose_mul_mul_modEq_choose` for the version with `ZMOD`. -/
+theorem choose_mul_mul_modEq_choose_nat :
+    choose (p * a) (p * b) ≡ choose a b [MOD p] := by
+  rw [← Int.natCast_modEq_iff]
+  exact_mod_cast choose_mul_mul_modEq_choose
+
+/-- For primes `p`, `choose (p ^ k * a) (p ^ k * b)` is congruent to `choose a b` modulo `p`.
+Also see `choose_pow_mul_pow_mul_modEq_choose_nat` for the version with `MOD`. -/
+theorem choose_pow_mul_pow_mul_modEq_choose :
+    choose (p ^ k * a) (p ^ k * b) ≡ choose a b [ZMOD p] := by
+  induction k with
+  | zero => simp [Int.ModEq.refl]
+  | succ k ih =>
+    grw [Nat.pow_succ', mul_assoc, mul_assoc, choose_mul_mul_modEq_choose, ih]
+
+/-- For primes `p`, `choose (p ^ k * a) (p ^ k * b)` is congruent to `choose a b` modulo `p`.
+Also see `choose_pow_mul_pow_mul_modEq_choose` for the version with `ZMOD`. -/
+theorem choose_pow_mul_pow_mul_modEq_choose_nat :
+    choose (p ^ k * a) (p ^ k * b) ≡ choose a b [MOD p] := by
+  rw [← Int.natCast_modEq_iff]
+  exact_mod_cast choose_pow_mul_pow_mul_modEq_choose
+
 end Choose