feat(data/nat/multiplicity): rename `nat.multiplicity_choose_prime_po…

…w`, add lemmas (#18183)

* Rename `nat.multiplicity_choose_prime_pow` to `nat.multiplicity_choose_prime_pow_add_multiplicity`.
* Add `part_enat.eq_coe_sub_of_add_eq_coe` and a version of `nat.multiplicity_choose_prime_pow` with just the multiplicity of `p` in `choose (p ^ n) k` in the LHS.
* Golf 2 proofs.

src/data/nat/multiplicity.lean

@@ -203,8 +203,8 @@ begin
   exact dvd_mul_right _ _
 end
 
-lemma multiplicity_choose_prime_pow {p n k : ℕ} (hp : p.prime)
-  (hkn : k ≤ p ^ n) (hk0 : 0 < k) :
+lemma multiplicity_choose_prime_pow_add_multiplicity {p n k : ℕ} (hp : p.prime) (hkn : k ≤ p ^ n)
+  (hk0 : k ≠ 0) :
   multiplicity p (choose (p ^ n) k) + multiplicity p k = n :=
 le_antisymm
   (have hdisj : disjoint
@@ -214,7 +214,7 @@ le_antisymm
         {contextual := tt},
   begin
     rw [multiplicity_choose hp hkn (lt_succ_self _),
-      multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0
+      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, part_enat.coe_le_coe, log_pow hp.one_lt,
       ← card_disjoint_union hdisj, filter_union_right],
@@ -224,6 +224,11 @@ le_antisymm
   (by rw [← hp.multiplicity_pow_self];
     exact multiplicity_le_multiplicity_choose_add hp _ _)
 
+lemma multiplicity_choose_prime_pow {p n k : ℕ} (hp : p.prime) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) :
+  multiplicity p (choose (p ^ n) k) =
+    ↑(n - (multiplicity p k).get (finite_nat_iff.2 ⟨hp.ne_one, hk0.bot_lt⟩)) :=
+part_enat.eq_coe_sub_of_add_eq_coe $ multiplicity_choose_prime_pow_add_multiplicity hp hkn hk0
+
 end prime
 
 lemma multiplicity_two_factorial_lt : ∀ {n : ℕ} (h : n ≠ 0), multiplicity 2 n! < n :=

src/data/nat/part_enat.lean

@@ -94,6 +94,8 @@ lemma some_eq_coe (n : ℕ) : some n = n := rfl
 
 @[simp] lemma dom_coe (x : ℕ) : (x : part_enat).dom := trivial
 
+instance : can_lift part_enat ℕ coe dom := ⟨λ n hn, ⟨n.get hn, part.some_get _⟩⟩
+
 instance : has_le part_enat := ⟨λ x y, ∃ h : y.dom → x.dom, ∀ hy : y.dom, x.get (h hy) ≤ y.get hy⟩
 instance : has_top part_enat := ⟨none⟩
 instance : has_bot part_enat := ⟨0⟩
@@ -326,6 +328,15 @@ instance : canonically_ordered_add_monoid part_enat :=
   ..part_enat.order_bot,
   ..part_enat.ordered_add_comm_monoid }
 
+lemma eq_coe_sub_of_add_eq_coe {x y : part_enat} {n : ℕ} (h : x + y = n) :
+  x = ↑(n - y.get (dom_of_le_coe ((le_add_left le_rfl).trans_eq h))) :=
+begin
+  lift x to ℕ using dom_of_le_coe ((le_add_right le_rfl).trans_eq h),
+  lift y to ℕ using dom_of_le_coe ((le_add_left le_rfl).trans_eq h),
+  rw [← nat.cast_add, coe_inj] at h,
+  rw [get_coe, coe_inj, eq_tsub_of_add_eq h]
+end
+
 protected lemma add_lt_add_right {x y z : part_enat} (h : x < y) (hz : z ≠ ⊤) : x + z < y + z :=
 begin
   rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩,

src/ring_theory/witt_vector/frobenius.lean

@@ -121,37 +121,23 @@ lemma map_frobenius_poly.key₁ (n j : ℕ) (hj : j < p ^ (n)) :
   p ^ (n - v p ⟨j + 1, j.succ_pos⟩) ∣ (p ^ n).choose (j + 1) :=
 begin
   apply multiplicity.pow_dvd_of_le_multiplicity,
-  have aux : (multiplicity p ((p ^ n).choose (j + 1))).dom,
-  { rw [← multiplicity.finite_iff_dom, multiplicity.finite_nat_iff],
-    exact ⟨hp.1.ne_one, nat.choose_pos hj⟩, },
-  rw [← part_enat.coe_get aux, part_enat.coe_le_coe, tsub_le_iff_left,
-      ← part_enat.coe_le_coe, nat.cast_add, pnat_multiplicity, part_enat.coe_get,
-      part_enat.coe_get, add_comm],
-  exact (hp.1.multiplicity_choose_prime_pow hj j.succ_pos).ge,
+  rw [hp.out.multiplicity_choose_prime_pow hj j.succ_ne_zero],
+  refl,
 end
 
 /-- A key numerical identity needed for the proof of `witt_vector.map_frobenius_poly`. -/
-lemma map_frobenius_poly.key₂ {n i j : ℕ} (hi : i < n) (hj : j < p ^ (n - i)) :
-  j - (v p ⟨j + 1, j.succ_pos⟩) + n =
-    i + j + (n - i - v p ⟨j + 1, j.succ_pos⟩) :=
+lemma map_frobenius_poly.key₂ {n i j : ℕ} (hi : i ≤ n) (hj : j < p ^ (n - i)) :
+  j - v p ⟨j + 1, j.succ_pos⟩ + n = i + j + (n - i - v p ⟨j + 1, j.succ_pos⟩) :=
 begin
   generalize h : (v p ⟨j + 1, j.succ_pos⟩) = m,
-  suffices : m ≤ n - i ∧ m ≤ j,
-  { rw [tsub_add_eq_add_tsub this.2, add_comm i j,
-      add_tsub_assoc_of_le (this.1.trans (nat.sub_le n i)), add_assoc, tsub_right_comm, add_comm i,
-      tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi.le).mp this.1))] },
-  split,
-  { rw [← h, ← part_enat.coe_le_coe, pnat_multiplicity, part_enat.coe_get,
-        ← hp.1.multiplicity_choose_prime_pow hj j.succ_pos],
-    apply le_add_left, refl },
-  { obtain ⟨c, hc⟩ : p ^ m ∣ j + 1,
-    { rw [← h], exact multiplicity.pow_multiplicity_dvd _, },
-    obtain ⟨c, rfl⟩ : ∃ k : ℕ, c = k + 1,
-    { apply nat.exists_eq_succ_of_ne_zero, rintro rfl, simpa only using hc },
-    rw [mul_add, mul_one] at hc,
-    apply nat.le_of_lt_succ,
-    calc m < p ^ m : nat.lt_pow_self hp.1.one_lt m
-       ... ≤ j + 1 : by { rw ← tsub_eq_of_eq_add_rev hc, apply nat.sub_le } }
+  rsuffices ⟨h₁, h₂⟩ : m ≤ n - i ∧ m ≤ j,
+  { rw [tsub_add_eq_add_tsub h₂, add_comm i j,
+      add_tsub_assoc_of_le (h₁.trans (nat.sub_le n i)), add_assoc, tsub_right_comm, add_comm i,
+      tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))] },
+  have hle : p ^ m ≤ j + 1,
+    from h ▸ nat.le_of_dvd j.succ_pos (multiplicity.pow_multiplicity_dvd _),
+  exact ⟨(pow_le_pow_iff hp.1.one_lt).1 (hle.trans hj),
+    nat.le_of_lt_succ ((nat.lt_pow_self hp.1.one_lt m).trans_le hle)⟩
 end
 
 lemma map_frobenius_poly (n : ℕ) :
@@ -200,7 +186,7 @@ begin
   { have aux : ∀ k : ℕ, (p ^ k : ℚ) ≠ 0,
     { intro, apply pow_ne_zero, exact_mod_cast hp.1.ne_zero },
     simpa [aux, -one_div] with field_simps using this.symm },
-  rw [mul_comm _ (p : ℚ), mul_assoc, mul_assoc, ← pow_add, map_frobenius_poly.key₂ p hi hj],
+  rw [mul_comm _ (p : ℚ), mul_assoc, mul_assoc, ← pow_add, map_frobenius_poly.key₂ p hi.le hj],
   ring_exp
 end