sorry
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
no goals