feat(data/pnat): add missing norm_cast attributes (#16995)

Also renames `nat.primes.coe_[p]nat_inj` to `nat.primes.coe_[p]nat_injective` to match the naming guide, and make room for the `iff` version occupying the original name.

src/data/nat/prime.lean

@@ -847,12 +847,15 @@ instance inhabited_primes : inhabited primes := ⟨⟨2, prime_two⟩⟩
 
 instance coe_nat : has_coe nat.primes ℕ := ⟨subtype.val⟩
 
-theorem coe_nat_inj (p q : nat.primes) : (p : ℕ) = (q : ℕ) → p = q :=
-λ h, subtype.eq h
+theorem coe_nat_injective : function.injective (coe : nat.primes → ℕ) :=
+subtype.coe_injective
+
+theorem coe_nat_inj (p q : nat.primes) : (p : ℕ) = (q : ℕ) ↔ p = q :=
+subtype.ext_iff.symm
 
 end primes
 
-instance monoid.prime_pow {α : Type*} [monoid α] : has_pow α primes := ⟨λ x p, x^p.val⟩
+instance monoid.prime_pow {α : Type*} [monoid α] : has_pow α primes := ⟨λ x p, x^(p : ℕ)⟩
 
 end nat
 

src/data/pnat/basic.lean

@@ -116,13 +116,13 @@ open nat
 
 theorem eq {m n : ℕ+} : (m : ℕ) = n → m = n := subtype.eq
 
-@[simp] lemma coe_inj {m n : ℕ+} : (m : ℕ) = n ↔ m = n := set_coe.ext_iff
+@[simp, norm_cast] lemma coe_inj {m n : ℕ+} : (m : ℕ) = n ↔ m = n := set_coe.ext_iff
 
 lemma coe_injective : function.injective (coe : ℕ+ → ℕ) := subtype.coe_injective
 
 @[simp] theorem mk_coe (n h) : ((⟨n, h⟩ : ℕ+) : ℕ) = n := rfl
 
-@[simp] theorem add_coe (m n : ℕ+) : ((m + n : ℕ+) : ℕ) = m + n := rfl
+@[simp, norm_cast] theorem add_coe (m n : ℕ+) : ((m + n : ℕ+) : ℕ) = m + n := rfl
 
 /-- `pnat.coe` promoted to an `add_hom`, that is, a morphism which preserves addition. -/
 def coe_add_hom : add_hom ℕ+ ℕ :=
@@ -194,8 +194,8 @@ iff.rfl
 @[simp] lemma bit1_le_bit1 (n m : ℕ+) : (bit1 n) ≤ (bit1 m) ↔ (bit1 (n : ℕ)) ≤ (bit1 (m : ℕ)) :=
 iff.rfl
 
-@[simp] theorem one_coe : ((1 : ℕ+) : ℕ) = 1 := rfl
-@[simp] theorem mul_coe (m n : ℕ+) : ((m * n : ℕ+) : ℕ) = m * n := rfl
+@[simp, norm_cast] theorem one_coe : ((1 : ℕ+) : ℕ) = 1 := rfl
+@[simp, norm_cast] theorem mul_coe (m n : ℕ+) : ((m * n : ℕ+) : ℕ) = m * n := rfl
 
 /-- `pnat.coe` promoted to a `monoid_hom`. -/
 def coe_monoid_hom : ℕ+ →* ℕ :=
@@ -205,18 +205,19 @@ def coe_monoid_hom : ℕ+ →* ℕ :=
 
 @[simp] lemma coe_coe_monoid_hom : (coe_monoid_hom : ℕ+ → ℕ) = coe := rfl
 
-@[simp] lemma coe_eq_one_iff {m : ℕ+} : (m : ℕ) = 1 ↔ m = 1 := subtype.coe_injective.eq_iff' one_coe
+@[simp, norm_cast] lemma coe_eq_one_iff {m : ℕ+} : (m : ℕ) = 1 ↔ m = 1 :=
+subtype.coe_injective.eq_iff' one_coe
 
 @[simp] lemma le_one_iff {n : ℕ+} : n ≤ 1 ↔ n = 1 := le_bot_iff
 
 lemma lt_add_left (n m : ℕ+) : n < m + n := lt_add_of_pos_left _ m.2
 
 lemma lt_add_right (n m : ℕ+) : n < n + m := (lt_add_left n m).trans_eq (add_comm _ _)
 
-@[simp] lemma coe_bit0 (a : ℕ+) : ((bit0 a : ℕ+) : ℕ) = bit0 (a : ℕ) := rfl
-@[simp] lemma coe_bit1 (a : ℕ+) : ((bit1 a : ℕ+) : ℕ) = bit1 (a : ℕ) := rfl
+@[simp, norm_cast] lemma coe_bit0 (a : ℕ+) : ((bit0 a : ℕ+) : ℕ) = bit0 (a : ℕ) := rfl
+@[simp, norm_cast] lemma coe_bit1 (a : ℕ+) : ((bit1 a : ℕ+) : ℕ) = bit1 (a : ℕ) := rfl
 
-@[simp] theorem pow_coe (m : ℕ+) (n : ℕ) : ((m ^ n : ℕ+) : ℕ) = (m : ℕ) ^ n :=
+@[simp, norm_cast] theorem pow_coe (m : ℕ+) (n : ℕ) : ((m ^ n : ℕ+) : ℕ) = (m : ℕ) ^ n :=
 rfl
 
 /-- Subtraction a - b is defined in the obvious way when

src/data/pnat/factors.lean

@@ -55,7 +55,7 @@ def coe_nat_monoid_hom : prime_multiset →+ multiset ℕ :=
   (coe_nat_monoid_hom : prime_multiset → multiset ℕ) = coe := rfl
 
 theorem coe_nat_injective : function.injective (coe : prime_multiset → multiset ℕ) :=
-multiset.map_injective nat.primes.coe_nat_inj
+multiset.map_injective nat.primes.coe_nat_injective
 
 theorem coe_nat_of_prime (p : nat.primes) :
 ((of_prime p) : multiset ℕ) = {p} := rfl
@@ -81,10 +81,10 @@ def coe_pnat_monoid_hom : prime_multiset →+ multiset ℕ+ :=
   (coe_pnat_monoid_hom : prime_multiset → multiset ℕ+) = coe := rfl
 
 theorem coe_pnat_injective : function.injective (coe : prime_multiset → multiset ℕ+) :=
-multiset.map_injective nat.primes.coe_pnat_inj
+multiset.map_injective nat.primes.coe_pnat_injective
 
 theorem coe_pnat_of_prime (p : nat.primes) :
-((of_prime p) : multiset ℕ+) = {(p : ℕ+)} := rfl
+  ((of_prime p) : multiset ℕ+) = {(p : ℕ+)} := rfl
 
 theorem coe_pnat_prime (v : prime_multiset)
   (p : ℕ+) (h : p ∈ (v : multiset ℕ+)) : p.prime :=

src/data/pnat/prime.lean

@@ -16,14 +16,14 @@ This file extends the theory of `ℕ+` with `gcd`, `lcm` and `prime` functions,
 namespace nat.primes
 
 instance coe_pnat : has_coe nat.primes ℕ+ := ⟨λ p, ⟨(p : ℕ), p.property.pos⟩⟩
-theorem coe_pnat_nat (p : nat.primes) : ((p : ℕ+) : ℕ) = p := rfl
 
-theorem coe_pnat_inj (p q : nat.primes) : (p : ℕ+) = (q : ℕ+) → p = q := λ h,
-begin
-  replace h : ((p : ℕ+) : ℕ) = ((q : ℕ+) : ℕ) := congr_arg subtype.val h,
-  rw [coe_pnat_nat, coe_pnat_nat] at h,
-  exact subtype.eq h,
-end
+@[norm_cast] theorem coe_pnat_nat (p : nat.primes) : ((p : ℕ+) : ℕ) = p := rfl
+
+theorem coe_pnat_injective : function.injective (coe : nat.primes → ℕ+) :=
+λ p q h, subtype.ext (congr_arg subtype.val h : _)
+
+@[norm_cast] theorem coe_pnat_inj (p q : nat.primes) : (p : ℕ+) = (q : ℕ+) ↔ p = q :=
+coe_pnat_injective.eq_iff
 
 end nat.primes
 
@@ -43,9 +43,9 @@ def lcm (n m : ℕ+) : ℕ+ :=
        rw [← gcd_mul_lcm (n : ℕ) (m : ℕ), mul_comm] at h,
        exact pos_of_dvd_of_pos (dvd.intro (nat.gcd (n : ℕ) (m : ℕ)) rfl) h }⟩
 
-@[simp] theorem gcd_coe (n m : ℕ+) : ((gcd n m) : ℕ) = nat.gcd n m := rfl
+@[simp, norm_cast] theorem gcd_coe (n m : ℕ+) : ((gcd n m) : ℕ) = nat.gcd n m := rfl
 
-@[simp] theorem lcm_coe (n m : ℕ+) : ((lcm n m) : ℕ) = nat.lcm n m := rfl
+@[simp, norm_cast] theorem lcm_coe (n m : ℕ+) : ((lcm n m) : ℕ) = nat.lcm n m := rfl
 
 theorem gcd_dvd_left (n m : ℕ+) : (gcd n m) ∣ n := dvd_iff.2 (nat.gcd_dvd_left (n : ℕ) (m : ℕ))
 
@@ -107,7 +107,7 @@ section coprime
 /-- Two pnats are coprime if their gcd is 1. -/
 def coprime (m n : ℕ+) : Prop := m.gcd n = 1
 
-@[simp]
+@[simp, norm_cast]
 lemma coprime_coe {m n : ℕ+} : nat.coprime ↑m ↑n ↔ m.coprime n :=
 by { unfold coprime, unfold nat.coprime, rw ← coe_inj, simp }