From 60af8c9a5a62728c41542c4fb5b472807bbb45c6 Mon Sep 17 00:00:00 2001
From: Jireh Loreaux <loreaujy@gmail.com>
Date: Mon, 25 Dec 2023 12:41:35 +0000
Subject: [PATCH] feat: add some missing API lemmas about `Nat.properDivisors`
 and `Nat.primeFactors` (#8858)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
---
 Mathlib/Data/Nat/PrimeFin.lean     |  5 +++++
 Mathlib/NumberTheory/Divisors.lean | 34 ++++++++++++++++++++++++++++++
 2 files changed, 39 insertions(+)

diff --git a/Mathlib/Data/Nat/PrimeFin.lean b/Mathlib/Data/Nat/PrimeFin.lean
index 1a2efccc29f54..50f85ef00af29 100644
--- a/Mathlib/Data/Nat/PrimeFin.lean
+++ b/Mathlib/Data/Nat/PrimeFin.lean
@@ -67,6 +67,11 @@ lemma le_of_mem_primeFactors (h : p ∈ n.primeFactors) : p ≤ n :=
     exact Nonempty.ne_empty $ ⟨_, mem_primeFactors.2 ⟨hp, hpn, hn.1⟩⟩
   · rintro (rfl | rfl) <;> simp
 
+@[simp]
+lemma nonempty_primeFactors {n : ℕ} : n.primeFactors.Nonempty ↔ 1 < n := by
+  rw [← not_iff_not, Finset.not_nonempty_iff_eq_empty, primeFactors_eq_empty, not_lt,
+    Nat.le_one_iff_eq_zero_or_eq_one]
+
 @[simp] protected lemma Prime.primeFactors (hp : p.Prime) : p.primeFactors = {p} := by
   simp [Nat.primeFactors, factors_prime hp]
 
diff --git a/Mathlib/NumberTheory/Divisors.lean b/Mathlib/NumberTheory/Divisors.lean
index 6aaf80c8eab22..cff3ebc327baa 100644
--- a/Mathlib/NumberTheory/Divisors.lean
+++ b/Mathlib/NumberTheory/Divisors.lean
@@ -172,6 +172,14 @@ theorem properDivisors_zero : properDivisors 0 = ∅ := by
   simp
 #align nat.proper_divisors_zero Nat.properDivisors_zero
 
+@[simp]
+lemma nonempty_divisors : (divisors n).Nonempty ↔ n ≠ 0 :=
+  ⟨fun ⟨m, hm⟩ hn ↦ by simp [hn] at hm, fun hn ↦ ⟨1, one_mem_divisors.2 hn⟩⟩
+
+@[simp]
+lemma divisors_eq_empty : divisors n = ∅ ↔ n = 0 :=
+  not_nonempty_iff_eq_empty.symm.trans nonempty_divisors.not_left
+
 theorem properDivisors_subset_divisors : properDivisors n ⊆ divisors n :=
   filter_subset_filter _ <| Ico_subset_Ico_right n.le_succ
 #align nat.proper_divisors_subset_divisors Nat.properDivisors_subset_divisors
@@ -208,6 +216,32 @@ lemma sup_divisors_id (n : ℕ) : n.divisors.sup id = n := by
   · apply zero_le
   · exact Finset.le_sup (f := id) <| mem_divisors_self n hn
 
+lemma one_lt_of_mem_properDivisors {m n : ℕ} (h : m ∈ n.properDivisors) : 1 < n :=
+  lt_of_le_of_lt (pos_of_mem_properDivisors h) (mem_properDivisors.1 h).2
+
+lemma one_lt_div_of_mem_properDivisors {m n : ℕ} (h : m ∈ n.properDivisors) :
+    1 < n / m := by
+  obtain ⟨h_dvd, h_lt⟩ := mem_properDivisors.mp h
+  rwa [Nat.lt_div_iff_mul_lt h_dvd, mul_one]
+
+/-- See also `Nat.mem_properDivisors`. -/
+lemma mem_properDivisors_iff_exists {m n : ℕ} (hn : n ≠ 0) :
+    m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k := by
+  refine ⟨fun h ↦ ⟨n / m, one_lt_div_of_mem_properDivisors h, ?_⟩, ?_⟩
+  · exact (Nat.mul_div_cancel' (mem_properDivisors.mp h).1).symm
+  · rintro ⟨k, hk, rfl⟩
+    rw [mul_ne_zero_iff] at hn
+    exact mem_properDivisors.mpr ⟨⟨k, rfl⟩, lt_mul_of_one_lt_right (Nat.pos_of_ne_zero hn.1) hk⟩
+
+@[simp]
+lemma nonempty_properDivisors : n.properDivisors.Nonempty ↔ 1 < n :=
+  ⟨fun ⟨_m, hm⟩ ↦ one_lt_of_mem_properDivisors hm, fun hn ↦
+    ⟨1, one_mem_properDivisors_iff_one_lt.2 hn⟩⟩
+
+@[simp]
+lemma properDivisors_eq_empty : n.properDivisors = ∅ ↔ n ≤ 1 := by
+  rw [← not_nonempty_iff_eq_empty, nonempty_properDivisors, not_lt]
+
 @[simp]
 theorem divisorsAntidiagonal_zero : divisorsAntidiagonal 0 = ∅ := by
   ext