y : ℝ
hy : 0 < y
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => x ^ y) (𝓝 ⊤) (𝓝 ⊤)
rw [ENNReal.tendsto_nhds_top_iff_nnreal]
y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
y : ℝ
hy : 0 < y
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
intro x
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
obtain ⟨c, _, hc⟩ :=
  (atTop_basis_Ioi.tendsto_iff atTop_basis_Ioi).mp (NNReal.tendsto_rpow_atTop hy) x trivial
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
have hc' : Set.Ioi ↑c ∈ 𝓝 (⊤ : ℝ≥0∞) := Ioi_mem_nhds ENNReal.coe_lt_top
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
⊢ ∀ (x_1 : ℝ≥0∞), x_1 ∈ Set.Ioi ↑c → ↑x < x_1 ^ y
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y
refine' eventually_of_mem hc' _
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
⊢ ↑x < a ^ y
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
⊢ ∀ (x_1 : ℝ≥0∞), x_1 ∈ Set.Ioi ↑c → ↑x < x_1 ^ y
intro a ha
case pos
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
ha' : a = ⊤
⊢ ↑x < a ^ y

case neg
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
ha' : ¬a = ⊤
⊢ ↑x < a ^ y
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
⊢ ↑x < a ^ y
by_cases ha' : a = ⊤
case neg.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0
ha : ↑a ∈ Set.Ioi ↑c
⊢ ↑x < ↑a ^ y
case neg
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
ha' : ¬a = ⊤
⊢ ↑x < a ^ y
lift a to ℝ≥0 using ha'
case neg.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → ↑x < ↑x_1 ^ y
⊢ ↑x < ↑a ^ y
case neg.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0
ha : ↑a ∈ Set.Ioi ↑c
⊢ ↑x < ↑a ^ y
simp only [Set.mem_Ioi, coe_lt_coe] at ha hc
case neg.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → ↑x < ↑x_1 ^ y
⊢ ↑x < ↑(a ^ y)
case neg.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → ↑x < ↑x_1 ^ y
⊢ ↑x < ↑a ^ y
rw [ENNReal.coe_rpow_of_nonneg _ hy.le]
no goals
case neg.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → ↑x < ↑x_1 ^ y
⊢ ↑x < ↑(a ^ y)
exact_mod_cast hc a ha
no goals
case pos
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ (x_1 : ℝ≥0), x_1 ∈ Set.Ioi c → ↑x_1 ^ y ∈ Set.Ioi ↑x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
ha' : a = ⊤
⊢ ↑x < a ^ y
simp [ha', hy]