internlm/Lean-Github huggingface dataset:
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:
field_simp
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 * ↑k.factorial * ↑(n - k).factorial = ↑n.factorial * (↑(n - k).factorial * ↑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 * ↑k.factorial * ↑(n - k).factorial = ↑n.factorial * (↑(n - k).factorial * ↑k.factorial)
Tactic:
rw [mul_comm ((n - k)! : ℚ) _]
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 * ↑k.factorial * ↑(n - k).factorial = ↑n.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 / (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]
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
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]
Proof state after:
no goals
Theorem: chapter03.factor_in_descFactorial
Proof state before:
n k p l : ℕ
h_klen : k ≤ n
h_klp : k < p
hp : p.Prime
h_pow_div : p ^ l ∣ n.descFactorial k
h_1lel : 1 ≤ l
⊢ ∃ i ≤ k - 1, p ^ l ∣ n - i
Tactic:
sorry
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
⊢ n.choose k ≠ m ^ l
Tactic:
cases' em (n ≥ 2*k) with h_2k h
Proof state after:
case inl
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h_2k : n ≥ 2 * k
⊢ n.choose k ≠ m ^ l

case inr
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h_wlog : ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
h : ¬n ≥ 2 * k
⊢ n.choose k ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
k l m n : ℕ
h_2lel : 2 ≤ l
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
⊢ ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
Tactic:
clear h_4lek h_klen4 k
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
⊢ ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
⊢ ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l
Tactic:
intros k h_4lek h_klen4 h
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
⊢ n.choose k ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
⊢ n.choose k ≠ m ^ l
Tactic:
have h_klen : k ≤ n := le_trans h_klen4 (Nat.sub_le n 4)
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
⊢ n.choose k ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
⊢ n.choose k ≠ m ^ l
Tactic:
have h_1lel : 1 ≤ l := le_of_succ_le (h_2lel)
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
⊢ n.choose k ≠ m ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
⊢ n.choose k ≠ m ^ l
Tactic:
by_contra H
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
⊢ False
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
h₁ : ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
⊢ False
Tactic:
cases em (l = 2)
Proof state after:
case inl
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
h₁ : ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
h✝ : l = 2
⊢ False

case inr
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
h₁ : ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
h✝ : ¬l = 2
⊢ False
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
⊢ ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
Tactic:
obtain ⟨p, ⟨h_klp, ⟨h_p, h_p_div_binom⟩⟩⟩ := sylvester k n h
Proof state after:
case intro.intro.intro
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
⊢ ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case intro.intro.intro
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
⊢ ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
Tactic:
use p
Proof state after:
case h
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
⊢ p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case h
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
⊢ p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
Tactic:
refine' ⟨h_p,  ⟨_, _⟩⟩
Proof state after:
case h.refine'_1
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
⊢ p ^ l ≤ n

case h.refine'_2
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
⊢ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case h.refine'_1
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
⊢ p ^ l ≤ n
Tactic:
have h_pl_div_desc: p^l ∣ n.descFactorial k :=
    prime_div_descFactorial n k m l p  h_klen h_p h_p_div_binom H
Proof state after:
case h.refine'_1
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
⊢ p ^ l ≤ n
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case h.refine'_1
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
⊢ p ^ l ≤ n
Tactic:
have h_klp_pow_dvd := factor_in_descFactorial n k p l h_klen (gt_iff_lt.mp h_klp) (h_p)
    h_pl_div_desc h_1lel
Proof state after:
case h.refine'_1
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
h_klp_pow_dvd : ∃ i ≤ k - 1, p ^ l ∣ n - i
⊢ p ^ l ≤ n
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case h.refine'_1
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
h_klp_pow_dvd : ∃ i ≤ k - 1, p ^ l ∣ n - i
⊢ p ^ l ≤ n
Tactic:
cases' h_klp_pow_dvd with i hi
Proof state after:
case h.refine'_1.intro
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi : i ≤ k - 1 ∧ p ^ l ∣ n - i
⊢ p ^ l ≤ n
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case h.refine'_1.intro
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi : i ≤ k - 1 ∧ p ^ l ∣ n - i
⊢ p ^ l ≤ n
Tactic:
cases' hi with hi_left hi_right
Proof state after:
case h.refine'_1.intro.intro
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
⊢ p ^ l ≤ n
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case h.refine'_1.intro.intro
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
⊢ p ^ l ≤ n
Tactic:
have : p^l ≤ n - i := by
  refine' Nat.le_of_dvd _ hi_right
  simp only [tsub_pos_iff_lt]
  have h_ilk : i < k := by
    have hk : 0 < k := lt_of_lt_of_le four_pos h_4lek
    zify at hi_left
    zify
    norm_cast at hi_left ⊢
    exact Iff.mpr (lt_iff_le_pred hk) hi_left
  exact lt_of_lt_of_le h_ilk h_klen
Proof state after:
case h.refine'_1.intro.intro
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
this : p ^ l ≤ n - i
⊢ p ^ l ≤ n
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case h.refine'_1.intro.intro
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
this : p ^ l ≤ n - i
⊢ p ^ l ≤ n
Tactic:
have h_klen4i : n - i ≤ n := Nat.sub_le n i
Proof state after:
case h.refine'_1.intro.intro
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
this : p ^ l ≤ n - i
h_klen4i : n - i ≤ n
⊢ p ^ l ≤ n
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case h.refine'_1.intro.intro
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
this : p ^ l ≤ n - i
h_klen4i : n - i ≤ n
⊢ p ^ l ≤ n
Tactic:
exact le_trans this h_klen4i
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
⊢ p ^ l ≤ n - i
Tactic:
refine' Nat.le_of_dvd _ hi_right
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
⊢ 0 < n - i
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
⊢ 0 < n - i
Tactic:
simp only [tsub_pos_iff_lt]
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
⊢ i < n
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
⊢ i < n
Tactic:
have h_ilk : i < k := by
  have hk : 0 < k := lt_of_lt_of_le four_pos h_4lek
  zify at hi_left
  zify
  norm_cast at hi_left ⊢
  exact Iff.mpr (lt_iff_le_pred hk) hi_left
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
h_ilk : i < k
⊢ i < n
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
h_ilk : i < k
⊢ i < n
Tactic:
exact lt_of_lt_of_le h_ilk h_klen
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
⊢ i < k
Tactic:
have hk : 0 < k := lt_of_lt_of_le four_pos h_4lek
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
hk : 0 < k
⊢ i < k
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_left : i ≤ k - 1
hi_right : p ^ l ∣ n - i
hk : 0 < k
⊢ i < k
Tactic:
zify at hi_left
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_right : p ^ l ∣ n - i
hk : 0 < k
hi_left : ↑i ≤ ↑(k - 1)
⊢ i < k
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_right : p ^ l ∣ n - i
hk : 0 < k
hi_left : ↑i ≤ ↑(k - 1)
⊢ i < k
Tactic:
zify
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_right : p ^ l ∣ n - i
hk : 0 < k
hi_left : ↑i ≤ ↑(k - 1)
⊢ ↑i < ↑k
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_right : p ^ l ∣ n - i
hk : 0 < k
hi_left : ↑i ≤ ↑(k - 1)
⊢ ↑i < ↑k
Tactic:
norm_cast at hi_left ⊢
Proof state after:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_right : p ^ l ∣ n - i
hk : 0 < k
hi_left : i ≤ k - 1
⊢ i < k
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
h_pl_div_desc : p ^ l ∣ n.descFactorial k
i : ℕ
hi_right : p ^ l ∣ n - i
hk : 0 < k
hi_left : i ≤ k - 1
⊢ i < k
Tactic:
exact Iff.mpr (lt_iff_le_pred hk) hi_left
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case h.refine'_2
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
p : ℕ
h_klp : p > k
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
⊢ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
Tactic:
exact ⟨
    Nat.pow_lt_pow_left (h_klp) (Nat.ne_of_gt <| gt_of_ge_of_gt h_2lel two_pos),
    Nat.pow_le_pow_of_le_right (pos_of_gt h_4lek) h_2lel ⟩
Proof state after:
no goals
Theorem: chapter03.binomials_coefficients_never_powers
Proof state before:
case inl
l m n : ℕ
h_2lel : 2 ≤ l
k : ℕ
h_4lek : 4 ≤ k
h_klen4 : k ≤ n - 4
h : 2 * k ≤ n
h_klen : k ≤ n
h_1lel : 1 ≤ l
H : n.choose k = m ^ l
h₁ : ∃ p, p.Prime ∧ p ^ l ≤ n ∧ k ^ l < p ^ l ∧ k ^ 2 ≤ k ^ l
h✝ : l = 2
⊢ False
Tactic:
sorry
Proof state after:
no goals