refactor(data/nat/prime): redefine nat.prime as irreducible (#11031)

archive/100-theorems-list/70_perfect_numbers.lean

@@ -53,8 +53,8 @@ end
 lemma ne_zero_of_prime_mersenne (k : ℕ) (pr : (mersenne (k + 1)).prime) :
   k ≠ 0 :=
 begin
-  rintro rfl,
-  simpa [mersenne, not_prime_one] using pr,
+  intro H,
+  simpa [H, mersenne, not_prime_one] using pr,
 end
 
 theorem even_two_pow_mul_mersenne_of_prime (k : ℕ) (pr : (mersenne (k + 1)).prime) :

archive/imo/imo1969_q1.lean

@@ -19,7 +19,7 @@ open int nat
 
 /-- `good_nats` is the set of natural numbers satisfying the condition in the problem
 statement, namely the `a : ℕ` such that `n^4 + a` is not prime for any `n : ℕ`. -/
-def good_nats : set ℕ := {a : ℕ | ∀ n : ℕ, ¬ prime (n^4 + a)}
+def good_nats : set ℕ := {a : ℕ | ∀ n : ℕ, ¬ nat.prime (n^4 + a)}
 
 /-!
 The key to the solution is that you can factor $z$ into the product of two polynomials,
@@ -43,11 +43,11 @@ lemma int_large {m : ℤ} (h : 1 < m) : 1 < m.nat_abs :=
 by exact_mod_cast lt_of_lt_of_le h le_nat_abs
 
 lemma not_prime_of_int_mul' {m n : ℤ} {c : ℕ}
-  (hm : 1 < m) (hn : 1 < n) (hc : m*n = (c : ℤ)) : ¬ prime c :=
+  (hm : 1 < m) (hn : 1 < n) (hc : m*n = (c : ℤ)) : ¬ nat.prime c :=
 not_prime_of_int_mul (int_large hm) (int_large hn) hc
 
 /-- Every natural number of the form `n^4 + 4*m^4` is not prime. -/
-lemma polynomial_not_prime {m : ℕ} (h1 : 1 < m) (n : ℕ) : ¬ prime (n^4 + 4*m^4) :=
+lemma polynomial_not_prime {m : ℕ} (h1 : 1 < m) (n : ℕ) : ¬ nat.prime (n^4 + 4*m^4) :=
 have h2 : 1 < (m : ℤ), from coe_nat_lt.mpr h1,
 begin
   refine not_prime_of_int_mul' (left_factor_large (n : ℤ) h2) (right_factor_large (n : ℤ) h2) _,
@@ -69,5 +69,5 @@ lemma a_choice_strict_mono : strict_mono a_choice :=
 
 /-- We conclude by using the fact that `a_choice` is an injective function from the natural numbers
 to the set `good_nats`. -/
-theorem imo1969_q1 : set.infinite {a : ℕ | ∀ n : ℕ, ¬ prime (n^4 + a)} :=
+theorem imo1969_q1 : set.infinite {a : ℕ | ∀ n : ℕ, ¬ nat.prime (n^4 + a)} :=
 set.infinite_of_injective_forall_mem a_choice_strict_mono.injective a_choice_good

src/algebra/associated.lean

@@ -135,6 +135,9 @@ lemma irreducible_iff [monoid α] {p : α} :
 @[simp] theorem not_irreducible_one [monoid α] : ¬ irreducible (1 : α) :=
 by simp [irreducible_iff]
 
+theorem irreducible.ne_one [monoid α] : ∀ {p:α}, irreducible p → p ≠ 1
+| _ hp rfl := not_irreducible_one hp
+
 @[simp] theorem not_irreducible_zero [monoid_with_zero α] : ¬ irreducible (0 : α)
 | ⟨hn0, h⟩ := have is_unit (0:α) ∨ is_unit (0:α), from h 0 0 ((mul_zero 0).symm),
   this.elim hn0 hn0

src/algebra/char_p/basic.lean

@@ -349,7 +349,7 @@ section no_zero_divisors
 variable [no_zero_divisors R]
 
 theorem char_is_prime_of_two_le (p : ℕ) [hc : char_p R p] (hp : 2 ≤ p) : nat.prime p :=
-suffices ∀d ∣ p, d = 1 ∨ d = p, from ⟨hp, this⟩,
+suffices ∀d ∣ p, d = 1 ∨ d = p, from nat.prime_def_lt''.mpr ⟨hp, this⟩,
 assume (d : ℕ) (hdvd : ∃ e, p = d * e),
 let ⟨e, hmul⟩ := hdvd in
 have (p : R) = 0, from (cast_eq_zero_iff R p p).mpr (dvd_refl p),

src/data/int/nat_prime.lean

@@ -14,7 +14,7 @@ open nat
 namespace int
 
 lemma not_prime_of_int_mul {a b : ℤ} {c : ℕ}
-  (ha : 1 < a.nat_abs) (hb : 1 < b.nat_abs) (hc : a*b = (c : ℤ)) : ¬ prime c :=
+  (ha : 1 < a.nat_abs) (hb : 1 < b.nat_abs) (hc : a*b = (c : ℤ)) : ¬ nat.prime c :=
 not_prime_mul' (nat_abs_mul_nat_abs_eq hc) ha hb
 
 end int

src/data/nat/prime.lean

@@ -8,6 +8,7 @@ import data.nat.gcd
 import data.nat.sqrt
 import tactic.norm_num
 import tactic.wlog
+import algebra.associated
 
 /-!
 # Prime numbers
@@ -33,18 +34,61 @@ namespace nat
 /-- `prime p` means that `p` is a prime number, that is, a natural number
   at least 2 whose only divisors are `p` and `1`. -/
 @[pp_nodot]
-def prime (p : ℕ) := 2 ≤ p ∧ ∀ m ∣ p, m = 1 ∨ m = p
+def prime (p : ℕ) := _root_.irreducible p
 
-theorem prime.two_le {p : ℕ} : prime p → 2 ≤ p := and.left
+theorem not_prime_zero : ¬ prime 0
+| h := h.ne_zero rfl
+
+theorem not_prime_one : ¬ prime 1
+| h := h.ne_one rfl
+
+theorem prime.ne_zero {n : ℕ} (h : prime n) : n ≠ 0 := irreducible.ne_zero h
+
+theorem prime.pos {p : ℕ} (pp : prime p) : 0 < p := nat.pos_of_ne_zero pp.ne_zero
+
+theorem prime.two_le : ∀ {p : ℕ}, prime p → 2 ≤ p
+| 0 h := (not_prime_zero h).elim
+| 1 h := (not_prime_one h).elim
+| (n+2) _ := le_add_self
 
 theorem prime.one_lt {p : ℕ} : prime p → 1 < p := prime.two_le
 
 instance prime.one_lt' (p : ℕ) [hp : _root_.fact p.prime] : _root_.fact (1 < p) := ⟨hp.1.one_lt⟩
 
 lemma prime.ne_one {p : ℕ} (hp : p.prime) : p ≠ 1 :=
-ne.symm $ ne_of_lt hp.one_lt
+hp.one_lt.ne'
+
+lemma two_le_iff (n : ℕ) : 2 ≤ n ↔ n ≠ 0 ∧ ¬is_unit n :=
+begin
+  rw nat.is_unit_iff,
+  rcases n with _|_|m; norm_num [one_lt_succ_succ, succ_le_iff]
+end
+
+lemma prime.eq_one_or_self_of_dvd {p : ℕ} (pp : p.prime) (m : ℕ) (hm : m ∣ p) : m = 1 ∨ m = p :=
+begin
+  obtain ⟨n, hn⟩ := hm,
+  have := pp.is_unit_or_is_unit hn,
+  rw [nat.is_unit_iff, nat.is_unit_iff] at this,
+  apply or.imp_right _ this,
+  rintro rfl,
+  rw [hn, mul_one]
+end
+
+theorem prime_def_lt'' {p : ℕ} : prime p ↔ 2 ≤ p ∧ ∀ m ∣ p, m = 1 ∨ m = p :=
+begin
+  refine ⟨λ h, ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, λ h, _⟩,
+  have h1 := one_lt_two.trans_le h.1,
+  refine ⟨mt nat.is_unit_iff.mp h1.ne', λ a b hab, _⟩,
+  simp only [nat.is_unit_iff],
+  apply or.imp_right _ (h.2 a _),
+  { rintro rfl,
+    rw [←nat.mul_right_inj (pos_of_gt h1), ←hab, mul_one] },
+  { rw hab,
+    exact dvd_mul_right _ _ }
+end
 
 theorem prime_def_lt {p : ℕ} : prime p ↔ 2 ≤ p ∧ ∀ m < p, m ∣ p → m = 1 :=
+prime_def_lt''.trans $
 and_congr_right $ λ p2, forall_congr $ λ m,
 ⟨λ h l d, (h d).resolve_right (ne_of_lt l),
  λ h d, (le_of_dvd (le_of_succ_le p2) d).lt_or_eq_dec.imp_left (λ l, h l d)⟩
@@ -98,16 +142,6 @@ local attribute [instance]
 def decidable_prime_1 (p : ℕ) : decidable (prime p) :=
 decidable_of_iff' _ prime_def_lt'
 
-lemma prime.ne_zero {n : ℕ} (h : prime n) : n ≠ 0 :=
-by { rintro rfl, revert h, dec_trivial }
-
-theorem prime.pos {p : ℕ} (pp : prime p) : 0 < p :=
-lt_of_succ_lt pp.one_lt
-
-theorem not_prime_zero : ¬ prime 0 := by simp [prime]
-
-theorem not_prime_one : ¬ prime 1 := by simp [prime]
-
 theorem prime_two : prime 2 := dec_trivial
 
 end
@@ -119,7 +153,7 @@ theorem succ_pred_prime {p : ℕ} (pp : prime p) : succ (pred p) = p :=
 succ_pred_eq_of_pos pp.pos
 
 theorem dvd_prime {p m : ℕ} (pp : prime p) : m ∣ p ↔ m = 1 ∨ m = p :=
-⟨λ d, pp.2 m d, λ h, h.elim (λ e, e.symm ▸ one_dvd _) (λ e, e.symm ▸ dvd_rfl)⟩
+⟨λ d, pp.eq_one_or_self_of_dvd m d, λ h, h.elim (λ e, e.symm ▸ one_dvd _) (λ e, e.symm ▸ dvd_rfl)⟩
 
 theorem dvd_prime_two_le {p m : ℕ} (pp : prime p) (H : 2 ≤ m) : m ∣ p ↔ m = p :=
 (dvd_prime pp).trans $ or_iff_right_of_imp $ not.elim $ ne_of_gt H
@@ -147,7 +181,8 @@ nat.lt_add_of_pos_right dec_trivial
 /-- If `n < k * k`, then `min_fac_aux n k = n`, if `k | n`, then `min_fac_aux n k = k`.
   Otherwise, `min_fac_aux n k = min_fac_aux n (k+2)` using well-founded recursion.
   If `n` is odd and `1 < n`, then then `min_fac_aux n 3` is the smallest prime factor of `n`. -/
-def min_fac_aux (n : ℕ) : ℕ → ℕ | k :=
+def min_fac_aux (n : ℕ) : ℕ → ℕ
+| k :=
 if h : n < k * k then n else
 if k ∣ n then k else
 have _, from min_fac_lemma n k h,
@@ -351,7 +386,7 @@ have np : n ≤ p, from le_of_not_ge $ λ h,
 
 lemma prime.eq_two_or_odd {p : ℕ} (hp : prime p) : p = 2 ∨ p % 2 = 1 :=
 p.mod_two_eq_zero_or_one.imp_left
-  (λ h, ((hp.2 2 (dvd_of_mod_eq_zero h)).resolve_left dec_trivial).symm)
+  (λ h, ((hp.eq_one_or_self_of_dvd 2 (dvd_of_mod_eq_zero h)).resolve_left dec_trivial).symm)
 
 theorem coprime_of_dvd {m n : ℕ} (H : ∀ k, prime k → k ∣ m → ¬ k ∣ n) : coprime m n :=
 begin
@@ -408,7 +443,7 @@ lemma prod_factors : ∀ {n}, 0 < n → list.prod (factors n) = n
 
 lemma factors_prime {p : ℕ} (hp : nat.prime p) : p.factors = [p] :=
 begin
-  have : p = (p - 2) + 2 := (tsub_eq_iff_eq_add_of_le hp.1).mp rfl,
+  have : p = (p - 2) + 2 := (tsub_eq_iff_eq_add_of_le hp.two_le).mp rfl,
   rw [this, nat.factors],
   simp only [eq.symm this],
   have : nat.min_fac p = p := (nat.prime_def_min_fac.mp hp).2,
@@ -539,7 +574,7 @@ lemma prime.pow_dvd_of_dvd_mul_left {p n a b : ℕ} (hp : p.prime) (h : p ^ n 
 by rw [mul_comm] at h; exact hp.pow_dvd_of_dvd_mul_right h hpb
 
 lemma prime.pow_not_prime {x n : ℕ} (hn : 2 ≤ n) : ¬ (x ^ n).prime :=
-λ hp, (hp.2 x $ dvd_trans ⟨x, sq _⟩ (pow_dvd_pow _ hn)).elim
+λ hp, (hp.eq_one_or_self_of_dvd x $ dvd_trans ⟨x, sq _⟩ (pow_dvd_pow _ hn)).elim
   (λ hx1, hp.ne_one $ hx1.symm ▸ one_pow _)
   (λ hxn, lt_irrefl x $ calc x = x ^ 1 : (pow_one _).symm
      ... < x ^ n : nat.pow_right_strict_mono (hxn.symm ▸ hp.two_le) hn
@@ -555,9 +590,9 @@ not_imp_not.mp prime.pow_not_prime' h
 
 lemma prime.pow_eq_iff {p a k : ℕ} (hp : p.prime) : a ^ k = p ↔ a = p ∧ k = 1 :=
 begin
-  refine ⟨_, λ h, by rw [h.1, h.2, pow_one]⟩,
-  rintro rfl,
-  rw [hp.eq_one_of_pow, eq_self_iff_true, and_true, pow_one],
+  refine ⟨λ h, _, λ h, by rw [h.1, h.2, pow_one]⟩,
+  rw ←h at hp,
+  rw [←h, hp.eq_one_of_pow, eq_self_iff_true, and_true, pow_one],
 end
 
 lemma prime.mul_eq_prime_sq_iff {x y p : ℕ} (hp : p.prime) (hx : x ≠ 1) (hy : y ≠ 1) :

src/data/zmod/basic.lean

@@ -843,7 +843,7 @@ instance : field (zmod p) :=
 instance (p : ℕ) [hp : fact p.prime] : is_domain (zmod p) :=
 begin
   -- We need `cases p` here in order to resolve which `comm_ring` instance is being used.
-  unfreezingI { cases p, { exfalso, rcases hp with ⟨⟨⟨⟩⟩⟩, }, },
+  unfreezingI { cases p, { exact (nat.not_prime_zero hp.out).elim }, },
   exact @field.is_domain (zmod _) (zmod.field _)
 end
 

src/dynamics/periodic_pts.lean

@@ -295,7 +295,7 @@ by simp_rw [is_periodic_pt_iff_minimal_period_dvd, dvd_right_iff_eq]
 
 lemma minimal_period_eq_prime {p : ℕ} [hp : fact p.prime] (hper : is_periodic_pt f p x)
   (hfix : ¬ is_fixed_pt f x) : minimal_period f x = p :=
-(hp.out.2 _ (hper.minimal_period_dvd)).resolve_left
+(hp.out.eq_one_or_self_of_dvd _ (hper.minimal_period_dvd)).resolve_left
   (mt is_fixed_point_iff_minimal_period_eq_one.1 hfix)
 
 lemma minimal_period_eq_prime_pow {p k : ℕ} [hp : fact p.prime] (hk : ¬ is_periodic_pt f (p ^ k) x)

src/group_theory/order_of_element.lean

@@ -259,8 +259,8 @@ omit hp
 -- An example on how to determine the order of an element of a finite group.
 example : order_of (-1 : units ℤ) = 2 :=
 begin
-  haveI : fact (prime 2) := ⟨prime_two⟩,
-  exact order_of_eq_prime (int.units_mul_self _) dec_trivial,
+  haveI := fact_prime_two,
+  exact order_of_eq_prime (int.units_sq _) dec_trivial,
 end
 
 end p_prime

src/group_theory/perm/cycle_type.lean

@@ -188,12 +188,12 @@ lemma cycle_type_prime_order {σ : perm α} (hσ : (order_of σ).prime) :
   ∃ n : ℕ, σ.cycle_type = repeat (order_of σ) (n + 1) :=
 begin
   rw eq_repeat_of_mem (λ n hn, or_iff_not_imp_left.mp
-    (hσ.2 n (dvd_of_mem_cycle_type hn)) (ne_of_gt (one_lt_of_mem_cycle_type hn))),
+    (hσ.eq_one_or_self_of_dvd n (dvd_of_mem_cycle_type hn)) (one_lt_of_mem_cycle_type hn).ne'),
   use σ.cycle_type.card - 1,
   rw tsub_add_cancel_of_le,
   rw [nat.succ_le_iff, pos_iff_ne_zero, ne, card_cycle_type_eq_zero],
-  rintro rfl,
-  rw order_of_one at hσ,
+  intro H,
+  rw [H, order_of_one] at hσ,
   exact hσ.ne_one rfl,
 end
 

src/group_theory/specific_groups/cyclic.lean

@@ -487,6 +487,7 @@ theorem prime_card [fintype α] : (fintype.card α).prime :=
 begin
   have h0 : 0 < fintype.card α := fintype.card_pos_iff.2 (by apply_instance),
   obtain ⟨g, hg⟩ := is_cyclic.exists_generator α,
+  rw nat.prime_def_lt'',
   refine ⟨fintype.one_lt_card_iff_nontrivial.2 infer_instance, λ n hn, _⟩,
   refine (is_simple_order.eq_bot_or_eq_top (subgroup.zpowers (g ^ n))).symm.imp _ _,
   { intro h,

src/number_theory/divisors.lean

@@ -262,11 +262,7 @@ lemma prime.divisors {p : ℕ} (pp : p.prime) :
   divisors p = {1, p} :=
 begin
   ext,
-  simp only [pp.ne_zero, and_true, ne.def, not_false_iff, finset.mem_insert,
-    finset.mem_singleton, mem_divisors],
-  refine ⟨pp.2 a, λ h, _⟩,
-  rcases h; subst h,
-  apply one_dvd,
+  rw [mem_divisors, dvd_prime pp, and_iff_left pp.ne_zero, finset.mem_insert, finset.mem_singleton]
 end
 
 lemma prime.proper_divisors {p : ℕ} (pp : p.prime) :
@@ -334,14 +330,10 @@ lemma proper_divisors_eq_singleton_one_iff_prime :
 ⟨λ h, begin
   have h1 := mem_singleton.2 rfl,
   rw [← h, mem_proper_divisors] at h1,
-  refine ⟨h1.2, _⟩,
-  intros m hdvd,
+  refine nat.prime_def_lt''.mpr ⟨h1.2, λ m hdvd, _⟩,
   rw [← mem_singleton, ← h, mem_proper_divisors],
-  cases lt_or_eq_of_le (nat.le_of_dvd (lt_trans (nat.succ_pos _) h1.2) hdvd),
-  { left,
-    exact ⟨hdvd, h_1⟩ },
-  { right,
-    exact h_1 }
+  have hle := nat.le_of_dvd (lt_trans (nat.succ_pos _) h1.2) hdvd,
+  exact or.imp_left (λ hlt, ⟨hdvd, hlt⟩) hle.lt_or_eq
 end, prime.proper_divisors⟩
 
 lemma sum_proper_divisors_eq_one_iff_prime :

src/number_theory/primorial.lean

@@ -25,12 +25,12 @@ open_locale big_operators nat
 
 /-- The primorial `n#` of `n` is the product of the primes less than or equal to `n`.
 -/
-def primorial (n : ℕ) : ℕ := ∏ p in (filter prime (range (n + 1))), p
+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# :=
 begin
-  have not_prime : ¬prime (n + 1),
+  have not_prime : ¬nat.prime (n + 1),
   { intros is_prime,
     cases (prime.eq_two_or_odd is_prime) with _ n_even,
     { linarith, },
@@ -41,7 +41,7 @@ begin
   { exact λ _ _, rfl, },
 end
 
-lemma dvd_choose_of_middling_prime (p : ℕ) (is_prime : prime p) (m : ℕ)
+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) :=
 begin
   have m_size : m + 1 ≤ 2 * m + 1 := le_of_lt (lt_of_lt_of_le p_big p_small),
@@ -65,7 +65,7 @@ begin
   cc, cc,
 end
 
-lemma prod_primes_dvd {s : finset ℕ} : ∀ (n : ℕ) (h : ∀ a ∈ s, prime a) (div : ∀ a ∈ s, a ∣ n),
+lemma prod_primes_dvd {s : finset ℕ} : ∀ (n : ℕ) (h : ∀ a ∈ s, nat.prime a) (div : ∀ a ∈ s, a ∣ n),
   (∏ p in s, p) ∣ n :=
 begin
   apply finset.induction_on s,
@@ -97,19 +97,19 @@ lemma primorial_le_4_pow : ∀ (n : ℕ), n# ≤ 4 ^ n
       let recurse : m + 1 < n + 2 := by linarith in
       begin
         calc (n + 2)#
-            = ∏ i in filter prime (range (2 * m + 2)), i : by simpa [←twice_m]
-        ... = ∏ i in filter prime (finset.Ico (m + 2) (2 * m + 2) ∪ range (m + 2)), i :
+            = ∏ i in filter nat.prime (range (2 * m + 2)), i : by simpa [←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,
                 simp only [add_le_add_iff_right],
                 linarith,
               end
-        ... = ∏ i in (filter prime (finset.Ico (m + 2) (2 * m + 2))
-              ∪ (filter prime (range (m + 2)))), i :
+        ... = ∏ 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 prime (finset.Ico (m + 2) (2 * m + 2)), i)
-              * (∏ i in filter prime (range (m + 2)), i) :
+        ... = (∏ 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)),
@@ -118,11 +118,11 @@ lemma primorial_le_4_pow : ∀ (n : ℕ), n# ≤ 4 ^ n
                   intros _ pr _, exact pr, },
                 exact finset.disjoint_filter_filter disj,
               end
-        ... ≤ (∏ i in filter prime (finset.Ico (m + 2) (2 * m + 2)), i) * 4 ^ (m + 1) :
-              by exact nat.mul_le_mul_left _ (primorial_le_4_pow (m + 1))
+        ... ≤ (∏ 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 prime (finset.Ico (m + 2) (2 * m + 2)),
+                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, cc, },
@@ -133,7 +133,7 @@ lemma primorial_le_4_pow : ∀ (n : ℕ), n# ≤ 4 ^ n
                     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 prime (finset.Ico (m + 2) (2 * m + 2)),
+                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), },
@@ -153,7 +153,7 @@ lemma primorial_le_4_pow : ∀ (n : ℕ), n# ≤ 4 ^ n
               ≤ 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, not_prime_zero, prime_two] },
+        norm_num [n_zero, primorial, range_succ, prod_filter, nat.not_prime_zero, nat.prime_two] },
     end
 
 end