internlm/Lean-Github huggingface dataset:
Theorem: chapter03.prime_div_descFactorial
Proof 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
Proof 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
Theorem: chapter03.prime_div_descFactorial
Proof 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]
Proof 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
Theorem: chapter03.prime_div_descFactorial
Proof 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
Proof 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
Theorem: chapter03.prime_div_descFactorial
Proof 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 _
Proof 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
Theorem: chapter03.prime_div_descFactorial
Proof 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]
Proof 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
Theorem: chapter03.prime_div_descFactorial
Proof 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
Proof state after:
no goals
Theorem: chapter03.prime_div_descFactorial
Proof 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
Proof 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
Theorem: chapter03.prime_div_descFactorial
Proof 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)
Proof 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
Theorem: chapter03.prime_div_descFactorial
Proof 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]
Proof 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
Theorem: chapter03.prime_div_descFactorial
Proof 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]
Proof 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
Theorem: chapter03.prime_div_descFactorial
Proof 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]
Proof 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
Theorem: chapter03.prime_div_descFactorial
Proof 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
Proof 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
Theorem: chapter03.prime_div_descFactorial
Proof 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
Proof 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)