chore(data/nat/prime): add 2 aliases (#17372)

Add `nat.prime.prime` and `prime.nat_prime`. Also move 2 lemmas and golf some proofs.

src/algebra/associated.lean

@@ -537,7 +537,6 @@ lemma associated.of_pow_associated_of_prime' [cancel_comm_monoid_with_zero α] {
   p₁ ~ᵤ p₂ :=
 (h.symm.of_pow_associated_of_prime hp₂ hp₁ hk₂).symm
 
-
 section unique_units
 variables [monoid α] [unique αˣ]
 
@@ -560,6 +559,20 @@ by rw [pp.dvd_prime_iff_associated qp, ←associated_eq_eq]
 
 end unique_units
 
+section unique_units₀
+
+variables {R : Type*} [cancel_comm_monoid_with_zero R] [unique Rˣ] {p₁ p₂ : R} {k₁ k₂ : ℕ}
+
+lemma eq_of_prime_pow_eq (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ = p₂ ^ k₂) :
+  p₁ = p₂ :=
+by { rw [←associated_iff_eq] at h ⊢, apply h.of_pow_associated_of_prime hp₁ hp₂ hk₁ }
+
+lemma eq_of_prime_pow_eq' (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₂) (h : p₁ ^ k₁ = p₂ ^ k₂) :
+  p₁ = p₂ :=
+by { rw [←associated_iff_eq] at h ⊢, apply h.of_pow_associated_of_prime' hp₁ hp₂ hk₁ }
+
+end unique_units₀
+
 /-- The quotient of a monoid by the `associated` relation. Two elements `x` and `y`
   are associated iff there is a unit `u` such that `x * u = y`. There is a natural
   monoid structure on `associates α`. -/

src/algebra/char_p/local_ring.lean

@@ -61,15 +61,11 @@ begin
     end,
     have q_eq_rn := nat.dvd_antisymm ((char_p.cast_eq_zero_iff R q (r ^ n)).mp rn_cast_zero)
       rn_dvd_q,
-    have n_pos : n ≠ 0 :=
-    begin
-      by_contradiction n_zero,
-      simp [n_zero] at q_eq_rn,
-      exact absurd q_eq_rn (char_p.char_ne_one R q),
-    end,
+    have n_pos : n ≠ 0,
+      from λ n_zero, absurd (by simpa [n_zero] using q_eq_rn) (char_p.char_ne_one R q),
 
     /- Definition of prime power: `∃ r n, prime r ∧ 0 < n ∧ r ^ n = q`. -/
-    exact ⟨r, ⟨n, ⟨nat.prime_iff.mp r_prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩},
+    exact ⟨r, ⟨n, ⟨r_prime.prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩},
   { haveI K_char_p_0 := ring_char.of_eq r_zero,
     haveI K_char_zero: char_zero K := char_p.char_p_to_char_zero K,
     haveI R_char_zero := ring_hom.char_zero (local_ring.residue R),

src/algebra/is_prime_pow.lean

@@ -59,28 +59,13 @@ theorem is_prime_pow.ne_zero [no_zero_divisors R] {n : R} (h : is_prime_pow n) :
 lemma is_prime_pow.ne_one {n : R} (h : is_prime_pow n) : n ≠ 1 :=
 λ t, eq.rec not_is_prime_pow_one t.symm h
 
-section unique_units
-
-lemma eq_of_prime_pow_eq {R : Type*} [cancel_comm_monoid_with_zero R] [unique Rˣ] {p₁ p₂ : R}
-  {k₁ k₂ : ℕ} (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ = p₂ ^ k₂) :
-  p₁ = p₂ :=
-by { rw [←associated_iff_eq] at h ⊢, apply h.of_pow_associated_of_prime hp₁ hp₂ hk₁ }
-
-lemma eq_of_prime_pow_eq' {R : Type*} [cancel_comm_monoid_with_zero R] [unique Rˣ] {p₁ p₂ : R}
-  {k₁ k₂ : ℕ} (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₂) (h : p₁ ^ k₁ = p₂ ^ k₂) :
-  p₁ = p₂ :=
-by { rw [←associated_iff_eq] at h ⊢, apply h.of_pow_associated_of_prime' hp₁ hp₂ hk₁ }
-
-end unique_units
-
 section nat
 
 lemma is_prime_pow_nat_iff (n : ℕ) :
   is_prime_pow n ↔ ∃ (p k : ℕ), nat.prime p ∧ 0 < k ∧ p ^ k = n :=
 by simp only [is_prime_pow_def, nat.prime_iff]
 
-lemma nat.prime.is_prime_pow {p : ℕ} (hp : p.prime) : is_prime_pow p :=
-(nat.prime_iff.mp hp).is_prime_pow
+lemma nat.prime.is_prime_pow {p : ℕ} (hp : p.prime) : is_prime_pow p := hp.prime.is_prime_pow
 
 lemma is_prime_pow_nat_iff_bounded (n : ℕ) :
   is_prime_pow n ↔ ∃ (p : ℕ), p ≤ n ∧ ∃ (k : ℕ), k ≤ n ∧ p.prime ∧ 0 < k ∧ p ^ k = n :=

src/data/nat/factorization/prime_pow.lean

@@ -28,7 +28,7 @@ lemma is_prime_pow_of_min_fac_pow_factorization_eq {n : ℕ}
 begin
   rcases eq_or_ne n 0 with rfl | hn',
   { simpa using h },
-  refine ⟨_, _, nat.prime_iff.1 (nat.min_fac_prime hn), _, h⟩,
+  refine ⟨_, _, (nat.min_fac_prime hn).prime, _, h⟩,
   rw [pos_iff_ne_zero, ←finsupp.mem_support_iff, nat.factor_iff_mem_factorization,
     nat.mem_factors_iff_dvd hn' (nat.min_fac_prime hn)],
   apply nat.min_fac_dvd

src/data/nat/prime.lean

@@ -569,8 +569,10 @@ mt pp.dvd_mul.1 $ by simp [Hm, Hn]
 theorem prime_iff {p : ℕ} : p.prime ↔ _root_.prime p :=
 ⟨λ h, ⟨h.ne_zero, h.not_unit, λ a b, h.dvd_mul.mp⟩, prime.irreducible⟩
 
-theorem irreducible_iff_prime {p : ℕ} : irreducible p ↔ _root_.prime p :=
-by rw [←prime_iff, prime]
+alias prime_iff ↔ prime.prime _root_.prime.nat_prime
+attribute [protected, nolint dup_namespace] prime.prime
+
+theorem irreducible_iff_prime {p : ℕ} : irreducible p ↔ _root_.prime p := prime_iff
 
 theorem prime.dvd_of_dvd_pow {p m n : ℕ} (pp : prime p) (h : p ∣ m^n) : p ∣ m :=
 begin

src/field_theory/cardinality.lean

@@ -50,7 +50,7 @@ lemma fintype.nonempty_field_iff {α} [fintype α] : nonempty (field α) ↔ is_
 begin
   refine ⟨λ ⟨h⟩, by exactI fintype.is_prime_pow_card_of_field, _⟩,
   rintros ⟨p, n, hp, hn, hα⟩,
-  haveI := fact.mk (nat.prime_iff.mpr hp),
+  haveI := fact.mk hp.nat_prime,
   exact ⟨(fintype.equiv_of_card_eq ((galois_field.card p n hn.ne').trans hα)).symm.field⟩,
 end
 

src/group_theory/p_group.lean

@@ -322,12 +322,9 @@ begin
   obtain ⟨n₂, hn₂⟩ := iff_order_of.mp hH₂ ⟨x, hx₂⟩,
   rw [← order_of_subgroup, subgroup.coe_mk] at hn₁ hn₂,
   have : p₁ ^ n₁ = p₂ ^ n₂, by rw [← hn₁, ← hn₂],
-  have : n₁ = 0,
-  { contrapose! hne with h,
-    rw ← associated_iff_eq at this ⊢,
-    exact associated.of_pow_associated_of_prime
-      (nat.prime_iff.mp hp₁.elim) (nat.prime_iff.mp hp₂.elim) (ne.bot_lt h) this },
-  simpa [this] using hn₁,
+  rcases n₁.eq_zero_or_pos with rfl|hn₁,
+  { simpa using hn₁ },
+  { exact absurd (eq_of_prime_pow_eq hp₁.out.prime hp₂.out.prime hn₁ this) hne }
 end
 
 section p2comm

src/group_theory/torsion.lean

@@ -219,15 +219,12 @@ by simpa [primary_component] using g.property
 @[to_additive "The `p`- and `q`-primary components are disjoint for `p ≠ q`."]
 lemma primary_component.disjoint {p' : ℕ} [hp' : fact p'.prime] (hne : p ≠ p') :
   disjoint (comm_monoid.primary_component G p) (comm_monoid.primary_component G p') :=
-submonoid.disjoint_def.mpr $ λ g hgp hgp',
+submonoid.disjoint_def.mpr $
 begin
-  obtain ⟨n, hn⟩ := primary_component.exists_order_of_eq_prime_pow ⟨g, set_like.mem_coe.mp hgp⟩,
-  obtain ⟨n', hn'⟩ := primary_component.exists_order_of_eq_prime_pow ⟨g, set_like.mem_coe.mp hgp'⟩,
-  have := mt (eq_of_prime_pow_eq (nat.prime_iff.mp hp.out) (nat.prime_iff.mp hp'.out)),
-  simp only [not_forall, exists_prop, not_lt, le_zero_iff, and_imp] at this,
-  rw [←order_of_submonoid, set_like.coe_mk] at hn hn',
-  have hnzero := this (hn.symm.trans hn') hne,
-  rwa [hnzero, pow_zero, order_of_eq_one_iff] at hn,
+  rintro g ⟨(_|n), hn⟩ ⟨n', hn'⟩,
+  { rwa [pow_zero, order_of_eq_one_iff] at hn },
+  { exact absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos
+      (hn.symm.trans hn')) hne }
 end
 
 end comm_monoid

src/number_theory/von_mangoldt.lean

@@ -77,7 +77,7 @@ lemma von_mangoldt_apply_pow {n k : ℕ} (hk : k ≠ 0) : Λ (n ^ k) = Λ n :=
 by simp only [von_mangoldt_apply, is_prime_pow_pow_iff hk, pow_min_fac hk]
 
 lemma von_mangoldt_apply_prime {p : ℕ} (hp : p.prime) : Λ p = real.log p :=
-by rw [von_mangoldt_apply, prime.min_fac_eq hp, if_pos (nat.prime_iff.1 hp).is_prime_pow]
+by rw [von_mangoldt_apply, prime.min_fac_eq hp, if_pos hp.prime.is_prime_pow]
 
 lemma von_mangoldt_ne_zero_iff {n : ℕ} : Λ n ≠ 0 ↔ is_prime_pow n :=
 begin

src/ring_theory/int/basic.lean

@@ -329,7 +329,7 @@ begin
     rw nat.is_unit_iff.1 h,
     exact h₁, },
   { intros a p _ hp ha,
-    exact h p a (nat.prime_iff.2 hp) ha, },
+    exact h p a hp.nat_prime ha, },
 end
 
 lemma int.associated_nat_abs (k : ℤ) : associated k k.nat_abs :=

src/ring_theory/roots_of_unity.lean

@@ -1054,7 +1054,7 @@ begin
     simp [nat.is_unit_iff.mp hunit] },
   { intros a p ha hprime hind n hcop h,
     rw hind (nat.coprime.coprime_mul_left hcop) h, clear hind,
-    replace hprime := nat.prime_iff.2 hprime,
+    replace hprime := hprime.nat_prime,
     have hdiv := (nat.prime.coprime_iff_not_dvd hprime).1 (nat.coprime.coprime_mul_right hcop),
     haveI := fact.mk hprime,
     rw [minpoly_eq_pow (h.pow_of_coprime a (nat.coprime.coprime_mul_left hcop)) hdiv],