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 / (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
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 / (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
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 / (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
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
⊢ p ^ l ∣ n.descFactorial k
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.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
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_pl_div_fac_part : p ^ l ∣ n.factorial / (n - k).factorial
⊢ p ^ l ∣ n.descFactorial k
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_pl_div_fac_part : p ^ l ∣ n.factorial / (n - k).factorial
⊢ p ^ l ∣ n.descFactorial k
Tactic:
rw [descFactorial_eq_div h_klen]
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_pl_div_fac_part : 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_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
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
⊢ p ∣ m ^ l
Tactic:
rw [← H]
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
⊢ p ∣ n.choose k
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
⊢ p ∣ n.choose k
Tactic:
exact h_p_div_binom
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
⊢ p ^ l ∣ m ^ l
Tactic:
exact pow_dvd_pow_of_dvd (Nat.Prime.dvd_of_dvd_pow (h_p) (h_p_div_ml)) l
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
⊢ p ^ l ∣ n.choose k
Tactic:
rw [H]
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
⊢ p ^ l ∣ m ^ l
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
⊢ p ^ l ∣ m ^ l
Tactic:
exact h_pl_div_ml
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
⊢ p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
Tactic:
rw [← Nat.choose_eq_factorial_div_factorial h_klen]
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
⊢ p ^ l ∣ n.choose k
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
⊢ p ^ l ∣ n.choose k
Tactic:
exact h_pl_div_binom
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 / (k.factorial * (n - k).factorial)
⊢ ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
Tactic:
norm_cast
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 / (k.factorial * (n - k).factorial)
⊢ k.factorial * (n - k).factorial ∣ n.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 / (k.factorial * (n - k).factorial)
⊢ k.factorial * (n - k).factorial ∣ n.factorial
Tactic:
exact factorial_mul_factorial_dvd_factorial h_klen
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 / (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
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 / (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
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 / (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 _
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 / (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
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 / (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
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 / (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
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 / (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]
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 / (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
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 / (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
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 / (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
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 / (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
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 / (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
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 / (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)
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 / (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
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 / (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
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 / (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]
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 / (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
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 / (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
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 / (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
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 / (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
Proof state after:
no goals