y : ℝ
hy : 0 < y
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => x ^ y) atTop atTop
rw [tendsto_atTop_atTop]
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y
y : ℝ
hy : 0 < y
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y
intro b
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∀ (a : ℝ), max b 0 ^ (1 / y) ≤ a → b ≤ a ^ y
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a ^ y
use max b 0 ^ (1 / y)
y : ℝ
hy : 0 < y
b x : ℝ
hx : max b 0 ^ (1 / y) ≤ x
⊢ b ≤ x ^ y
y : ℝ
hy : 0 < y
b : ℝ
⊢ ∀ (a : ℝ), max b 0 ^ (1 / y) ≤ a → b ≤ a ^ y
intro x hx
no goals
y : ℝ
hy : 0 < y
b x : ℝ
hx : max b 0 ^ (1 / y) ≤ x
⊢ b ≤ x ^ y
exact
  le_of_max_le_left
    (by
      convert rpow_le_rpow (rpow_nonneg_of_nonneg (le_max_right b 0) (1 / y)) hx (le_of_lt hy)
        using 1
      rw [← rpow_mul (le_max_right b 0), (eq_div_iff (ne_of_gt hy)).mp rfl, Real.rpow_one])
case h.e'_3
y : ℝ
hy : 0 < y
b x : ℝ
hx : max b 0 ^ (1 / y) ≤ x
⊢ max b ?m.720 = (max b 0 ^ (1 / y)) ^ y
y : ℝ
hy : 0 < y
b x : ℝ
hx : max b 0 ^ (1 / y) ≤ x
⊢ max b ?m.720 ≤ x ^ y
convert rpow_le_rpow (rpow_nonneg_of_nonneg (le_max_right b 0) (1 / y)) hx (le_of_lt hy)
  using 1
no goals
case h.e'_3
y : ℝ
hy : 0 < y
b x : ℝ
hx : max b 0 ^ (1 / y) ≤ x
⊢ max b ?m.720 = (max b 0 ^ (1 / y)) ^ y
rw [← rpow_mul (le_max_right b 0), (eq_div_iff (ne_of_gt hy)).mp rfl, Real.rpow_one]