refine' (pow_le_pow_right (Finset.mem_filter.1 h1).2.one_lt.le _).trans (pow_one p).le
case h₂.refine'_1.intro
n : ℕ
n_big : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
p : ℕ
hp : p ∈ Finset.filter (fun x => ¬x ≤ (2 * n).sqrt) S
h1 : p ∈ S
h2 : ¬p ≤ (2 * n).sqrt
⊢ f p ≤ p
case h₂.refine'_1.intro
n : ℕ
n_big : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
p : ℕ
hp : p ∈ Finset.filter (fun x => ¬x ≤ (2 * n).sqrt) S
h1 : p ∈ S
h2 : ¬p ≤ (2 * n).sqrt
⊢ n.centralBinom.factorization p ≤ 1