Theorem: chapter03.prime_div_descFactorial (FormalBook/Chapter_03.lean)

State before:
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
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_p_div_ml : p ∣ m^l := by
  rw [← H]
  exact h_p_div_binom
State after:
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
⊢ p ^ l ∣ n.descFactorial k

State before:
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
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_pl_div_ml : p^l ∣ m^l := by
  exact pow_dvd_pow_of_dvd (Nat.Prime.dvd_of_dvd_pow (h_p) (h_p_div_ml)) l
State after:
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
⊢ p ^ l ∣ n.descFactorial k

State before:
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
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_pl_div_binom : p^l ∣ choose n k := by
  rw [H]
  exact h_pl_div_ml
State after:
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
⊢ p ^ l ∣ n.descFactorial k

State before:
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
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_pl_div_fac : p^l ∣  (n.factorial / (k.factorial * (n-k).factorial)) := by
  rw [← Nat.choose_eq_factorial_div_factorial h_klen]
  exact h_pl_div_binom
State after:
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 / (k.factorial * (n - k).factorial)
⊢ p ^ l ∣ n.descFactorial k

State before:
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 / (k.factorial * (n - k).factorial)
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_fac_div : ((↑k ! * ↑(n - k)!) : ℤ)  ∣ (n ! : ℤ) := by
  norm_cast
  exact factorial_mul_factorial_dvd_factorial h_klen
State after:
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 / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
⊢ p ^ l ∣ n.descFactorial k

State before:
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 / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_fac_div' : ↑(n - k)! ∣ (n ! : ℤ) := dvd_of_mul_left_dvd h_fac_div
State after:
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 / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
⊢ p ^ l ∣ n.descFactorial k

State before:
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 / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_fac_div'' : (k ! : ℤ) ∣ (↑n ! / ↑(n - k)!) := by
  norm_cast
  refine' (dvd_div_iff ((Int.coe_nat_dvd).mp h_fac_div')).mpr _
  norm_cast at h_fac_div
  rw [mul_comm]
  exact h_fac_div
State after:
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 / (k.factorial * (n - 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
⊢ p ^ l ∣ n.descFactorial k

State before:
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 / (k.factorial * (n - 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
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_kfac_ne_zero : (k ! : ℚ) ≠ 0 := cast_ne_zero.mpr (factorial_ne_zero k)
State after:
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 / (k.factorial * (n - 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
⊢ p ^ l ∣ n.descFactorial k

State before:
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 / (k.factorial * (n - 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
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_nkfac_ne_zero : ((n - k)! : ℚ) ≠ 0 := cast_ne_zero.mpr (n - k).factorial_ne_zero
State after:
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 / (k.factorial * (n - 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
⊢ p ^ l ∣ n.descFactorial k

State before:
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 / (k.factorial * (n - 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
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have : (k ! * (n - k)! : ℚ) ≠ 0 := mul_ne_zero h_kfac_ne_zero h_nkfac_ne_zero
State after:
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 / (k.factorial * (n - 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
⊢ p ^ l ∣ n.descFactorial k

State before:
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 / (k.factorial * (n - 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
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_fraction: (n.factorial / (k.factorial * (n - k).factorial)) =
  (n.factorial / (n - k).factorial) / k.factorial := by
  zify
  qify
  field_simp
  rw [mul_comm]
  left
  rfl
State after:
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 / (k.factorial * (n - 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

State before:
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 / (k.factorial * (n - 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
Tactic:
rw [h_fraction] at h_pl_div_fac
State after:
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

State before:
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
Tactic:
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
State after:
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

State before:
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
Tactic:
rw [descFactorial_eq_div h_klen]
State after:
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.factorial / (n - k).factorial

State before:
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.factorial / (n - k).factorial
Tactic:
convert h_pl_div_fac_part
State after:
no goals

State before:
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
⊢ p ∣ m ^ l
Tactic:
rw [← H]
State after:
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
⊢ p ∣ n.choose k

State before:
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
⊢ p ∣ n.choose k
Tactic:
exact h_p_div_binom
State after:
no goals

State before:
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
⊢ p ^ l ∣ m ^ l
Tactic:
exact pow_dvd_pow_of_dvd (Nat.Prime.dvd_of_dvd_pow (h_p) (h_p_div_ml)) l
State after:
no goals

State before:
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
⊢ p ^ l ∣ n.choose k
Tactic:
rw [H]
State after:
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
⊢ p ^ l ∣ m ^ l

State before:
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
⊢ p ^ l ∣ m ^ l
Tactic:
exact h_pl_div_ml
State after:
no goals

State before:
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
⊢ p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
Tactic:
rw [← Nat.choose_eq_factorial_div_factorial h_klen]
State after:
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
⊢ p ^ l ∣ n.choose k

State before:
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
⊢ p ^ l ∣ n.choose k
Tactic:
exact h_pl_div_binom
State after:
no goals

State before:
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 / (k.factorial * (n - k).factorial)
⊢ ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
Tactic:
norm_cast
State after:
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 / (k.factorial * (n - k).factorial)
⊢ k.factorial * (n - k).factorial ∣ n.factorial

State before:
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 / (k.factorial * (n - k).factorial)
⊢ k.factorial * (n - k).factorial ∣ n.factorial
Tactic:
exact factorial_mul_factorial_dvd_factorial h_klen
State after:
no goals

State before:
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 / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
⊢ ↑k.factorial ∣ ↑n.factorial / ↑(n - k).factorial
Tactic:
norm_cast
State after:
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 / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
⊢ k.factorial ∣ n.factorial / (n - k).factorial

State before:
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 / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
⊢ k.factorial ∣ n.factorial / (n - k).factorial
Tactic:
refine' (dvd_div_iff ((Int.coe_nat_dvd).mp h_fac_div')).mpr _
State after:
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 / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
⊢ (n - k).factorial * k.factorial ∣ n.factorial

State before:
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 / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
⊢ (n - k).factorial * k.factorial ∣ n.factorial
Tactic:
norm_cast at h_fac_div
State after:
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 / (k.factorial * (n - k).factorial)
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div : k.factorial * (n - k).factorial ∣ n.factorial
⊢ (n - k).factorial * k.factorial ∣ n.factorial

State before:
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 / (k.factorial * (n - k).factorial)
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div : k.factorial * (n - k).factorial ∣ n.factorial
⊢ (n - k).factorial * k.factorial ∣ n.factorial
Tactic:
rw [mul_comm]
State after:
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 / (k.factorial * (n - k).factorial)
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div : k.factorial * (n - k).factorial ∣ n.factorial
⊢ k.factorial * (n - k).factorial ∣ n.factorial

State before:
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 / (k.factorial * (n - k).factorial)
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div : k.factorial * (n - k).factorial ∣ n.factorial
⊢ k.factorial * (n - k).factorial ∣ n.factorial
Tactic:
exact h_fac_div
State after:
no goals

State before:
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 / (k.factorial * (n - 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
⊢ n.factorial / (k.factorial * (n - k).factorial) = n.factorial / (n - k).factorial / k.factorial
Tactic:
zify
State after:
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 / (k.factorial * (n - 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
⊢ ↑n.factorial / (↑k.factorial * ↑(n - k).factorial) = ↑n.factorial / ↑(n - k).factorial / ↑k.factorial

State before:
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 / (k.factorial * (n - 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
⊢ ↑n.factorial / (↑k.factorial * ↑(n - k).factorial) = ↑n.factorial / ↑(n - k).factorial / ↑k.factorial
Tactic:
qify
State after:
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 / (k.factorial * (n - 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
⊢ ↑(↑n.factorial / (↑k.factorial * ↑(n - k).factorial)) = ↑(↑n.factorial / ↑(n - k).factorial / ↑k.factorial)

State before:
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 / (k.factorial * (n - 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
⊢ ↑(↑n.factorial / (↑k.factorial * ↑(n - k).factorial)) = ↑(↑n.factorial / ↑(n - k).factorial / ↑k.factorial)
Tactic:
field_simp
State after:
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 / (k.factorial * (n - 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
⊢ ↑(n - k).factorial * ↑k.factorial = ↑k.factorial * ↑(n - k).factorial ∨ n.factorial = 0

State before:
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 / (k.factorial * (n - 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
⊢ ↑(n - k).factorial * ↑k.factorial = ↑k.factorial * ↑(n - k).factorial ∨ n.factorial = 0
Tactic:
rw [mul_comm]
State after:
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 / (k.factorial * (n - 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
⊢ ↑k.factorial * ↑(n - k).factorial = ↑k.factorial * ↑(n - k).factorial ∨ n.factorial = 0

State before:
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 / (k.factorial * (n - 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
⊢ ↑k.factorial * ↑(n - k).factorial = ↑k.factorial * ↑(n - k).factorial ∨ n.factorial = 0
Tactic:
left
State after:
case h
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 / (k.factorial * (n - 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
⊢ ↑k.factorial * ↑(n - k).factorial = ↑k.factorial * ↑(n - k).factorial

State before:
case h
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 / (k.factorial * (n - 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
⊢ ↑k.factorial * ↑(n - k).factorial = ↑k.factorial * ↑(n - k).factorial
Tactic:
rfl
State after:
no goals

State before:
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.factorial / (n - k).factorial
Tactic:
have h_eq_pl_with_k := exists_eq_mul_right_of_dvd h_pl_div_fac
State after:
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_eq_pl_with_k : ∃ c, n.factorial / (n - k).factorial / k.factorial = p ^ l * c
⊢ p ^ l ∣ n.factorial / (n - k).factorial

State before:
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_eq_pl_with_k : ∃ c, n.factorial / (n - k).factorial / k.factorial = p ^ l * c
⊢ p ^ l ∣ n.factorial / (n - k).factorial
Tactic:
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]
State after:
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_eq_pl_with_k : ∃ c, n.factorial / (n - k).factorial / k.factorial = p ^ l * c
h_eq_pl : ∃ r, r * p ^ l = n.factorial / (n - k).factorial
⊢ p ^ l ∣ n.factorial / (n - k).factorial

State before:
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_eq_pl_with_k : ∃ c, n.factorial / (n - k).factorial / k.factorial = p ^ l * c
h_eq_pl : ∃ r, r * p ^ l = n.factorial / (n - k).factorial
⊢ p ^ l ∣ n.factorial / (n - k).factorial
Tactic:
cases' h_eq_pl with j h_eq
State after:
case intro
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_eq_pl_with_k : ∃ c, n.factorial / (n - k).factorial / k.factorial = p ^ l * c
j : ℕ
h_eq : j * p ^ l = n.factorial / (n - k).factorial
⊢ p ^ l ∣ n.factorial / (n - k).factorial

State before:
case intro
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_eq_pl_with_k : ∃ c, n.factorial / (n - k).factorial / k.factorial = p ^ l * c
j : ℕ
h_eq : j * p ^ l = n.factorial / (n - k).factorial
⊢ p ^ l ∣ n.factorial / (n - k).factorial
Tactic:
refine' Dvd.intro j _
State after:
case intro
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_eq_pl_with_k : ∃ c, n.factorial / (n - k).factorial / k.factorial = p ^ l * c
j : ℕ
h_eq : j * p ^ l = n.factorial / (n - k).factorial
⊢ p ^ l * j = n.factorial / (n - k).factorial

State before:
case intro
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_eq_pl_with_k : ∃ c, n.factorial / (n - k).factorial / k.factorial = p ^ l * c
j : ℕ
h_eq : j * p ^ l = n.factorial / (n - k).factorial
⊢ p ^ l * j = n.factorial / (n - k).factorial
Tactic:
rw [mul_comm]
State after:
case intro
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_eq_pl_with_k : ∃ c, n.factorial / (n - k).factorial / k.factorial = p ^ l * c
j : ℕ
h_eq : j * p ^ l = n.factorial / (n - k).factorial
⊢ j * p ^ l = n.factorial / (n - k).factorial

State before:
case intro
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_eq_pl_with_k : ∃ c, n.factorial / (n - k).factorial / k.factorial = p ^ l * c
j : ℕ
h_eq : j * p ^ l = n.factorial / (n - k).factorial
⊢ j * p ^ l = n.factorial / (n - k).factorial
Tactic:
exact h_eq
State after:
no goals

State before:
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_eq_pl_with_k : ∃ c, n.factorial / (n - k).factorial / k.factorial = p ^ l * c
⊢ ∃ r, r * p ^ l = n.factorial / (n - k).factorial
Tactic:
cases' h_eq_pl_with_k with j h_eq
State after:
case intro
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
⊢ ∃ r, r * p ^ l = n.factorial / (n - k).factorial

State before:
case intro
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
⊢ ∃ r, r * p ^ l = n.factorial / (n - k).factorial
Tactic:
use (j * k.factorial)
State after:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
⊢ j * k.factorial * p ^ l = n.factorial / (n - k).factorial

State before:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
⊢ j * k.factorial * p ^ l = n.factorial / (n - k).factorial
Tactic:
have h_rew : j * k.factorial * p^l = p^l * j * k.factorial := by
  rw [mul_comm, mul_assoc]
State after:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ j * k.factorial * p ^ l = n.factorial / (n - k).factorial

State before:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ j * k.factorial * p ^ l = n.factorial / (n - k).factorial
Tactic:
rw [h_rew]
State after:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ p ^ l * j * k.factorial = n.factorial / (n - k).factorial

State before:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ p ^ l * j * k.factorial = n.factorial / (n - k).factorial
Tactic:
rw [← h_eq]
State after:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ n.factorial / (n - k).factorial / k.factorial * k.factorial = n.factorial / (n - k).factorial

State before:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ n.factorial / (n - k).factorial / k.factorial * k.factorial = n.factorial / (n - k).factorial
Tactic:
zify
State after:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ ↑n.factorial / ↑(n - k).factorial / ↑k.factorial * ↑k.factorial = ↑n.factorial / ↑(n - k).factorial

State before:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ ↑n.factorial / ↑(n - k).factorial / ↑k.factorial * ↑k.factorial = ↑n.factorial / ↑(n - k).factorial
Tactic:
qify
State after:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ ↑(↑n.factorial / ↑(n - k).factorial / ↑k.factorial) * ↑k.factorial = ↑(↑n.factorial / ↑(n - k).factorial)

State before:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ ↑(↑n.factorial / ↑(n - k).factorial / ↑k.factorial) * ↑k.factorial = ↑(↑n.factorial / ↑(n - k).factorial)
Tactic:
field_simp
State after:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ ↑n.factorial * ↑k.factorial * ↑(n - k).factorial = ↑n.factorial * (↑(n - k).factorial * ↑k.factorial)

State before:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ ↑n.factorial * ↑k.factorial * ↑(n - k).factorial = ↑n.factorial * (↑(n - k).factorial * ↑k.factorial)
Tactic:
rw [mul_comm ((n - k)! : ℚ) _]
State after:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ ↑n.factorial * ↑k.factorial * ↑(n - k).factorial = ↑n.factorial * (↑k.factorial * ↑(n - k).factorial)

State before:
case h
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
h_rew : j * k.factorial * p ^ l = p ^ l * j * k.factorial
⊢ ↑n.factorial * ↑k.factorial * ↑(n - k).factorial = ↑n.factorial * (↑k.factorial * ↑(n - k).factorial)
Tactic:
rw [mul_assoc]
State after:
no goals

State before:
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
j : ℕ
h_eq : n.factorial / (n - k).factorial / k.factorial = p ^ l * j
⊢ j * k.factorial * p ^ l = p ^ l * j * k.factorial
Tactic:
rw [mul_comm, mul_assoc]
State after:
no goals