feat(data/nat/basic, data/nat/prime): add various lemmas (#7171)

src/algebra/ordered_ring.lean

@@ -139,6 +139,14 @@ lemma le_mul_of_one_le_left (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a * b :=
 suffices 1 * b ≤ a * b, by rwa one_mul at this,
 mul_le_mul_of_nonneg_right h hb
 
+lemma lt_mul_of_one_lt_right (hb : 0 < b) (h : 1 < a) : b < b * a :=
+suffices b * 1 < b * a, by rwa mul_one at this,
+mul_lt_mul' (le_refl _) h zero_le_one hb
+
+lemma lt_mul_of_one_lt_left (hb : 0 < b) (h : 1 < a) : b < a * b :=
+suffices 1 * b < a * b, by rwa one_mul at this,
+mul_lt_mul h (le_refl _) hb (zero_le_one.trans h.le)
+
 lemma add_le_mul_two_add {a b : α}
   (a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b) :=
 calc a + (2 + b) ≤ a + (a + a * b) :
@@ -458,9 +466,6 @@ lemma lt_mul_iff_one_lt_right (hb : 0 < b) : b < b * a ↔ 1 < a :=
 suffices b * 1 < b * a ↔ 1 < a, by rwa mul_one at this,
 mul_lt_mul_left hb
 
-lemma lt_mul_of_one_lt_right (hb : 0 < b) : 1 < a → b < b * a :=
-(lt_mul_iff_one_lt_right hb).2
-
 theorem mul_nonneg_iff_right_nonneg_of_pos (h : 0 < a) : 0 ≤ b * a ↔ 0 ≤ b :=
 ⟨assume : 0 ≤ b * a, nonneg_of_mul_nonneg_right this h, assume : 0 ≤ b, mul_nonneg this h.le⟩
 

src/data/nat/basic.lean

@@ -947,6 +947,15 @@ nat.dvd_add_right (dvd_refl m)
   m ∣ n + m ↔ m ∣ n :=
 nat.dvd_add_left (dvd_refl m)
 
+-- TODO: update `nat.dvd_sub` in core
+lemma dvd_sub' {k m n : ℕ} (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=
+begin
+  cases le_total n m with H H,
+  { exact dvd_sub H h₁ h₂ },
+  { rw nat.sub_eq_zero_of_le H,
+    exact dvd_zero k },
+end
+
 lemma not_dvd_of_pos_of_lt {a b : ℕ} (h1 : 0 < b) (h2 : b < a) : ¬ a ∣ b :=
 begin
   rintros ⟨c, rfl⟩,
@@ -1263,6 +1272,9 @@ strict_mono.lt_iff_lt (pow_left_strict_mono k)
 lemma pow_left_injective {m : ℕ} (k : 1 ≤ m) : function.injective (λ (x : ℕ), x^m) :=
 strict_mono.injective (pow_left_strict_mono k)
 
+theorem pow_two_sub_pow_two (a b : ℕ) : a ^ 2 - b ^ 2 = (a + b) * (a - b) :=
+by { rw [pow_two, pow_two], exact nat.mul_self_sub_mul_self_eq a b }
+
 /-! ### `pow` and `mod` / `dvd` -/
 
 theorem mod_pow_succ {b : ℕ} (b_pos : 0 < b) (w m : ℕ)

src/data/nat/prime.lean

@@ -370,15 +370,15 @@ def factors : ℕ → list ℕ
   let m := min_fac n in have n / m < n := factors_lemma,
   m :: factors (n / m)
 
-lemma mem_factors : ∀ {n p}, p ∈ factors n → prime p
+lemma prime_of_mem_factors : ∀ {n p}, p ∈ factors n → prime p
 | 0       := λ p, false.elim
 | 1       := λ p, false.elim
 | n@(k+2) := λ p h,
   let m := min_fac n in have n / m < n := factors_lemma,
   have h₁ : p = m ∨ p ∈ (factors (n / m)) :=
     (list.mem_cons_iff _ _ _).1 h,
   or.cases_on h₁ (λ h₂, h₂.symm ▸ min_fac_prime dec_trivial)
-    mem_factors
+    prime_of_mem_factors
 
 lemma prod_factors : ∀ {n}, 0 < n → list.prod (factors n) = n
 | 0       := (lt_irrefl _).elim
@@ -538,7 +538,11 @@ lemma mem_list_primes_of_dvd_prod {p : ℕ} (hp : prime p) :
 
 lemma mem_factors_iff_dvd {n p : ℕ} (hn : 0 < n) (hp : prime p) : p ∈ factors n ↔ p ∣ n :=
 ⟨λ h, prod_factors hn ▸ list.dvd_prod h,
- λ h, mem_list_primes_of_dvd_prod hp (@mem_factors n) ((prod_factors hn).symm ▸ h)⟩
+ λ h, mem_list_primes_of_dvd_prod hp (@prime_of_mem_factors n) ((prod_factors hn).symm ▸ h)⟩
+
+lemma mem_factors {n p} (hn : 0 < n) : p ∈ factors n ↔ prime p ∧ p ∣ n :=
+⟨λ h, ⟨prime_of_mem_factors h, (mem_factors_iff_dvd hn $ prime_of_mem_factors h).mp h⟩,
+ λ ⟨hprime, hdvd⟩, (mem_factors_iff_dvd hn hprime).mpr hdvd⟩
 
 lemma perm_of_prod_eq_prod : ∀ {l₁ l₂ : list ℕ}, prod l₁ = prod l₂ →
   (∀ p ∈ l₁, prime p) → (∀ p ∈ l₂, prime p) → l₁ ~ l₂
@@ -570,7 +574,7 @@ have hn : 0 < n := nat.pos_of_ne_zero $ λ h, begin
     exact nat.mul_ne_zero (ne_of_lt (prime.pos (h₂ a (mem_cons_self _ _)))).symm
       (hi (λ p hp, h₂ p (mem_cons_of_mem _ hp))) h₁ }
 end,
-perm_of_prod_eq_prod (by rwa prod_factors hn) h₂ (@mem_factors _)
+perm_of_prod_eq_prod (by rwa prod_factors hn) h₂ (@prime_of_mem_factors _)
 
 end
 

src/data/padics/padic_norm.lean

@@ -467,7 +467,7 @@ begin
   { intros, assumption },
   { intros p hp hpn,
     rw [multiset.mem_to_finset, multiset.mem_coe] at hp,
-    haveI Hp : fact p.prime := ⟨mem_factors hp⟩,
+    haveI Hp : fact p.prime := ⟨prime_of_mem_factors hp⟩,
     simp only [exists_prop, ne.def, finset.mem_filter, finset.mem_range],
     refine ⟨p, ⟨_, Hp.1⟩, ⟨_, rfl⟩⟩,
     { rw mem_factors_iff_dvd hn Hp.1 at hp, exact lt_of_le_of_lt (le_of_dvd hn hp) pr },

src/data/pnat/factors.lean

@@ -193,7 +193,7 @@ namespace pnat
 
 /-- The prime factors of n, regarded as a multiset -/
 def factor_multiset (n : ℕ+) : prime_multiset :=
-prime_multiset.of_nat_list (nat.factors n) (@nat.mem_factors n)
+prime_multiset.of_nat_list (nat.factors n) (@nat.prime_of_mem_factors n)
 
 /-- The product of the factors is the original number -/
 theorem prod_factor_multiset (n : ℕ+) : (factor_multiset n).prod = n :=
@@ -203,7 +203,7 @@ eq $ by { dsimp [factor_multiset],
 
 theorem coe_nat_factor_multiset (n : ℕ+) :
   ((factor_multiset n) : (multiset ℕ)) = ((nat.factors n) : multiset ℕ) :=
-prime_multiset.to_of_nat_multiset (nat.factors n) (@nat.mem_factors n)
+prime_multiset.to_of_nat_multiset (nat.factors n) (@nat.prime_of_mem_factors n)
 
 end pnat
 

src/number_theory/arithmetic_function.lean

@@ -648,7 +648,7 @@ begin
     simp },
   rcases list.length_eq_one.1 h with ⟨x, hx⟩,
   rw [← prod_factors n.succ_pos, hx, list.prod_singleton],
-  apply mem_factors,
+  apply prime_of_mem_factors,
   rw [hx, list.mem_singleton]
 end
 

src/ring_theory/int/basic.lean

@@ -308,7 +308,7 @@ begin
   { apply_instance },
   { intros x hx,
     rw [nat.irreducible_iff_prime, ← nat.prime_iff],
-    apply nat.mem_factors hx, }
+    exact nat.prime_of_mem_factors hx }
 end
 
 lemma nat.factors_multiset_prod_of_irreducible