-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem ENNReal.tendsto_rpow_at_top {y : ℝ} (hy : 0 < y) :
    Tendsto (fun x : ℝ≥0∞ => x ^ y) (𝓝 ⊤) (𝓝 ⊤)

Proof state:
case h
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ 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

Tactic:
by_cases ha' : a = ⊤

Result:
case pos
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ 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 ∈ 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

Proof state:
case pos
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ 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

Tactic:
simp [ha', hy]

Result:
no goals

Proof state:
case neg
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ 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

Tactic:
lift a to ℝ≥0 using ha'

Result:
case neg.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ 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

Proof state:
y : ℝ
hy : 0 < y
⊢ Tendsto (fun x => x ^ y) (𝓝 ⊤) (𝓝 ⊤)

Tactic:
rw [ENNReal.tendsto_nhds_top_iff_nnreal]

Result:
y : ℝ
hy : 0 < y
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y

Proof state:
y : ℝ
hy : 0 < y
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y

Tactic:
intro x

Result:
y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y

Proof state:
case neg.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ 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

Tactic:
simp only [Set.mem_Ioi, coe_lt_coe] at ha hc

Result:
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

Proof state:
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y

Tactic:
have hc' : Set.Ioi ↑c ∈ 𝓝 (⊤ : ℝ≥0∞) := Ioi_mem_nhds ENNReal.coe_lt_top

Result:
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y

Proof state:
y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y

Tactic:
obtain ⟨c, _, hc⟩ :=
  (atTop_basis_Ioi.tendsto_iff atTop_basis_Ioi).mp (NNReal.tendsto_rpow_atTop hy) x trivial

Result:
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y

Proof state:
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)

Tactic:
exact mod_cast hc a ha

Result:
no goals

Proof state:
case intro.intro
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Set.Ioi ↑c ∈ 𝓝 ⊤
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ⊤, ↑x < a ^ y

Tactic:
filter_upwards [hc'] with a ha

Result:
case h
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ 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

Proof state:
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

Tactic:
rw [← ENNReal.coe_rpow_of_nonneg _ hy.le]

Result:
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)