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