feat(data/nat/totient): add nat.totient_prime_iff (#8833)

Co-authored-by: Johan Commelin <johan@commelin.net>

src/data/finset/basic.lean

@@ -270,6 +270,9 @@ def coe_emb : finset α ↪o set α := ⟨⟨coe, coe_injective⟩, λ s t, coe_
 theorem subset.antisymm_iff {s₁ s₂ : finset α} : s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁ :=
 le_antisymm_iff
 
+theorem not_subset (s t : finset α) : ¬(s ⊆ t) ↔ ∃ x ∈ s, ¬(x ∈ t) :=
+by simp only [←finset.coe_subset, set.not_subset, exists_prop, finset.mem_coe]
+
 @[simp] theorem le_eq_subset : ((≤) : finset α → finset α → Prop) = (⊆) := rfl
 @[simp] theorem lt_eq_subset : ((<) : finset α → finset α → Prop) = (⊂) := rfl
 
@@ -2337,6 +2340,13 @@ card_le_of_subset $ filter_subset _ _
 theorem eq_of_subset_of_card_le {s t : finset α} (h : s ⊆ t) (h₂ : card t ≤ card s) : s = t :=
 eq_of_veq $ multiset.eq_of_le_of_card_le (val_le_iff.mpr h) h₂
 
+lemma filter_card_eq {s : finset α} {p : α → Prop} [decidable_pred p]
+  (h : (s.filter p).card = s.card) (x : α) (hx : x ∈ s) : p x :=
+begin
+  rw [←eq_of_subset_of_card_le (s.filter_subset p) h.ge, mem_filter] at hx,
+  exact hx.2,
+end
+
 lemma card_lt_card {s t : finset α} (h : s ⊂ t) : s.card < t.card :=
 card_lt_of_lt (val_lt_iff.2 h)
 

src/data/nat/prime.lean

@@ -78,6 +78,16 @@ prime_def_lt'.trans $ and_congr_right $ λ p2,
       rwa [one_mul, ← e] }
   end⟩
 
+theorem prime_of_coprime (n : ℕ) (h1 : 1 < n) (h : ∀ m < n, m ≠ 0 → n.coprime m) : prime n :=
+begin
+  refine prime_def_lt.mpr ⟨h1, λ m mlt mdvd, _⟩,
+  have hm : m ≠ 0,
+  { rintro rfl,
+    rw zero_dvd_iff at mdvd,
+    exact mlt.ne' mdvd },
+  exact (h m mlt hm).symm.eq_one_of_dvd mdvd,
+end
+
 section
 
 /--

src/data/nat/totient.lean

@@ -172,6 +172,28 @@ by rcases exists_eq_succ_of_ne_zero (pos_iff_ne_zero.1 hn) with ⟨m, rfl⟩;
 lemma totient_prime {p : ℕ} (hp : p.prime) : φ p = p - 1 :=
 by rw [← pow_one p, totient_prime_pow hp]; simp
 
+lemma totient_eq_iff_prime {p : ℕ} (hp : 0 < p) : p.totient = p - 1 ↔ p.prime :=
+begin
+  refine ⟨λ h, _, totient_prime⟩,
+  replace hp : 1 < p,
+  { apply lt_of_le_of_ne,
+    { rwa succ_le_iff },
+    { rintro rfl,
+      rw [totient_one, nat.sub_self] at h,
+      exact one_ne_zero h } },
+  have hsplit : finset.range p = {0} ∪ (finset.Ico 1 p),
+  { rw [finset.range_eq_Ico, ←finset.Ico.union_consecutive zero_le_one hp.le,
+      finset.Ico.succ_singleton] },
+  have hempty : finset.filter p.coprime {0} = ∅,
+  { simp only [finset.filter_singleton, nat.coprime_zero_right, hp.ne', if_false] },
+  rw [totient_eq_card_coprime, hsplit, finset.filter_union, hempty, finset.empty_union,
+    ←finset.Ico.card 1 p] at h,
+  refine p.prime_of_coprime hp (λ n hn hnz, _),
+  apply finset.filter_card_eq h n,
+  refine finset.Ico.mem.mpr ⟨_, hn⟩,
+  rwa [succ_le_iff, pos_iff_ne_zero],
+end
+
 @[simp] lemma totient_two : φ 2 = 1 :=
 (totient_prime prime_two).trans (by norm_num)