refactor(number_theory/primorial): split the proof, golf it (#18238)

* Add `nat.prime.dvd_choose`, delete less general `dvd_choose_of_middling_prime`.
* Add `primorial_pos`, `primorial_add`, `primorial_add_dvd`, and `primorial_add_le`.
* Golf some proofs.

Here is a proof of `dvd_choose_of_middling_prime` based on `nat.prime.dvd_choose`:

```lean
open nat

lemma dvd_choose_of_middling_prime (p : ℕ) (is_prime : nat.prime p) (m : ℕ)
  (p_big : m + 1 < p) (p_small : p ≤ 2 * m + 1) : p ∣ choose (2 * m + 1) (m + 1) :=
is_prime.dvd_choose p_big (by simpa [two_mul] using p_big.le) p_small
```

Forward-ported in leanprover-community/mathlib4#1770

src/algebra/char_p/basic.lean

@@ -144,8 +144,7 @@ begin
   { intros b h1 h2,
     suffices : (p.choose b : R) = 0, { rw this, simp },
     rw char_p.cast_eq_zero_iff R p,
-    refine nat.prime.dvd_choose_self (pos_iff_ne_zero.mpr h2) _ (fact.out _),
-    rwa ← finset.mem_range },
+    exact nat.prime.dvd_choose_self (fact.out _) h2 (finset.mem_range.1 h1) },
   { intro h1,
     contrapose! h1,
     rw finset.mem_range,

src/data/nat/choose/dvd.lean

@@ -19,26 +19,23 @@ open_locale nat
 
 namespace prime
 
-lemma dvd_choose_add {p a b : ℕ} (hap : a < p) (hbp : b < p) (h : p ≤ a + b)
-  (hp : prime p) : p ∣ choose (a + b) a :=
-have h₁ : p ∣ (a + b)!, from hp.dvd_factorial.2 h,
-have h₂ : ¬p ∣ a!, from mt hp.dvd_factorial.1 (not_le_of_gt hap),
-have h₃ : ¬p ∣ b!, from mt hp.dvd_factorial.1 (not_le_of_gt hbp),
-by
-  rw [← choose_mul_factorial_mul_factorial (le.intro rfl), mul_assoc, hp.dvd_mul, hp.dvd_mul,
-      add_tsub_cancel_left a b] at h₁;
-  exact h₁.resolve_right (not_or_distrib.2 ⟨h₂, h₃⟩)
-
-lemma dvd_choose_self {p k : ℕ} (hk : 0 < k) (hkp : k < p) (hp : prime p) :
-  p ∣ choose p k :=
+lemma dvd_choose_add {p a b : ℕ} (hp : prime p) (hap : a < p) (hbp : b < p) (h : p ≤ a + b) :
+  p ∣ choose (a + b) a :=
 begin
-  have r : k + (p - k) = p,
-    by rw [← add_tsub_assoc_of_le (nat.le_of_lt hkp) k, add_tsub_cancel_left],
-  have e : p ∣ choose (k + (p - k)) k,
-    by exact dvd_choose_add hkp (nat.sub_lt (hk.trans hkp) hk) (by rw r) hp,
-  rwa r at e,
+  have h₁ : p ∣ (a + b)!, from hp.dvd_factorial.2 h,
+  rw [← add_choose_mul_factorial_mul_factorial, ← choose_symm_add, hp.dvd_mul, hp.dvd_mul,
+    hp.dvd_factorial, hp.dvd_factorial] at h₁,
+  exact (h₁.resolve_right hbp.not_le).resolve_right hap.not_le
 end
 
+lemma dvd_choose {p a b : ℕ} (hp : prime p) (ha : a < p) (hab : b - a < p) (h : p ≤ b) :
+  p ∣ choose b a :=
+have a + (b - a) = b := nat.add_sub_of_le (ha.le.trans h),
+this ▸ hp.dvd_choose_add ha hab (this.symm ▸ h)
+
+lemma dvd_choose_self {p k : ℕ} (hp : prime p) (hk : k ≠ 0) (hkp : k < p) : p ∣ choose p k :=
+hp.dvd_choose hkp (nat.sub_lt ((zero_le _).trans_lt hkp) hk.bot_lt) le_rfl
+
 end prime
 
 end nat

src/number_theory/primorial.lean

@@ -1,13 +1,13 @@
 /-
 Copyright (c) 2020 Patrick Stevens. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Patrick Stevens
+Authors: Patrick Stevens, Yury Kudryashov
 -/
 import algebra.big_operators.associated
 import data.nat.choose.sum
+import data.nat.choose.dvd
 import data.nat.parity
 import data.nat.prime
-import tactic.ring_exp
 
 /-!
 # Primorial
@@ -30,105 +30,54 @@ open_locale big_operators nat
 def primorial (n : ℕ) : ℕ := ∏ p in (filter nat.prime (range (n + 1))), p
 local notation x`#` := primorial x
 
-lemma primorial_succ {n : ℕ} (n_big : 1 < n) (r : n % 2 = 1) : (n + 1)# = n# :=
+lemma primorial_pos (n : ℕ) : 0 < n# :=
+prod_pos $ λ p hp, (mem_filter.1 hp).2.pos
+
+lemma primorial_succ {n : ℕ} (hn1 : n ≠ 1) (hn : odd n) : (n + 1)# = n# :=
 begin
   refine prod_congr _ (λ _ _, rfl),
-  rw [range_succ, filter_insert, if_neg (λ h, _)],
-  have two_dvd : 2 ∣ n + 1 := dvd_iff_mod_eq_zero.mpr (by rw [← mod_add_mod, r, mod_self]),
-  linarith [(h.dvd_iff_eq (nat.bit0_ne_one 1)).mp two_dvd],
+  rw [range_succ, filter_insert, if_neg (λ h, odd_iff_not_even.mp hn _)],
+  exact (h.even_sub_one $ mt succ.inj hn1)
 end
 
-lemma dvd_choose_of_middling_prime (p : ℕ) (is_prime : nat.prime p) (m : ℕ)
-  (p_big : m + 1 < p) (p_small : p ≤ 2 * m + 1) : p ∣ choose (2 * m + 1) (m + 1) :=
+lemma primorial_add (m n : ℕ) :
+  (m + n)# = m# * ∏ p in filter nat.prime (Ico (m + 1) (m + n + 1)), p :=
 begin
-  have m_size : m + 1 ≤ 2 * m + 1 := le_of_lt (lt_of_lt_of_le p_big p_small),
-  have s : ¬(p ∣ (m + 1)!),
-  { intros p_div_fact,
-    exact lt_le_antisymm p_big (is_prime.dvd_factorial.mp p_div_fact), },
-  have t : ¬(p ∣ (2 * m + 1 - (m + 1))!),
-  { intros p_div_fact,
-    refine lt_le_antisymm (lt_of_succ_lt p_big) _,
-    convert is_prime.dvd_factorial.mp p_div_fact,
-    rw [two_mul, add_assoc, nat.add_sub_cancel] },
-  have expanded :
-    choose (2 * m + 1) (m + 1) * (m + 1)! * (2 * m + 1 - (m + 1))! = (2 * m + 1)! :=
-    @choose_mul_factorial_mul_factorial (2 * m + 1) (m + 1) m_size,
-  have p_div_big_fact : p ∣ (2 * m + 1)! := (prime.dvd_factorial is_prime).mpr p_small,
-  rw [←expanded, mul_assoc] at p_div_big_fact,
-  obtain p_div_choose | p_div_facts : p ∣ choose (2 * m + 1) (m + 1) ∨ p ∣ _! * _! :=
-    (prime.dvd_mul is_prime).1 p_div_big_fact,
-  { exact p_div_choose, },
-  cases (prime.dvd_mul is_prime).1 p_div_facts,
-  exacts [(s h).elim, (t h).elim],
+  rw [primorial, primorial, ← Ico_zero_eq_range, ← prod_union, ← filter_union,
+    Ico_union_Ico_eq_Ico],
+  exacts [zero_le _, add_le_add_right (nat.le_add_right _ _) _,
+    disjoint_filter_filter $ Ico_disjoint_Ico_consecutive _ _ _]
 end
 
-lemma primorial_le_4_pow : ∀ (n : ℕ), n# ≤ 4 ^ n
-| 0 := le_rfl
-| 1 := le_of_inf_eq rfl
-| (n + 2) :=
-  match nat.mod_two_eq_zero_or_one (n + 1) with
-  | or.inl n_odd :=
-    match nat.even_iff.2 n_odd with
-    | ⟨m, twice_m⟩ :=
-      have recurse : m + 1 < n + 2 := by linarith,
-      begin
-        calc (n + 2)#
-            = ∏ i in filter nat.prime (range (2 * m + 2)), i : by simpa [two_mul, ←twice_m]
-        ... = ∏ i in filter nat.prime (finset.Ico (m + 2) (2 * m + 2) ∪ range (m + 2)), i :
-              begin
-                rw [range_eq_Ico, finset.union_comm, finset.Ico_union_Ico_eq_Ico],
-                { exact bot_le },
-                { simpa only [add_le_add_iff_right, two_mul] using nat.le_add_left m m },
-              end
-        ... = ∏ i in (filter nat.prime (finset.Ico (m + 2) (2 * m + 2))
-              ∪ (filter nat.prime (range (m + 2)))), i :
-              by rw filter_union
-        ... = (∏ i in filter nat.prime (finset.Ico (m + 2) (2 * m + 2)), i)
-              * (∏ i in filter nat.prime (range (m + 2)), i) :
-              begin
-                apply finset.prod_union,
-                have disj : disjoint (finset.Ico (m + 2) (2 * m + 2)) (range (m + 2)),
-                { simp only [finset.disjoint_left, and_imp, finset.mem_Ico, not_lt,
-                    finset.mem_range],
-                  intros _ pr _, exact pr, },
-                exact finset.disjoint_filter_filter disj,
-              end
-        ... ≤ (∏ i in filter nat.prime (finset.Ico (m + 2) (2 * m + 2)), i) * 4 ^ (m + 1) :
-              nat.mul_le_mul_left _ (primorial_le_4_pow (m + 1))
-        ... ≤ (choose (2 * m + 1) (m + 1)) * 4 ^ (m + 1) :
-              begin
-                have s : ∏ i in filter nat.prime (finset.Ico (m + 2) (2 * m + 2)),
-                  i ∣ choose (2 * m + 1) (m + 1),
-                { refine prod_primes_dvd  (choose (2 * m + 1) (m + 1)) _ _,
-                  { intros a, rw [finset.mem_filter, nat.prime_iff], apply and.right, },
-                  { intros a, rw finset.mem_filter,
-                    intros pr,
-                    rcases pr with ⟨ size, is_prime ⟩,
-                    simp only [finset.mem_Ico] at size,
-                    rcases size with ⟨ a_big , a_small ⟩,
-                    exact dvd_choose_of_middling_prime a is_prime m a_big
-                      (nat.lt_succ_iff.mp a_small), }, },
-                have r : ∏ i in filter nat.prime (finset.Ico (m + 2) (2 * m + 2)),
-                  i ≤ choose (2 * m + 1) (m + 1),
-                { refine @nat.le_of_dvd _ _ _ s,
-                  exact @choose_pos (2 * m + 1) (m + 1) (by linarith), },
-                exact nat.mul_le_mul_right _ r,
-              end
-        ... = (choose (2 * m + 1) m) * 4 ^ (m + 1) : by rw choose_symm_half m
-        ... ≤ 4 ^ m * 4 ^ (m + 1) : nat.mul_le_mul_right _ (choose_middle_le_pow m)
-        ... = 4 ^ (2 * m + 1) : by ring_exp
-        ... = 4 ^ (n + 2) : by rw [two_mul, ←twice_m],
-      end
-    end
-  | or.inr n_even :=
+lemma primorial_add_dvd {m n : ℕ} (h : n ≤ m) : (m + n)# ∣ m# * choose (m + n) m :=
+calc (m + n)# = m# * ∏ p in filter nat.prime (Ico (m + 1) (m + n + 1)), p :
+  primorial_add _ _
+... ∣ m# * choose (m + n) m :
+  mul_dvd_mul_left _ $ prod_primes_dvd _ (λ k hk, (mem_filter.1 hk).2.prime) $ λ p hp,
     begin
-      obtain one_lt_n | n_le_one : 1 < n + 1 ∨ n + 1 ≤ 1 := lt_or_le 1 (n + 1),
-      { rw primorial_succ one_lt_n n_even,
-        calc (n + 1)#
-              ≤ 4 ^ n.succ : primorial_le_4_pow (n + 1)
-          ... ≤ 4 ^ (n + 2) : pow_le_pow (by norm_num) (nat.le_succ _), },
-      { have n_zero : n = 0 := eq_bot_iff.2 (succ_le_succ_iff.1 n_le_one),
-        norm_num [n_zero, primorial, range_succ, prod_filter, nat.not_prime_zero, nat.prime_two] },
+      rw [mem_filter, mem_Ico] at hp,
+      exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1))
+        (nat.lt_succ_iff.1 hp.1.2)
     end
 
+lemma primorial_add_le {m n : ℕ} (h : n ≤ m) : (m + n)# ≤ m# * choose (m + n) m :=
+le_of_dvd (mul_pos (primorial_pos _) (choose_pos $ nat.le_add_right _ _)) (primorial_add_dvd h)
+
+lemma primorial_le_4_pow (n : ℕ) : n# ≤ 4 ^ n :=
+begin
+  induction n using nat.strong_induction_on with n ihn,
+  cases n, { refl },
+  rcases n.even_or_odd with (⟨m, rfl⟩ | ho),
+  { rcases m.eq_zero_or_pos with rfl | hm, { dec_trivial },
+    calc (m + m + 1)# = (m + 1 + m)# : by rw [add_right_comm]
+    ... ≤ (m + 1)# * choose (m + 1 + m) (m + 1) : primorial_add_le m.le_succ
+    ... = (m + 1)# * choose (2 * m + 1) m : by rw [choose_symm_add, two_mul, add_right_comm]
+    ... ≤ 4 ^ (m + 1) * 4 ^ m :
+      mul_le_mul' (ihn _ $ succ_lt_succ $ (lt_add_iff_pos_left _).2 hm) (choose_middle_le_pow _)
+    ... ≤ 4 ^ (m + m + 1) : by rw [← pow_add, add_right_comm] },
+  { rcases decidable.eq_or_ne n 1 with rfl | hn,
+    { dec_trivial },
+    { calc (n + 1)# = n# : primorial_succ hn ho
+      ... ≤ 4 ^ n : ihn n n.lt_succ_self
+      ... ≤ 4 ^ (n + 1) : pow_le_pow_of_le_right  four_pos n.le_succ } }
 end

src/ring_theory/polynomial/eisenstein/is_integral.lean

@@ -54,10 +54,9 @@ begin
       rw [lcoeff_apply, ← C_eq_nat_cast, C_mul_X_pow_eq_monomial, coeff_monomial] },
     rw [nat_degree_comp, show (X + 1 : ℤ[X]) = X + C 1, by simp, nat_degree_X_add_C, mul_one,
       nat_degree_cyclotomic, nat.totient_prime hp.out] at hi,
-    simp only [lt_of_lt_of_le hi (nat.sub_le _ _), sum_ite_eq', mem_range,
-      if_true, ideal.submodule_span_eq, ideal.mem_span_singleton],
-    exact int.coe_nat_dvd.2
-      (nat.prime.dvd_choose_self (nat.succ_pos i) (lt_tsub_iff_right.1 hi) hp.out) },
+    simp only [hi.trans_le (nat.sub_le _ _), sum_ite_eq', mem_range, if_true,
+      ideal.submodule_span_eq, ideal.mem_span_singleton, int.coe_nat_dvd],
+    exact hp.out.dvd_choose_self i.succ_ne_zero (lt_tsub_iff_right.1 hi) },
   { rw [coeff_zero_eq_eval_zero, eval_comp, cyclotomic_prime, eval_add, eval_X,
       eval_one, zero_add, eval_geom_sum, one_geom_sum,
       ideal.submodule_span_eq, ideal.span_singleton_pow, ideal.mem_span_singleton],