have h_pl_div_fac_part: p^l ∣ (n.factorial / (n - k).factorial) := by
  have h_eq_pl_with_k := exists_eq_mul_right_of_dvd h_pl_div_fac
  have h_eq_pl : ∃ (r : ℕ), r * p^l = n.factorial / (n - k).factorial := by
    cases' h_eq_pl_with_k with j h_eq
    use (j * k.factorial)
    have h_rew : j * k.factorial * p^l = p^l * j * k.factorial := by
      rw [mul_comm, mul_assoc]
    rw [h_rew]
    rw [← h_eq]
    zify
    qify
    field_simp
    rw [mul_comm ((n - k)! : ℚ) _]
    rw [mul_assoc]
  cases' h_eq_pl with j h_eq
  refine' Dvd.intro j _
  rw [mul_comm]
  exact h_eq
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (n - k).factorial / k.factorial
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div'' : ↑k.factorial ∣ ↑n.factorial / ↑(n - k).factorial
h_kfac_ne_zero : ↑k.factorial ≠ 0
h_nkfac_ne_zero : ↑(n - k).factorial ≠ 0
this : ↑k.factorial * ↑(n - k).factorial ≠ 0
h_fraction : n.factorial / (k.factorial * (n - k).factorial) = n.factorial / (n - k).factorial / k.factorial
⊢ p ^ l ∣ n.descFactorial k
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (n - k).factorial / k.factorial
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div'' : ↑k.factorial ∣ ↑n.factorial / ↑(n - k).factorial
h_kfac_ne_zero : ↑k.factorial ≠ 0
h_nkfac_ne_zero : ↑(n - k).factorial ≠ 0
this : ↑k.factorial * ↑(n - k).factorial ≠ 0
h_fraction : n.factorial / (k.factorial * (n - k).factorial) = n.factorial / (n - k).factorial / k.factorial
h_pl_div_fac_part : p ^ l ∣ n.factorial / (n - k).factorial
⊢ p ^ l ∣ n.descFactorial k