feat(number_theory/divisors): add filter_dvd_eq_proper_divisors (#1…

…4049)

Adds `filter_dvd_eq_proper_divisors` and golfs `filter_dvd_eq_divisors` and a few other lemmas

src/number_theory/divisors.lean

@@ -49,23 +49,32 @@ def divisors_antidiagonal : finset (ℕ × ℕ) :=
 
 variable {n}
 
-lemma proper_divisors.not_self_mem : ¬ n ∈ proper_divisors n :=
+@[simp]
+lemma filter_dvd_eq_divisors (h : n ≠ 0) :
+  (finset.range n.succ).filter (∣ n) = n.divisors :=
+begin
+  ext,
+  simp only [divisors, mem_filter, mem_range, mem_Ico, and.congr_left_iff, iff_and_self],
+  exact λ ha _, succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt),
+end
+
+@[simp]
+lemma filter_dvd_eq_proper_divisors (h : n ≠ 0) :
+  (finset.range n).filter (∣ n) = n.proper_divisors :=
 begin
-  rw proper_divisors,
-  simp,
+  ext,
+  simp only [proper_divisors, mem_filter, mem_range, mem_Ico, and.congr_left_iff, iff_and_self],
+  exact λ ha _, succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt),
 end
 
+lemma proper_divisors.not_self_mem : ¬ n ∈ proper_divisors n :=
+by simp [proper_divisors]
+
 @[simp]
 lemma mem_proper_divisors {m : ℕ} : n ∈ proper_divisors m ↔ n ∣ m ∧ n < m :=
 begin
-  rw [proper_divisors, finset.mem_filter, finset.mem_Ico, and_comm],
-  apply and_congr_right,
-  rw and_iff_right_iff_imp,
-  intros hdvd hlt,
-  apply nat.pos_of_ne_zero _,
-  rintro rfl,
-  rw zero_dvd_iff.1 hdvd at hlt,
-  apply lt_irrefl 0 hlt,
+  rcases eq_or_ne m 0 with rfl | hm, { simp [proper_divisors] },
+  simp only [and_comm, ←filter_dvd_eq_proper_divisors hm, mem_filter, mem_range],
 end
 
 lemma divisors_eq_proper_divisors_insert_self_of_pos (h : 0 < n):
@@ -74,21 +83,12 @@ by rw [divisors, proper_divisors, Ico_succ_right_eq_insert_Ico h, finset.filter_
   if_pos (dvd_refl n)]
 
 @[simp]
-lemma mem_divisors {m : ℕ} :
-  n ∈ divisors m ↔ (n ∣ m ∧ m ≠ 0) :=
+lemma mem_divisors {m : ℕ} : n ∈ divisors m ↔ (n ∣ m ∧ m ≠ 0) :=
 begin
-  cases m,
-  { simp [divisors] },
-  simp only [divisors, finset.mem_Ico, ne.def, finset.mem_filter, succ_ne_zero, and_true,
-             and_iff_right_iff_imp, not_false_iff],
-  intro hdvd,
-  split,
-  { apply nat.pos_of_ne_zero,
-    rintro rfl,
-    apply nat.succ_ne_zero,
-    rwa zero_dvd_iff at hdvd },
-  { rw nat.lt_succ_iff,
-    apply nat.le_of_dvd (nat.succ_pos m) hdvd }
+  rcases eq_or_ne m 0 with rfl | hm, { simp [divisors] },
+  simp only [hm, ne.def, not_false_iff, and_true, ←filter_dvd_eq_divisors hm, mem_filter,
+    mem_range, and_iff_right_iff_imp, lt_succ_iff],
+  exact le_of_dvd hm.bot_lt,
 end
 
 lemma mem_divisors_self (n : ℕ) (h : n ≠ 0) : n ∈ n.divisors := mem_divisors.2 ⟨dvd_rfl, h⟩
@@ -170,10 +170,7 @@ end
 lemma pos_of_mem_divisors {m : ℕ} (h : m ∈ n.divisors) : 0 < m :=
 begin
   cases m,
-  { rw [mem_divisors, zero_dvd_iff] at h,
-    rcases h with ⟨rfl, h⟩,
-    exfalso,
-    apply h rfl },
+  { rw [mem_divisors, zero_dvd_iff] at h, cases h.2 h.1 },
   apply nat.succ_pos,
 end
 
@@ -414,17 +411,6 @@ begin
   exact prod_divisors_antidiagonal (λ i j, f j i),
 end
 
-@[simp]
-lemma filter_dvd_eq_divisors {n : ℕ} (h : n ≠ 0) :
-  finset.filter (λ (x : ℕ), x ∣ n) (finset.range (n : ℕ).succ) = (n : ℕ).divisors :=
-begin
-  apply finset.ext,
-  simp only [h, mem_filter, and_true, and_iff_right_iff_imp, cast_id, mem_range, ne.def,
-  not_false_iff, mem_divisors],
-  intros a ha,
-  exact nat.lt_succ_of_le (nat.divisor_le (nat.mem_divisors.2 ⟨ha, h⟩))
-end
-
 /-- The factors of `n` are the prime divisors -/
 lemma prime_divisors_eq_to_filter_divisors_prime (n : ℕ) :
   n.factors.to_finset = (divisors n).filter prime :=