y : ℝ
hy : 0 < y
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ ↑a ^ y
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => ↑x ^ y) atTop atTop
rw [Filter.tendsto_atTop_atTop]
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ ↑a ^ y
y : ℝ
hy : 0 < y
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ ↑a ^ y
intro b
case intro
y : ℝ
hy : 0 < y
b c : ℝ
hc : ∀ (a : ℝ), c ≤ a → b ≤ a ^ y
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ ↑a ^ y
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ ↑a ^ y
obtain ⟨c, hc⟩ := tendsto_atTop_atTop.mp (tendsto_rpow_atTop hy) b
case intro
y : ℝ
hy : 0 < y
b c : ℝ
hc : ∀ (a : ℝ), c ≤ a → b ≤ a ^ y
⊢ ∀ (a : ℝ≥0), toNNReal c ≤ a → b ≤ ↑a ^ y
case intro
y : ℝ
hy : 0 < y
b c : ℝ
hc : ∀ (a : ℝ), c ≤ a → b ≤ a ^ y
⊢ ∃ i, ∀ (a : ℝ≥0), i ≤ a → b ≤ ↑a ^ y
use c.toNNReal
case intro
y : ℝ
hy : 0 < y
b c : ℝ
hc : ∀ (a : ℝ), c ≤ a → b ≤ a ^ y
a : ℝ≥0
ha : toNNReal c ≤ a
⊢ b ≤ ↑a ^ y
case intro
y : ℝ
hy : 0 < y
b c : ℝ
hc : ∀ (a : ℝ), c ≤ a → b ≤ a ^ y
⊢ ∀ (a : ℝ≥0), toNNReal c ≤ a → b ≤ ↑a ^ y
intro a ha
no goals
case intro
y : ℝ
hy : 0 < y
b c : ℝ
hc : ∀ (a : ℝ), c ≤ a → b ≤ a ^ y
a : ℝ≥0
ha : toNNReal c ≤ a
⊢ b ≤ ↑a ^ y
exact_mod_cast hc a (Real.toNNReal_le_iff_le_coe.mp ha)