chore(data/nat/prime): slightly weaken assumption in nat.exists_prime…

…_and_dvd (#12156)

It is vacuously true for zero, as everything divides zero.

src/algebra/squarefree.lean

@@ -514,7 +514,7 @@ begin
   subst e,
   refine λ k0 ih, irreducible.squarefree (nat.prime_def_le_sqrt.2 ⟨bit1_lt_bit1.2 h, _⟩),
   intros m m2 hm md,
-  obtain ⟨p, pp, hp⟩ := nat.exists_prime_and_dvd m2,
+  obtain ⟨p, pp, hp⟩ := nat.exists_prime_and_dvd (ne_of_gt m2),
   have := (ih p pp (dvd_trans hp md)).trans
     (le_trans (nat.le_of_dvd (lt_of_lt_of_le dec_trivial m2) hp) hm),
   rw nat.le_sqrt at this,

src/data/nat/prime.lean

@@ -377,8 +377,8 @@ theorem exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬ prime n) :
 ⟨min_fac n, min_fac_dvd _, (min_fac_prime (ne_of_gt n2)).two_le,
   (not_prime_iff_min_fac_lt n2).1 np⟩
 
-theorem exists_prime_and_dvd {n : ℕ} (n2 : 2 ≤ n) : ∃ p, prime p ∧ p ∣ n :=
-⟨min_fac n, min_fac_prime (ne_of_gt n2), min_fac_dvd _⟩
+theorem exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, prime p ∧ p ∣ n :=
+⟨min_fac n, min_fac_prime hn, min_fac_dvd _⟩
 
 /-- Euclid's theorem on the **infinitude of primes**.
 Here given in the form: for every `n`, there exists a prime number `p ≥ n`. -/
@@ -398,13 +398,9 @@ p.mod_two_eq_zero_or_one.imp_left
 
 theorem coprime_of_dvd {m n : ℕ} (H : ∀ k, prime k → k ∣ m → ¬ k ∣ n) : coprime m n :=
 begin
-  have g1 : 1 ≤ gcd m n,
-  { refine nat.succ_le_of_lt (pos_iff_ne_zero.mpr (λ g0, _)),
-    rw [eq_zero_of_gcd_eq_zero_left g0, eq_zero_of_gcd_eq_zero_right g0] at H,
-    exact H 2 prime_two (dvd_zero _) (dvd_zero _) },
-  rw [coprime_iff_gcd_eq_one, eq_comm],
-  refine g1.lt_or_eq.resolve_left (λ g2, _),
-  obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd (succ_le_of_lt g2),
+  rw [coprime_iff_gcd_eq_one],
+  by_contra g2,
+  obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd g2,
   apply H p hp; apply dvd_trans hpdvd,
   { exact gcd_dvd_left _ _ },
   { exact gcd_dvd_right _ _ }

src/data/pnat/prime.lean

@@ -93,9 +93,9 @@ lemma not_prime_one : ¬ (1: ℕ+).prime :=  nat.not_prime_one
 lemma prime.not_dvd_one {p : ℕ+} :
 p.prime →  ¬ p ∣ 1 := λ pp : p.prime, by {rw dvd_iff, apply nat.prime.not_dvd_one pp}
 
-lemma exists_prime_and_dvd {n : ℕ+} : 2 ≤ n → (∃ (p : ℕ+), p.prime ∧ p ∣ n) :=
+lemma exists_prime_and_dvd {n : ℕ+} (hn : n ≠ 1) : (∃ (p : ℕ+), p.prime ∧ p ∣ n) :=
 begin
-  intro h, cases nat.exists_prime_and_dvd h with p hp,
+  obtain ⟨p, hp⟩ := nat.exists_prime_and_dvd (mt coe_eq_one_iff.mp hn),
   existsi (⟨p, nat.prime.pos hp.left⟩ : ℕ+), rw dvd_iff, apply hp
 end
 

src/ring_theory/int/basic.lean

@@ -263,9 +263,9 @@ begin
     exact (or_self _).mp ((nat.prime.dvd_mul hp).mp hpp)}
 end
 
-lemma int.exists_prime_and_dvd {n : ℤ} (n2 : 2 ≤ n.nat_abs) : ∃ p, prime p ∧ p ∣ n :=
+lemma int.exists_prime_and_dvd {n : ℤ} (hn : n.nat_abs ≠ 1) : ∃ p, prime p ∧ p ∣ n :=
 begin
-  obtain ⟨p, pp, pd⟩ := nat.exists_prime_and_dvd n2,
+  obtain ⟨p, pp, pd⟩ := nat.exists_prime_and_dvd hn,
   exact ⟨p, nat.prime_iff_prime_int.mp pp, int.coe_nat_dvd_left.mpr pd⟩,
 end