chore(number_theory/primorial): golf a proof (#12807)

Use a new lemma to golf a proof.

src/number_theory/primorial.lean

@@ -30,15 +30,10 @@ local notation x`#` := primorial x
 
 lemma primorial_succ {n : ℕ} (n_big : 1 < n) (r : n % 2 = 1) : (n + 1)# = n# :=
 begin
-  have not_prime : ¬nat.prime (n + 1),
-  { intros is_prime,
-    cases (prime.eq_two_or_odd is_prime) with _ n_even,
-    { linarith, },
-    { apply nat.zero_ne_one,
-      rwa [add_mod, r, nat.one_mod, ←two_mul, mul_one, nat.mod_self] at n_even, }, },
-  apply finset.prod_congr,
-  { rw [@range_succ (n + 1), filter_insert, if_neg not_prime], },
-  { exact λ _ _, rfl, },
+  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],
 end
 
 lemma dvd_choose_of_middling_prime (p : ℕ) (is_prime : nat.prime p) (m : ℕ)