From 0e834dfe6c83c8035fa12f12971b3df50435ef66 Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Date: Thu, 12 May 2022 16:23:39 +0000
Subject: [PATCH] chore(data/nat/multiplicity): simplify proof (#14103)

---
 src/data/nat/multiplicity.lean | 32 ++++++++++----------------------
 1 file changed, 10 insertions(+), 22 deletions(-)

diff --git a/src/data/nat/multiplicity.lean b/src/data/nat/multiplicity.lean
index 916ba94714d98..9388e5e5dba76 100644
--- a/src/data/nat/multiplicity.lean
+++ b/src/data/nat/multiplicity.lean
@@ -190,28 +190,16 @@ have h₁ : multiplicity p (choose n k) + multiplicity p (k! * (n - k)!) =
   h₁
 
 /-- A lower bound on the multiplicity of `p` in `choose n k`. -/
-lemma multiplicity_le_multiplicity_choose_add {p : ℕ} (hp : p.prime) (n k : ℕ) :
-  multiplicity p n ≤ multiplicity p (choose n k) + multiplicity p k :=
-if hkn : n < k then by simp [choose_eq_zero_of_lt hkn]
-else if hk0 : k = 0 then by simp [hk0]
-else if hn0 : n = 0 then by cases k; simp [hn0, *] at *
-else begin
-  rw [multiplicity_choose hp (le_of_not_gt hkn) (lt_succ_self _),
-    multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) (nat.pos_of_ne_zero hk0)
-      (lt_succ_of_le (log_mono_right (le_of_not_gt hkn))),
-    multiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) (nat.pos_of_ne_zero hn0) (lt_succ_self _),
-    ← nat.cast_add, enat.coe_le_coe],
-  calc ((Ico 1 (log p n).succ).filter (λ i, p ^ i ∣ n)).card
-      ≤ ((Ico 1 (log p n).succ).filter (λ i, p ^ i ≤ k % p ^ i + (n - k) % p ^ i) ∪
-        (Ico 1 (log p n).succ).filter (λ i, p ^ i ∣ k) ).card :
-    card_le_of_subset $ λ i, begin
-      have := @le_mod_add_mod_of_dvd_add_of_not_dvd k (n - k) (p ^ i),
-      simp [add_tsub_cancel_of_le (le_of_not_gt hkn)] at * {contextual := tt},
-      tauto
-    end
-  ... ≤ ((Ico 1 (log p n).succ).filter (λ i, p ^ i ≤ k % p ^ i + (n - k) % p ^ i)).card +
-        ((Ico 1 (log p n).succ).filter (λ i, p ^ i ∣ k)).card :
-    card_union_le _ _
+lemma multiplicity_le_multiplicity_choose_add {p : ℕ} (hp : p.prime) : ∀ (n k : ℕ),
+  multiplicity p n ≤ multiplicity p (choose n k) + multiplicity p k
+| _     0     := by simp
+| 0     (_+1) := by simp
+| (n+1) (k+1) := 
+begin
+  rw ← hp.multiplicity_mul,
+  refine multiplicity_le_multiplicity_of_dvd_right _,
+  rw [← succ_mul_choose_eq],
+  exact dvd_mul_right _ _
 end
 
 lemma multiplicity_choose_prime_pow {p n k : ℕ} (hp : p.prime)