awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this :
  Eq (α := (p : ℝ≥0 × ℝ) → ℝ≥0) (fun (p : ℝ≥0 × ℝ) ↦ p.1 ^ p.2)
    (toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2))
refine_1 : ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ((↑(x, y).1 : ℝ), (x, y).2)
refine_2 : ContinuousAt (Y := ℝ × ℝ) (fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) (x, y)
⊢ ContinuousAt (toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) (x, y)

Tactic:
refine continuous_real_toNNReal.continuousAt.comp (ContinuousAt.comp ?_ ?_)

Premises used: Continuous.continuousAt, continuous_real_toNNReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this :
  Eq (α := (p : ℝ≥0 × ℝ) → ℝ≥0) (fun (p : ℝ≥0 × ℝ) ↦ p.1 ^ p.2)
    (toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2))
refine_1 : ((↑(x, y).1 : ℝ), (x, y).2).1 ≠ 0 ∨ 0 < ((↑(x, y).1 : ℝ), (x, y).2).2
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ((↑(x, y).1 : ℝ), (x, y).2)

Tactic:
apply Real.continuousAt_rpow

Premises used: Real.continuousAt_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this :
  Eq (α := (p : ℝ≥0 × ℝ) → ℝ≥0) (fun (p : ℝ≥0 × ℝ) ↦ p.1 ^ p.2)
    (toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2))
⊢ ((↑(x, y).1 : ℝ), (x, y).2).1 ≠ 0 ∨ 0 < ((↑(x, y).1 : ℝ), (x, y).2).2

Tactic:
simpa using h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this :
  Eq (α := (p : ℝ≥0 × ℝ) → ℝ≥0) (fun (p : ℝ≥0 × ℝ) ↦ p.1 ^ p.2)
    (toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2))
⊢ ContinuousAt (Y := ℝ × ℝ) (fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) (x, y)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ≥0
hy : 1 < y
obtain : ∀ (m : ℕ) (hm : x < (y - 1 + 1) ^ m), ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y

Tactic:
obtain ⟨m, hm⟩ := add_one_pow_unbounded_of_pos x (tsub_pos_of_lt hy)

Premises used: add_one_pow_unbounded_of_pos, tsub_pos_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < (y - 1 + 1) ^ m
⊢ x < y ^ m

Tactic:
rw [tsub_add_cancel_of_le hy.le] at hm

Premises used: tsub_add_cancel_of_le, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y

Tactic:
eventually_atTop.2 ⟨m + 1, fun n hn => ?_⟩

Premises used: Iff.mpr, HAdd.hAdd, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
refine : ∀ (n : ℕ) (hn : n ≥ m + 1), x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y

Tactic:
refine eventually_atTop.2 ⟨m + 1, fun n hn => ?_⟩

Premises used: Iff.mpr, HAdd.hAdd, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : n ≥ m + 1
simp : HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ≤ y
⊢ x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y

Tactic:
simp only [one_div]

Premises used: one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : n ≥ m + 1
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ≤ y

Tactic:
simpa only [NNReal.rpow_inv_le_iff (Nat.cast_pos.2 <| m.succ_pos.trans_le hn),
    NNReal.rpow_natCast] using hm.le.trans (pow_right_mono₀ hy.le (m.le_succ.trans hn))

Premises used: Iff.mpr, Nat.cast_pos, NNReal.rpow_natCast, LT.lt.le, Nat.le_succ, NNReal.rpow_inv_le_iff, pow_right_mono₀, LT.lt.trans_le, Nat.succ_pos, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0
v : α → ℝ
x : ℝ≥0
y : ℝ
hx : Tendsto u f (𝓝 x)
hy : Tendsto v f (𝓝 y)
h : x ≠ 0 ∨ 0 < y
⊢ Tendsto (fun (a : α) ↦ u a ^ v a) f (𝓝 (x ^ y))

Tactic:
Tendsto.comp (NNReal.continuousAt_rpow h) (hx.prodMk_nhds hy)

Premises used: NNReal.continuousAt_rpow, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0
y : ℝ
h_1 : x ≠ 0 ∨ 0 ≤ y
h_2 : 0 ≤ y
h : 0 = y
⊢ ContinuousAt (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ HPow.hPow (β := ℝ) z 0) x

Tactic:
simp only [rpow_zero, continuousAt_const]

Premises used: continuousAt_const, NNReal.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
h : 0 ≤ y
⊢ Continuous (Y := ℝ≥0) fun (x : ℝ≥0) ↦ x ^ y

Tactic:
continuous_iff_continuousAt.2 fun _ => continuousAt_rpow_const (Or.inr h)

Premises used: Iff.mpr, NNReal.continuousAt_rpow_const, Or.inr, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
r : ℝ
⊢ ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ r) {0}ᶜ

Tactic:
fun _ h => ContinuousAt.continuousWithinAt <| NNReal.continuousAt_rpow_const (.inl h)

Premises used: ContinuousAt.continuousWithinAt, NNReal.continuousAt_rpow_const, ContinuousOn, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
r : ℝ
s : Set ℝ≥0
h : 0 ∉ s ∨ 0 ≤ r
h_1 : 0 ∉ s
⊢ ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ r) {0}ᶜ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
r : ℝ
s : Set ℝ≥0
h : 0 ∉ s ∨ 0 ≤ r
h_1 : 0 ∉ s
⊢ s ⊆ {0}ᶜ

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
hx : x ≠ ∞
y : ℝ≥0∞
hy : 1 < y
⊢ x ≠ ∞

Tactic:
hx
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
hx : x ≠ ∞
y : ℝ≥0∞
hy : 1 < y
lift : ∀ (x : ℝ≥0), ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y

Tactic:
lift x to ℝ≥0 using hx
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
pos : ∀ (h : y = ∞), ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
neg : ∀ (h : ¬y = ∞), ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y

Tactic:
by_cases h : y = ∞
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : y = ∞
⊢ ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y

Tactic:
Eventually.of_forall fun n => h.symm ▸ le_top

Premises used: Eq.rec, Filter.Eventually.of_forall, le_top, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : y = ∞
⊢ ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y

Tactic:
exact Eventually.of_forall fun n => h.symm ▸ le_top

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : ¬y = ∞
⊢ y ≠ ∞

Tactic:
h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : ¬y = ∞
neg : ∀ (y : ℝ≥0) (hy : 1 < (↑y : ℝ≥0∞)), ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑y : ℝ≥0∞)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y

Tactic:
lift y to ℝ≥0 using h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y

Tactic:
have := NNReal.eventually_pow_one_div_le x (mod_cast hy : 1 < y)
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
this : ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑y : ℝ≥0∞)

Tactic:
this.congr (Eventually.of_forall fun n => ?_)

Premises used: Filter.Eventually.of_forall, Filter.Eventually.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
this : ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
neg : ∀ (n : ℕ), x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y ↔ (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑y : ℝ≥0∞)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑y : ℝ≥0∞)

Tactic:
refine this.congr (Eventually.of_forall fun n => ?_)

Premises used: Filter.Eventually.of_forall, Filter.Eventually.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
this : ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
n : ℕ
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
this : ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
n : ℕ
neg : x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y ↔ (↑(x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ≤ (↑y : ℝ≥0∞)
neg₁ neg₂ : x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y ↔ x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
⊢ x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y ↔ (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑y : ℝ≥0∞)

Tactic:
rw [← coe_rpow_of_nonneg x (by positivity : 0 ≤ (1 / n : ℝ)), coe_le_coe]

Premises used: ENNReal.coe_rpow_of_nonneg, ENNReal.coe_le_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
pos : ∀ (hx : x = ∞), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
neg : ∀ (hx : ¬x = ∞), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x

Tactic:
by_cases hx : x = ⊤
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ∞
pos : Tendsto (fun (a : ℝ≥0∞) ↦ a ^ y) (𝓝 ∞) (𝓝 (HPow.hPow (α := ℝ≥0∞) ∞ y))
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x

Tactic:
rw [hx, ContinuousAt]

Premises used: ContinuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ x ^ y) (𝓝 ∞) (𝓝 ∞)

Tactic:
ENNReal.tendsto_rpow_at_top h

Premises used: ENNReal.tendsto_rpow_at_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ∞
h₁ : HPow.hPow (α := ℝ≥0∞) ∞ y = ∞
⊢ Tendsto (fun (a : ℝ≥0∞) ↦ a ^ y) (𝓝 ∞) (𝓝 (HPow.hPow (α := ℝ≥0∞) ∞ y))

Tactic:
convert! ENNReal.tendsto_rpow_at_top h

Premises used: ENNReal.tendsto_rpow_at_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ∞
⊢ HPow.hPow (α := ℝ≥0∞) ∞ y = ∞

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : ¬x = ∞
⊢ x ≠ ∞

Tactic:
hx
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : ¬x = ∞
neg : ∀ (x : ℝ≥0), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) (↑x : ℝ≥0∞)
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x

Tactic:
lift x to ℝ≥0 using hx
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
h : 0 < y
x : ℝ≥0
neg : ContinuousAt (Y := ℝ≥0∞) ((fun (a : ℝ≥0∞) ↦ a ^ y) ∘ ofNNReal) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) (↑x : ℝ≥0∞)

Tactic:
rw [continuousAt_coe_iff]

Premises used: ENNReal.continuousAt_coe_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt (ofNNReal ∘ fun (z : ℝ≥0) ↦ z ^ y) x

Tactic:
continuous_coe.continuousAt.comp (NNReal.continuousAt_rpow_const (Or.inr h.le))

Premises used: LT.lt.le, Continuous.continuousAt, NNReal.continuousAt_rpow_const, ContinuousAt.comp, ENNReal.continuous_coe, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
h : 0 < y
x : ℝ≥0
h₁ : (fun (a : ℝ≥0∞) ↦ a ^ y) ∘ ofNNReal = ofNNReal ∘ fun (z : ℝ≥0) ↦ z ^ y
⊢ ContinuousAt (Y := ℝ≥0∞) ((fun (a : ℝ≥0∞) ↦ a ^ y) ∘ ofNNReal) x

Tactic:
convert! continuous_coe.continuousAt.comp (NNReal.continuousAt_rpow_const (Or.inr h.le)) using 1

Premises used: LT.lt.le, Continuous.continuousAt, NNReal.continuousAt_rpow_const, ContinuousAt.comp, ENNReal.continuous_coe, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
h : 0 < y
x : ℝ≥0
h₁ : ∀ (x : ℝ≥0), ((fun (a : ℝ≥0∞) ↦ a ^ y) ∘ ofNNReal) x = (ofNNReal ∘ fun (z : ℝ≥0) ↦ z ^ y) x
⊢ (fun (a : ℝ≥0∞) ↦ a ^ y) ∘ ofNNReal = ofNNReal ∘ fun (z : ℝ≥0) ↦ z ^ y

Tactic:
ext1 x
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
h : 0 < y
x_1 x : ℝ≥0
⊢ ((fun (a : ℝ≥0∞) ↦ a ^ y) ∘ ofNNReal) x = (ofNNReal ∘ fun (z : ℝ≥0) ↦ z ^ y) x

Tactic:
simp [← coe_rpow_of_nonneg _ h.le]

Premises used: ENNReal.coe_rpow_of_nonneg, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
⊢ Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ y

Tactic:
continuous_iff_continuousAt.2 fun x => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
refine : ∀ (x : ℝ≥0∞), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
⊢ Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ y

Tactic:
refine continuous_iff_continuousAt.2 fun x => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
x : ℝ≥0∞
inl : ∀ (hy : 0 < y), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
inr : ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ HPow.hPow (β := ℝ) a 0) x
inr₁ : ∀ (hy : y < 0), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x

Tactic:
rcases lt_trichotomy (0 : ℝ) y with (hy | rfl | hy)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
x : ℝ≥0∞
hy : 0 < y
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x

Tactic:
continuousAt_rpow_const_of_pos hy

Premises used: _private.0.ENNReal.continuousAt_rpow_const_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
x : ℝ≥0∞
hy : 0 < y
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x

Tactic:
exact continuousAt_rpow_const_of_pos hy

Premises used: _private.0.ENNReal.continuousAt_rpow_const_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
inr : ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ 1) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ HPow.hPow (β := ℝ) a 0) x

Tactic:
simp only [rpow_zero]

Premises used: ENNReal.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ 1) x

Tactic:
continuousAt_const

Premises used: continuousAt_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ 1) x

Tactic:
exact continuousAt_const

Premises used: continuousAt_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
x : ℝ≥0∞
hy : y < 0
⊢ ∃ (z : ℝ), y = -z

Tactic:
⟨-y, (neg_neg _).symm⟩

Premises used: neg_neg, Exists.intro, Eq.symm, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
x : ℝ≥0∞
hy : y < 0
inr : ∀ (z : ℝ) (hz : y = -z), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x

Tactic:
obtain ⟨z, hz⟩ : ∃ z, y = -z := ⟨-y, (neg_neg _).symm⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ 0 < z

Tactic:
simpa [hz] using hy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ 0 < z

Tactic:
have z_pos : 0 < z := by simpa [hz] using hy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
inr : ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ (a ^ z)⁻¹) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x

Tactic:
simp_rw [hz, rpow_neg]

Premises used: ENNReal.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ (a ^ z)⁻¹) x

Tactic:
continuous_inv.continuousAt.comp (continuousAt_rpow_const_of_pos z_pos)

Premises used: _private.0.ENNReal.continuousAt_rpow_const_of_pos, setOf, Continuous.continuousAt, ContinuousAt.comp, ContinuousInv.continuous_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ (a ^ z)⁻¹) x

Tactic:
exact continuous_inv.continuousAt.comp (continuousAt_rpow_const_of_pos z_pos)

Premises used: _private.0.ENNReal.continuousAt_rpow_const_of_pos, Continuous.continuousAt, ContinuousAt.comp, ContinuousInv.continuous_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
c : ℝ≥0∞
hc : c ≠ ∞
y : ℝ
hy : 0 < y
⊢ Tendsto (fun (b : ℝ≥0∞) ↦ c * b ^ y) (𝓝 0) (𝓝 (c * HPow.hPow (α := ℝ≥0∞) 0 y))

Tactic:
ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _

Premises used: ENNReal.Tendsto.const_mul, Continuous.tendsto, ENNReal.continuous_rpow_const, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
c : ℝ≥0∞
hc : c ≠ ∞
y : ℝ
hy : 0 < y
h : 0 = c * HPow.hPow (α := ℝ≥0∞) 0 y
convert_3 : HPow.hPow (α := ℝ≥0∞) 0 y ≠ 0 ∨ c ≠ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ c * x ^ y) (𝓝 0) (𝓝 0)

Tactic:
convert! ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _

Premises used: ENNReal.Tendsto.const_mul, Continuous.tendsto, ENNReal.continuous_rpow_const, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
c : ℝ≥0∞
hc : c ≠ ∞
y : ℝ
hy : 0 < y
⊢ 0 = c * HPow.hPow (α := ℝ≥0∞) 0 y

Tactic:
simp [hy]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
c : ℝ≥0∞
hc : c ≠ ∞
y : ℝ
hy : 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) 0 y ≠ 0 ∨ c ≠ ∞

Tactic:
Or.inr hc

Premises used: Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
c : ℝ≥0∞
hc : c ≠ ∞
y : ℝ
hy : 0 < y
⊢ HPow.hPow (α := ℝ≥0∞) 0 y ≠ 0 ∨ c ≠ ∞

Tactic:
exact Or.inr hc

Premises used: Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a : ℝ≥0∞
r : ℝ
hm : Tendsto m f (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ m x ^ r) f (𝓝 (a ^ r))

Tactic:
(ENNReal.continuous_rpow_const.tendsto a).comp hm

Premises used: Continuous.tendsto, Filter.Tendsto.comp, ENNReal.continuous_rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
⊢ p.1 ≠ 0

Tactic:
have A : p.1 ≠ 0 := slitPlane_ne_zero hp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
A : p.1 ≠ 0
⊢ (𝓝 p).EventuallyEq (β := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) fun (x : ℂ × ℂ) ↦ cexp (log x.1 * x.2)

Tactic:
have : (fun x : ℂ × ℂ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
    ((isOpen_ne.preimage continuous_fst).eventually_mem A).mono fun p hp =>
      cpow_def_of_ne_zero hp _
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
A : p.1 ≠ 0
this : (𝓝 p).EventuallyEq (β := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) fun (x : ℂ × ℂ) ↦ cexp (log x.1 * x.2)
rw :
  HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2)
    (p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 / p.1) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    p
⊢ HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2)
    (HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    p

Tactic:
rw [cpow_sub _ _ A, cpow_one, mul_div_left_comm, mul_smul, mul_smul]

Premises used: Complex.cpow_sub, Complex.cpow_one, mul_div_left_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
A : p.1 ≠ 0
this : (𝓝 p).EventuallyEq (β := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) fun (x : ℂ × ℂ) ↦ cexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2)
    (p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 / p.1) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    p

Tactic:
HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm

Premises used: HasStrictFDerivAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
A : p.1 ≠ 0
this : (𝓝 p).EventuallyEq (β := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) fun (x : ℂ × ℂ) ↦ cexp (log x.1 * x.2)
refine :
  HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ cexp (log x.1 * x.2))
    (p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 / p.1) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    p
⊢ HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2)
    (p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 / p.1) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    p

Tactic:
refine HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm

Premises used: HasStrictFDerivAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
A : p.1 ≠ 0
this : (𝓝 p).EventuallyEq (β := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) fun (x : ℂ × ℂ) ↦ cexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ cexp (log x.1 * x.2))
    (p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 / p.1) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    p

Tactic:
simpa only [cpow_def_of_ne_zero A, div_eq_mul_inv, mul_smul, add_comm, smul_add] using
    ((hasStrictFDerivAt_fst.clog hp).mul hasStrictFDerivAt_snd).cexp

Premises used: hasStrictFDerivAt_snd, HasStrictFDerivAt.cexp, HasStrictFDerivAt.clog, div_eq_mul_inv, add_comm, HasStrictFDerivAt.mul, Complex.cpow_def_of_ne_zero, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x y : ℂ
hp : x ∈ slitPlane
⊢ HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2)
    (HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (y * x ^ (y - 1)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (x ^ y * log x) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    (x, y)

Tactic:
@hasStrictFDerivAt_cpow (x, y) hp

Premises used: Complex.hasStrictFDerivAt_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
inl :
  ∀ (h : Ne (α := ℂ) 0 0 ∨ y ≠ 0),
    HasStrictDerivAt (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y) (HPow.hPow (α := ℂ) 0 y * log 0) y
inr : ∀ (hx : ¬x = 0), HasStrictDerivAt (fun (y : ℂ) ↦ x ^ y) (x ^ y * log x) y
⊢ HasStrictDerivAt (fun (y : ℂ) ↦ x ^ y) (x ^ y * log x) y

Tactic:
rcases em (x = 0) with (rfl | hx)

Premises used: em, OfNat.ofNat, Eq, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
y : ℂ
h : Ne (α := ℂ) 0 0 ∨ y ≠ 0
⊢ y ≠ 0

Tactic:
replace h := h.neg_resolve_left rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
y : ℂ
h : y ≠ 0
inl : HasStrictDerivAt (F := ℂ) (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y) 0 y
⊢ HasStrictDerivAt (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y) (HPow.hPow (α := ℂ) 0 y * log 0) y

Tactic:
rw [log_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Complex.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (F := ℂ) (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y) 0 y

Tactic:
(hasStrictDerivAt_const y 0).congr_of_eventuallyEq ?_

Premises used: hasStrictDerivAt_const, OfNat.ofNat, HasStrictDerivAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
y : ℂ
h : y ≠ 0
inl : (𝓝 y).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ 0) fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y
⊢ HasStrictDerivAt (F := ℂ) (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y) 0 y

Tactic:
refine (hasStrictDerivAt_const y 0).congr_of_eventuallyEq ?_

Premises used: hasStrictDerivAt_const, OfNat.ofNat, HasStrictDerivAt.congr_of_eventuallyEq