From ae5a55ecb6b12c6efce48e5306c10ef94e275658 Mon Sep 17 00:00:00 2001 From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com> Date: Sat, 23 Mar 2024 13:54:06 -0700 Subject: [PATCH 1/9] feat(Data/Nat/Prime): add 2 theorems --- Mathlib/Data/Nat/Prime.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean index c45fe63d02914..d513c9dff7376 100644 --- a/Mathlib/Data/Nat/Prime.lean +++ b/Mathlib/Data/Nat/Prime.lean @@ -455,6 +455,23 @@ theorem exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) : (not_prime_iff_minFac_lt n2).1 np⟩ #align nat.exists_dvd_of_not_prime2 Nat.exists_dvd_of_not_prime2 +theorem not_prime_of_dvd (n2 : 2 ≤ n) : (∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n) → ¬Prime n := by + intro ⟨m, dvd, hne1, hneq⟩ + have n0 : 0 < n := lt_of_succ_le (le_of_succ_le n2) + have mn : m < n := lt_of_le_of_ne (le_of_dvd n0 dvd) hneq + refine' (not_prime_iff_minFac_lt n2).mpr _ + refine' lt_of_le_of_lt (minFac_le_of_dvd _ dvd) mn + match m with + | 0 => refine False.elim (hneq (Nat.zero_dvd.mp dvd).symm) + | 1 => contradiction + | m + 2 => simp only [le_add_iff_nonneg_left, _root_.zero_le] + +theorem not_prime_of_dvd2 (n2 : 2 ≤ n) : (∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n) → ¬Prime n := by + intro ⟨m, dvd, hm2, hm⟩ + refine' not_prime_of_dvd n2 ⟨m, ⟨dvd, ⟨_, _⟩⟩⟩ + · exact ne_of_gt (lt_of_succ_le hm2) + · exact ne_of_lt hm + theorem exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, Prime p ∧ p ∣ n := ⟨minFac n, minFac_prime hn, minFac_dvd _⟩ #align nat.exists_prime_and_dvd Nat.exists_prime_and_dvd From 7be4eadc0f849c9070077652fd48b6762b7f98bf Mon Sep 17 00:00:00 2001 From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com> Date: Sun, 24 Mar 2024 15:00:59 -0700 Subject: [PATCH 2/9] fixup: add 2 iff theorems --- Mathlib/Data/Nat/Prime.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean index d513c9dff7376..bfb44a998481a 100644 --- a/Mathlib/Data/Nat/Prime.lean +++ b/Mathlib/Data/Nat/Prime.lean @@ -472,6 +472,12 @@ theorem not_prime_of_dvd2 (n2 : 2 ≤ n) : (∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n · exact ne_of_gt (lt_of_succ_le hm2) · exact ne_of_lt hm +theorem exists_dvd_iff_not_prime {n : ℕ} (n2 : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := + ⟨exists_dvd_of_not_prime n2, not_prime_of_dvd n2⟩ + +theorem exists_dvd_iff_not_prime2 {n : ℕ} (n2 : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n := + ⟨exists_dvd_of_not_prime2 n2, not_prime_of_dvd2 n2⟩ + theorem exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, Prime p ∧ p ∣ n := ⟨minFac n, minFac_prime hn, minFac_dvd _⟩ #align nat.exists_prime_and_dvd Nat.exists_prime_and_dvd From ec93200480d94912481dd6b2e1ae8bf103347f5e Mon Sep 17 00:00:00 2001 From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com> Date: Fri, 29 Mar 2024 23:11:03 -0700 Subject: [PATCH 3/9] Update Mathlib/Data/Nat/Prime.lean golf from @tb65536 Co-authored-by: Thomas Browning --- Mathlib/Data/Nat/Prime.lean | 24 ++++++++---------------- 1 file changed, 8 insertions(+), 16 deletions(-) diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean index bfb44a998481a..4ce6e1486447d 100644 --- a/Mathlib/Data/Nat/Prime.lean +++ b/Mathlib/Data/Nat/Prime.lean @@ -455,22 +455,14 @@ theorem exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) : (not_prime_iff_minFac_lt n2).1 np⟩ #align nat.exists_dvd_of_not_prime2 Nat.exists_dvd_of_not_prime2 -theorem not_prime_of_dvd (n2 : 2 ≤ n) : (∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n) → ¬Prime n := by - intro ⟨m, dvd, hne1, hneq⟩ - have n0 : 0 < n := lt_of_succ_le (le_of_succ_le n2) - have mn : m < n := lt_of_le_of_ne (le_of_dvd n0 dvd) hneq - refine' (not_prime_iff_minFac_lt n2).mpr _ - refine' lt_of_le_of_lt (minFac_le_of_dvd _ dvd) mn - match m with - | 0 => refine False.elim (hneq (Nat.zero_dvd.mp dvd).symm) - | 1 => contradiction - | m + 2 => simp only [le_add_iff_nonneg_left, _root_.zero_le] - -theorem not_prime_of_dvd2 (n2 : 2 ≤ n) : (∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n) → ¬Prime n := by - intro ⟨m, dvd, hm2, hm⟩ - refine' not_prime_of_dvd n2 ⟨m, ⟨dvd, ⟨_, _⟩⟩⟩ - · exact ne_of_gt (lt_of_succ_le hm2) - · exact ne_of_lt hm +theorem not_prime_of_dvd (h : ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n) : ¬Prime n := by + contrapose! h + simp only [← or_iff_not_imp_left] + exact h.eq_one_or_self_of_dvd + +theorem not_prime_of_dvd2 (h : ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n) : ¬Prime n := by + obtain ⟨m, dvd, hm2, hm⟩ := h + exact not_prime_of_dvd ⟨m, dvd, ne_of_gt hm2, ne_of_lt hm⟩ theorem exists_dvd_iff_not_prime {n : ℕ} (n2 : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := ⟨exists_dvd_of_not_prime n2, not_prime_of_dvd n2⟩ From 4b9eb090fd1e0af4284943ae87ce587b7928875a Mon Sep 17 00:00:00 2001 From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com> Date: Sat, 30 Mar 2024 14:03:41 -0700 Subject: [PATCH 4/9] Fix rebase --- Mathlib/Data/Nat/Prime.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean index 4ce6e1486447d..cb01d6663485b 100644 --- a/Mathlib/Data/Nat/Prime.lean +++ b/Mathlib/Data/Nat/Prime.lean @@ -465,10 +465,10 @@ theorem not_prime_of_dvd2 (h : ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n) : ¬Prime n exact not_prime_of_dvd ⟨m, dvd, ne_of_gt hm2, ne_of_lt hm⟩ theorem exists_dvd_iff_not_prime {n : ℕ} (n2 : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := - ⟨exists_dvd_of_not_prime n2, not_prime_of_dvd n2⟩ + ⟨exists_dvd_of_not_prime n2, not_prime_of_dvd⟩ theorem exists_dvd_iff_not_prime2 {n : ℕ} (n2 : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n := - ⟨exists_dvd_of_not_prime2 n2, not_prime_of_dvd2 n2⟩ + ⟨exists_dvd_of_not_prime2 n2, not_prime_of_dvd2⟩ theorem exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, Prime p ∧ p ∣ n := ⟨minFac n, minFac_prime hn, minFac_dvd _⟩ From fed8b69d258cafbd4e3a368c5ae77e3534519b64 Mon Sep 17 00:00:00 2001 From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com> Date: Mon, 1 Apr 2024 21:35:50 -0700 Subject: [PATCH 5/9] Rename the theorems --- Mathlib/Data/Nat/Prime.lean | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean index cb01d6663485b..c80b1b4745365 100644 --- a/Mathlib/Data/Nat/Prime.lean +++ b/Mathlib/Data/Nat/Prime.lean @@ -455,20 +455,17 @@ theorem exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) : (not_prime_iff_minFac_lt n2).1 np⟩ #align nat.exists_dvd_of_not_prime2 Nat.exists_dvd_of_not_prime2 -theorem not_prime_of_dvd (h : ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n) : ¬Prime n := by - contrapose! h - simp only [← or_iff_not_imp_left] - exact h.eq_one_or_self_of_dvd +theorem not_prime_of_dvd_of_ne {m n : ℕ} (h1 : m ∣ n) (h2 : m ≠ 1) (h3 : m ≠ n) : ¬Prime n := + fun h => Or.elim (h.eq_one_or_self_of_dvd m h1) h2 h3 -theorem not_prime_of_dvd2 (h : ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n) : ¬Prime n := by - obtain ⟨m, dvd, hm2, hm⟩ := h - exact not_prime_of_dvd ⟨m, dvd, ne_of_gt hm2, ne_of_lt hm⟩ +theorem not_prime_of_dvd_of_lt {m n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m < n) : ¬Prime n := + not_prime_of_dvd_of_ne h1 (ne_of_gt h2) (ne_of_lt h3) -theorem exists_dvd_iff_not_prime {n : ℕ} (n2 : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := - ⟨exists_dvd_of_not_prime n2, not_prime_of_dvd⟩ +theorem exists_dvd_ne_iff_not_prime {n : ℕ} (n2 : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := + ⟨exists_dvd_of_not_prime n2, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_ne h1 h2 h3⟩ -theorem exists_dvd_iff_not_prime2 {n : ℕ} (n2 : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n := - ⟨exists_dvd_of_not_prime2 n2, not_prime_of_dvd2⟩ +theorem exists_dvd_lt_iff_not_prime2 {n : ℕ} (n2 : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n := + ⟨exists_dvd_of_not_prime2 n2, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_lt h1 h2 h3⟩ theorem exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, Prime p ∧ p ∣ n := ⟨minFac n, minFac_prime hn, minFac_dvd _⟩ From 71f91afbdab1828fea93924b744e762d6e458ca3 Mon Sep 17 00:00:00 2001 From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com> Date: Mon, 1 Apr 2024 21:38:50 -0700 Subject: [PATCH 6/9] Fix up rename --- Mathlib/Data/Nat/Prime.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean index c80b1b4745365..164036bc56c99 100644 --- a/Mathlib/Data/Nat/Prime.lean +++ b/Mathlib/Data/Nat/Prime.lean @@ -461,11 +461,11 @@ theorem not_prime_of_dvd_of_ne {m n : ℕ} (h1 : m ∣ n) (h2 : m ≠ 1) (h3 : m theorem not_prime_of_dvd_of_lt {m n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m < n) : ¬Prime n := not_prime_of_dvd_of_ne h1 (ne_of_gt h2) (ne_of_lt h3) -theorem exists_dvd_ne_iff_not_prime {n : ℕ} (n2 : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := - ⟨exists_dvd_of_not_prime n2, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_ne h1 h2 h3⟩ +theorem exists_dvd_ne_iff_not_prime {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := + ⟨exists_dvd_of_not_prime h, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_ne h1 h2 h3⟩ -theorem exists_dvd_lt_iff_not_prime2 {n : ℕ} (n2 : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n := - ⟨exists_dvd_of_not_prime2 n2, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_lt h1 h2 h3⟩ +theorem exists_dvd_lt_iff_not_prime {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n := + ⟨exists_dvd_of_not_prime2 h, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_lt h1 h2 h3⟩ theorem exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, Prime p ∧ p ∣ n := ⟨minFac n, minFac_prime hn, minFac_dvd _⟩ From c87b8a6ba25229c36bfa4971ea6341fe5c19ca08 Mon Sep 17 00:00:00 2001 From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com> Date: Mon, 1 Apr 2024 22:20:27 -0700 Subject: [PATCH 7/9] rename the theorem so that the match the actual expr --- Mathlib/Data/Nat/Prime.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean index 164036bc56c99..23d80af85c1d3 100644 --- a/Mathlib/Data/Nat/Prime.lean +++ b/Mathlib/Data/Nat/Prime.lean @@ -461,10 +461,10 @@ theorem not_prime_of_dvd_of_ne {m n : ℕ} (h1 : m ∣ n) (h2 : m ≠ 1) (h3 : m theorem not_prime_of_dvd_of_lt {m n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m < n) : ¬Prime n := not_prime_of_dvd_of_ne h1 (ne_of_gt h2) (ne_of_lt h3) -theorem exists_dvd_ne_iff_not_prime {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := +theorem not_prime_iff_exists_dvd_ne {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := ⟨exists_dvd_of_not_prime h, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_ne h1 h2 h3⟩ -theorem exists_dvd_lt_iff_not_prime {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n := +theorem not_prime_iff_exists_dvd_lt {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n := ⟨exists_dvd_of_not_prime2 h, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_lt h1 h2 h3⟩ theorem exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, Prime p ∧ p ∣ n := From 399921cd55ba80f9057ac799dd10f701c2f96aac Mon Sep 17 00:00:00 2001 From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com> Date: Tue, 2 Apr 2024 09:45:08 -0700 Subject: [PATCH 8/9] Update Mathlib/Data/Nat/Prime.lean style Co-authored-by: damiano --- Mathlib/Data/Nat/Prime.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean index 23d80af85c1d3..cf339f729b30a 100644 --- a/Mathlib/Data/Nat/Prime.lean +++ b/Mathlib/Data/Nat/Prime.lean @@ -462,7 +462,7 @@ theorem not_prime_of_dvd_of_lt {m n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m not_prime_of_dvd_of_ne h1 (ne_of_gt h2) (ne_of_lt h3) theorem not_prime_iff_exists_dvd_ne {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n := - ⟨exists_dvd_of_not_prime h, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_ne h1 h2 h3⟩ + ⟨exists_dvd_of_not_prime h, fun ⟨_, h1, h2, h3⟩ => not_prime_of_dvd_of_ne h1 h2 h3⟩ theorem not_prime_iff_exists_dvd_lt {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n := ⟨exists_dvd_of_not_prime2 h, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_lt h1 h2 h3⟩ From a41bc51a3202c3655adc16623ca407ef0cd0f9c6 Mon Sep 17 00:00:00 2001 From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com> Date: Tue, 2 Apr 2024 09:45:31 -0700 Subject: [PATCH 9/9] Update Mathlib/Data/Nat/Prime.lean style Co-authored-by: damiano --- Mathlib/Data/Nat/Prime.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean index cf339f729b30a..71177230ed072 100644 --- a/Mathlib/Data/Nat/Prime.lean +++ b/Mathlib/Data/Nat/Prime.lean @@ -465,7 +465,7 @@ theorem not_prime_iff_exists_dvd_ne {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ⟨exists_dvd_of_not_prime h, fun ⟨_, h1, h2, h3⟩ => not_prime_of_dvd_of_ne h1 h2 h3⟩ theorem not_prime_iff_exists_dvd_lt {n : ℕ} (h : 2 ≤ n) : (¬Prime n) ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n := - ⟨exists_dvd_of_not_prime2 h, fun ⟨_,h1,h2,h3⟩ => not_prime_of_dvd_of_lt h1 h2 h3⟩ + ⟨exists_dvd_of_not_prime2 h, fun ⟨_, h1, h2, h3⟩ => not_prime_of_dvd_of_lt h1 h2 h3⟩ theorem exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, Prime p ∧ p ∣ n := ⟨minFac n, minFac_prime hn, minFac_dvd _⟩