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

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
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

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
State after:
l m n : ℕ
h_2lel : 2 ≤ l
⊢ ∀ (k' : ℕ), 4 ≤ k' → k' ≤ n - 4 → 2 * k' ≤ n → n.choose k' ≠ m ^ l

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
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

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)
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

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)
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

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
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

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)
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

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
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

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
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

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,  ⟨_, _⟩⟩
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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]
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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 ⊢
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

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
State after:
no goals

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 ⟩
State after:
no goals

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
State after:
no goals

State before:
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
Tactic:
have h_3lel : 3 ≤ l := by
  sorry
State after:
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
h_3lel : 3 ≤ l
⊢ False

State before:
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
h_3lel : 3 ≤ l
⊢ False
Tactic:
have h₄ : n < k^3 := by
  sorry
State after:
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
h_3lel : 3 ≤ l
h₄ : n < k ^ 3
⊢ False

State before:
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
h_3lel : 3 ≤ l
h₄ : n < k ^ 3
⊢ False
Tactic:
sorry
State after:
no goals

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
h✝ : ¬l = 2
⊢ 3 ≤ l
Tactic:
sorry
State after:
no goals

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
h✝ : ¬l = 2
h_3lel : 3 ≤ l
⊢ n < k ^ 3
Tactic:
sorry
State after:
no goals

State before:
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
Tactic:
exact h_wlog k h_4lek h_klen4 h_2k
State after:
no goals

State before:
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
Tactic:
simp only [not_le] at h
State after:
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

State before:
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
Tactic:
have h_klen : k ≤ n := le_trans h_klen4 (Nat.sub_le n 4)
State after:
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
h_klen : k ≤ n
⊢ n.choose k ≠ m ^ l

State before:
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
h_klen : k ≤ n
⊢ n.choose k ≠ m ^ l
Tactic:
rw [← choose_symm h_klen]
State after:
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
h_klen : k ≤ n
⊢ n.choose (n - k) ≠ m ^ l

State before:
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
h_klen : k ≤ n
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
let k' := n - k
State after:
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
h_klen : k ≤ n
k' : ℕ := n - k
⊢ n.choose (n - k) ≠ m ^ l

State before:
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
h_klen : k ≤ n
k' : ℕ := n - k
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
have h_k'_def : k' = n - k := by rfl
State after:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
⊢ n.choose (n - k) ≠ m ^ l

State before:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
have h_2k'len : 2 * k' ≤ n := by
  sorry
State after:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ n.choose (n - k) ≠ m ^ l

State before:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
have h_k'len4 : k' ≤ n - 4 := by
  simp [h_k'_def]
  have help : k + k ≤ n - 4 + k := add_le_add_right h_klen4 k
  rw [← (two_mul k)] at help
  exact le_trans (le_of_lt h) help
State after:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
⊢ n.choose (n - k) ≠ m ^ l

State before:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
have h_4lek' : 4 ≤ k' := by
  have h_4len : 4 ≤ n := le_trans (le_trans h_4lek h_klen4) (Nat.sub_le n 4)
  exact Iff.mp (le_tsub_iff_le_tsub h_klen h_4len) h_klen4
State after:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
h_4lek' : 4 ≤ k'
⊢ n.choose (n - k) ≠ m ^ l

State before:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
h_4lek' : 4 ≤ k'
⊢ n.choose (n - k) ≠ m ^ l
Tactic:
exact h_wlog k' h_4lek' h_k'len4 h_2k'len
State after:
no goals

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
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
⊢ k' = n - k
Tactic:
rfl
State after:
no goals

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
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
⊢ 2 * k' ≤ n
Tactic:
sorry
State after:
no goals

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
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ k' ≤ n - 4
Tactic:
simp [h_k'_def]
State after:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ n ≤ n - 4 + k

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
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
⊢ n ≤ n - 4 + k
Tactic:
have help : k + k ≤ n - 4 + k := add_le_add_right h_klen4 k
State after:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
help : k + k ≤ n - 4 + k
⊢ n ≤ n - 4 + k

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
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
help : k + k ≤ n - 4 + k
⊢ n ≤ n - 4 + k
Tactic:
rw [← (two_mul k)] at help
State after:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
help : 2 * k ≤ n - 4 + k
⊢ n ≤ n - 4 + k

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
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
help : 2 * k ≤ n - 4 + k
⊢ n ≤ n - 4 + k
Tactic:
exact le_trans (le_of_lt h) help
State after:
no goals

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
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
⊢ 4 ≤ k'
Tactic:
have h_4len : 4 ≤ n := le_trans (le_trans h_4lek h_klen4) (Nat.sub_le n 4)
State after:
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
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
h_4len : 4 ≤ n
⊢ 4 ≤ k'

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
h : n < 2 * k
h_klen : k ≤ n
k' : ℕ := n - k
h_k'_def : k' = n - k
h_2k'len : 2 * k' ≤ n
h_k'len4 : k' ≤ n - 4
h_4len : 4 ≤ n
⊢ 4 ≤ k'
Tactic:
exact Iff.mp (le_tsub_iff_le_tsub h_klen h_4len) h_klen4
State after:
no goals