[Merged by Bors] - feat: port Data.Nat.Multiplicity

Mathlib/Data/Nat/Multiplicity.lean

@@ -25,19 +25,19 @@ coefficients.
 
 ## Multiplicity calculations
 
-* `nat.multiplicity_factorial`: Legendre's Theorem. The multiplicity of `p` in `n!` is
+* `Nat.multiplicity_factorial`: Legendre's Theorem. The multiplicity of `p` in `n!` is
   `n/p + ... + n/p^b` for any `b` such that `n/p^(b + 1) = 0`.
-* `nat.multiplicity_factorial_mul`: The multiplicity of `p` in `(p * n)!` is `n` more than that of
+* `Nat.multiplicity_factorial_mul`: The multiplicity of `p` in `(p * n)!` is `n` more than that of
   `n!`.
-* `nat.multiplicity_choose`: The multiplicity of `p` in `n.choose k` is the number of carries when
+* `Nat.multiplicity_choose`: The multiplicity of `p` in `n.choose k` is the number of carries when
   `k` and`n - k` are added in base `p`.
 
 ## Other declarations
 
-* `nat.multiplicity_eq_card_pow_dvd`: The multiplicity of `m` in `n` is the number of positive
+* `Nat.multiplicity_eq_card_pow_dvd`: The multiplicity of `m` in `n` is the number of positive
   natural numbers `i` such that `m ^ i` divides `n`.
-* `nat.multiplicity_two_factorial_lt`: The multiplicity of `2` in `n!` is strictly less than `n`.
-* `nat.prime.multiplicity_something`: Specialization of `multiplicity.something` to a prime in the
+* `Nat.multiplicity_two_factorial_lt`: The multiplicity of `2` in `n!` is strictly less than `n`.
+* `Nat.prime.multiplicity_something`: Specialization of `multiplicity.something` to a prime in the
   naturals. Avoids having to provide `p ≠ 1` and other trivialities, along with translating between
   `prime` and `nat.prime`.
 
@@ -57,49 +57,46 @@ namespace Nat
 divides `n`. This set is expressed by filtering `Ico 1 b` where `b` is any bound greater than
 `log m n`. -/
 theorem multiplicity_eq_card_pow_dvd {m n b : ℕ} (hm : m ≠ 1) (hn : 0 < n) (hb : log m n < b) :
-    multiplicity m n = ↑((Finset.Ico 1 b).filterₓ fun i => m ^ i ∣ n).card :=
+    multiplicity m n = ↑((Finset.Ico 1 b).filter fun i => m ^ i ∣ n).card :=
   calc
     multiplicity m n = ↑(Ico 1 <| (multiplicity m n).get (finite_nat_iff.2 ⟨hm, hn⟩) + 1).card := by
       simp
-    _ = ↑((Finset.Ico 1 b).filterₓ fun i => m ^ i ∣ n).card :=
-      congr_arg coe <|
+    _ = ↑((Finset.Ico 1 b).filter fun i => m ^ i ∣ n).card :=
+      congr_arg _ <|
         congr_arg card <|
-          Finset.ext fun i =>
-            by
+          Finset.ext fun i => by
             rw [mem_filter, mem_Ico, mem_Ico, lt_succ_iff, ← @PartENat.coe_le_coe i,
               PartENat.natCast_get, ← pow_dvd_iff_le_multiplicity, and_right_comm]
             refine' (and_iff_left_of_imp fun h => lt_of_le_of_lt _ hb).symm
-            cases m
-            · rw [zero_pow, zero_dvd_iff] at h
-              exacts[(hn.ne' h.2).elim, h.1]
-            exact
-              le_log_of_pow_le (one_lt_iff_ne_zero_and_ne_one.2 ⟨m.succ_ne_zero, hm⟩)
+            cases' m with m
+            · rw [zero_eq, zero_pow, zero_dvd_iff] at h
+              exacts [(hn.ne' h.2).elim, h.1]
+            exact le_log_of_pow_le (one_lt_iff_ne_zero_and_ne_one.2 ⟨m.succ_ne_zero, hm⟩)
                 (le_of_dvd hn h.2)
-
 #align nat.multiplicity_eq_card_pow_dvd Nat.multiplicity_eq_card_pow_dvd
 
 namespace Prime
 
 theorem multiplicity_one {p : ℕ} (hp : p.Prime) : multiplicity p 1 = 0 :=
-  multiplicity.one_right hp.Prime.not_unit
+  multiplicity.one_right hp.prime.not_unit
 #align nat.prime.multiplicity_one Nat.Prime.multiplicity_one
 
 theorem multiplicity_mul {p m n : ℕ} (hp : p.Prime) :
     multiplicity p (m * n) = multiplicity p m + multiplicity p n :=
-  multiplicity.mul hp.Prime
+  multiplicity.mul hp.prime
 #align nat.prime.multiplicity_mul Nat.Prime.multiplicity_mul
 
 theorem multiplicity_pow {p m n : ℕ} (hp : p.Prime) :
     multiplicity p (m ^ n) = n • multiplicity p m :=
-  multiplicity.pow hp.Prime
+  multiplicity.pow hp.prime
 #align nat.prime.multiplicity_pow Nat.Prime.multiplicity_pow
 
 theorem multiplicity_self {p : ℕ} (hp : p.Prime) : multiplicity p p = 1 :=
-  multiplicity_self hp.Prime.not_unit hp.NeZero
+  multiplicity.multiplicity_self hp.prime.not_unit hp.ne_zero
 #align nat.prime.multiplicity_self Nat.Prime.multiplicity_self
 
 theorem multiplicity_pow_self {p n : ℕ} (hp : p.Prime) : multiplicity p (p ^ n) = n :=
-  multiplicity_pow_self hp.NeZero hp.Prime.not_unit n
+  multiplicity.multiplicity_pow_self hp.ne_zero hp.prime.not_unit n
 #align nat.prime.multiplicity_pow_self Nat.Prime.multiplicity_pow_self
 
 /-- **Legendre's Theorem**
@@ -108,24 +105,20 @@ The multiplicity of a prime in `n!` is the sum of the quotients `n / p ^ i`. Thi
 over the finset `Ico 1 b` where `b` is any bound greater than `log p n`. -/
 theorem multiplicity_factorial {p : ℕ} (hp : p.Prime) :
     ∀ {n b : ℕ}, log p n < b → multiplicity p n ! = (∑ i in Ico 1 b, n / p ^ i : ℕ)
-  | 0, b, hb => by simp [Ico, hp.multiplicity_one]
+  | 0, b, _ => by simp [Ico, hp.multiplicity_one]
   | n + 1, b, hb =>
     calc
       multiplicity p (n + 1)! = multiplicity p n ! + multiplicity p (n + 1) := by
         rw [factorial_succ, hp.multiplicity_mul, add_comm]
-      _ =
-          (∑ i in Ico 1 b, n / p ^ i : ℕ) +
-            ((Finset.Ico 1 b).filterₓ fun i => p ^ i ∣ n + 1).card :=
-        by
-        rw [multiplicity_factorial ((log_mono_right <| le_succ _).trans_lt hb), ←
+      _ = (∑ i in Ico 1 b, n / p ^ i : ℕ) +
+            ((Finset.Ico 1 b).filter fun i => p ^ i ∣ n + 1).card := by
+        rw [multiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), ←
           multiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]
-      _ = (∑ i in Ico 1 b, n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0 : ℕ) :=
-        by
+      _ = (∑ i in Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0) : ℕ) := by
         rw [sum_add_distrib, sum_boole]
         simp
       _ = (∑ i in Ico 1 b, (n + 1) / p ^ i : ℕ) :=
-        congr_arg coe <| Finset.sum_congr rfl fun _ _ => (succ_div _ _).symm
-
+        congr_arg _ <| Finset.sum_congr rfl fun _ _ => (succ_div _ _).symm
 #align nat.prime.multiplicity_factorial Nat.Prime.multiplicity_factorial
 
 /-- The multiplicity of `p` in `(p * (n + 1))!` is one more than the sum
@@ -139,13 +132,11 @@ theorem multiplicity_factorial_mul_succ {n p : ℕ} (hp : p.Prime) :
   linarith
   have h3 : p * n + 1 ≤ p * (n + 1) + 1
   linarith
-  have hm : multiplicity p (p * n)! ≠ ⊤ :=
-    by
+  have hm : multiplicity p (p * n)! ≠ ⊤ := by
     rw [Ne.def, eq_top_iff_not_finite, Classical.not_not, finite_nat_iff]
     exact ⟨hp.ne_one, factorial_pos _⟩
   revert hm
-  have h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), multiplicity p m = 0 :=
-    by
+  have h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), multiplicity p m = 0 := by
     intro m hm
     rw [multiplicity_eq_zero, ← not_dvd_iff_between_consec_multiples _ hp.pos]
     rw [mem_Ico] at hm
@@ -184,40 +175,37 @@ theorem multiplicity_factorial_le_div_pred {p : ℕ} (hp : p.Prime) (n : ℕ) :
 theorem multiplicity_choose_aux {p n b k : ℕ} (hp : p.Prime) (hkn : k ≤ n) :
     (∑ i in Finset.Ico 1 b, n / p ^ i) =
       ((∑ i in Finset.Ico 1 b, k / p ^ i) + ∑ i in Finset.Ico 1 b, (n - k) / p ^ i) +
-        ((Finset.Ico 1 b).filterₓ fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i).card :=
+        ((Finset.Ico 1 b).filter fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i).card :=
   calc
     (∑ i in Finset.Ico 1 b, n / p ^ i) = ∑ i in Finset.Ico 1 b, (k + (n - k)) / p ^ i := by
       simp only [add_tsub_cancel_of_le hkn]
-    _ =
-        ∑ i in Finset.Ico 1 b,
-          k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0 :=
+    _ = ∑ i in Finset.Ico 1 b,
+          (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0) :=
       by simp only [Nat.add_div (pow_pos hp.pos _)]
     _ = _ := by simp [sum_add_distrib, sum_boole]
-    
+
 #align nat.prime.multiplicity_choose_aux Nat.Prime.multiplicity_choose_aux
 
 /-- The multiplicity of `p` in `choose n k` is the number of carries when `k` and `n - k`
   are added in base `p`. The set is expressed by filtering `Ico 1 b` where `b`
   is any bound greater than `log p n`. -/
 theorem multiplicity_choose {p n k b : ℕ} (hp : p.Prime) (hkn : k ≤ n) (hnb : log p n < b) :
     multiplicity p (choose n k) =
-      ((Ico 1 b).filterₓ fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i).card :=
+      ((Ico 1 b).filter fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i).card := by
   have h₁ :
     multiplicity p (choose n k) + multiplicity p (k ! * (n - k)!) =
-      ((Finset.Ico 1 b).filterₓ fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i).card +
-        multiplicity p (k ! * (n - k)!) :=
-    by
+      ((Finset.Ico 1 b).filter fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i).card +
+        multiplicity p (k ! * (n - k)!) := by
     rw [← hp.multiplicity_mul, ← mul_assoc, choose_mul_factorial_mul_factorial hkn,
       hp.multiplicity_factorial hnb, hp.multiplicity_mul,
       hp.multiplicity_factorial ((log_mono_right hkn).trans_lt hnb),
       hp.multiplicity_factorial (lt_of_le_of_lt (log_mono_right tsub_le_self) hnb),
       multiplicity_choose_aux hp hkn]
     simp [add_comm]
-  (PartENat.add_right_cancel_iff
-        (PartENat.ne_top_iff_dom.2 <|
-          finite_nat_iff.2
-            ⟨ne_of_gt hp.one_lt, mul_pos (factorial_pos k) (factorial_pos (n - k))⟩)).1
-    h₁
+  refine (PartENat.add_right_cancel_iff ?_).1 h₁
+  apply PartENat.ne_top_iff_dom.2
+  apply finite_nat_iff.2
+            ⟨ne_of_gt hp.one_lt, mul_pos (factorial_pos k) (factorial_pos (n - k))⟩
 #align nat.prime.multiplicity_choose Nat.Prime.multiplicity_choose
 
 /-- A lower bound on the multiplicity of `p` in `choose n k`. -/
@@ -239,19 +227,19 @@ theorem multiplicity_choose_prime_pow_add_multiplicity (hp : p.Prime) (hkn : k 
   le_antisymm
     (by
       have hdisj :
-        Disjoint ((Ico 1 n.succ).filterₓ fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i)
-          ((Ico 1 n.succ).filterₓ fun i => p ^ i ∣ k) :=
-        by
+        Disjoint ((Ico 1 n.succ).filter fun i => p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i)
+          ((Ico 1 n.succ).filter fun i => p ^ i ∣ k) := by
         simp (config := { contextual := true }) [disjoint_right, *, dvd_iff_mod_eq_zero,
           Nat.mod_lt _ (pow_pos hp.pos _)]
       rw [multiplicity_choose hp hkn (lt_succ_self _),
         multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0.bot_lt
           (lt_succ_of_le (log_mono_right hkn)),
         ← Nat.cast_add, PartENat.coe_le_coe, log_pow hp.one_lt, ← card_disjoint_union hdisj,
         filter_union_right]
-      have filter_le_Ico := (Ico 1 n.succ).card_filter_le _
+      have filter_le_Ico := (Ico 1 n.succ).card_filter_le 
+        fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k
       rwa [card_Ico 1 n.succ] at filter_le_Ico)
-    (by rw [← hp.multiplicity_pow_self] <;> exact multiplicity_le_multiplicity_choose_add hp _ _)
+    (by rw [← hp.multiplicity_pow_self]; exact multiplicity_le_multiplicity_choose_add hp _ _)
 #align nat.prime.multiplicity_choose_prime_pow_add_multiplicity Nat.Prime.multiplicity_choose_prime_pow_add_multiplicity
 
 theorem multiplicity_choose_prime_pow {p n k : ℕ} (hp : p.Prime) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) :
@@ -272,22 +260,24 @@ theorem dvd_choose_pow (hp : Prime p) (hk : k ≠ 0) (hkp : k ≠ p ^ n) : p ∣
 
 theorem dvd_choose_pow_iff (hp : Prime p) : p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n := by
   refine' ⟨fun h => ⟨_, _⟩, fun h => dvd_choose_pow hp h.1 h.2⟩ <;> rintro rfl <;>
-    simpa [hp.ne_one] using h
+    simp [hp.ne_one] at h
 #align nat.prime.dvd_choose_pow_iff Nat.Prime.dvd_choose_pow_iff
 
 end Prime
 
-theorem multiplicity_two_factorial_lt : ∀ {n : ℕ} (h : n ≠ 0), multiplicity 2 n ! < n := by
+theorem multiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), multiplicity 2 n ! < n := by
   have h2 := prime_two.prime
-  refine' binary_rec _ _
-  · contradiction
+  refine' binaryRec _ _
+  · exact fun h => False.elim <| h rfl
   · intro b n ih h
     by_cases hn : n = 0
     · subst hn
       simp at h
       simp [h, one_right h2.not_unit]
-    have : multiplicity 2 (2 * n)! < (2 * n : ℕ) :=
-      by
+      rw [Prime.multiplicity_one]
+      simp only [zero_lt_one]
+      decide
+    have : multiplicity 2 (2 * n)! < (2 * n : ℕ) := by
       rw [prime_two.multiplicity_factorial_mul]
       refine' (PartENat.add_lt_add_right (ih hn) (PartENat.natCast_ne_top _)).trans_le _
       rw [two_mul]
@@ -303,4 +293,3 @@ theorem multiplicity_two_factorial_lt : ∀ {n : ℕ} (h : n ≠ 0), multiplicit
 #align nat.multiplicity_two_factorial_lt Nat.multiplicity_two_factorial_lt
 
 end Nat
-