rw [← Real.rpow_le_rpow_iff (by norm_num) h0 (by norm_num : (0:ℝ) < 6)]
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ (2 * n) ^ 6⁻¹
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ ((2 * n) ^ 6⁻¹) ^ 6