awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f g : α → ℂ
hf : Continuous[inst, _] f
hg : Continuous[inst, _] g
h0 : ∀ (a : α), f a ∈ slitPlane
⊢ Continuous[inst, _] fun (x : α) ↦ f x ^ g x

Tactic:
continuous_iff_continuousAt.2 fun a => hf.continuousAt.cpow hg.continuousAt (h0 a)

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.cpow, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
b : ℂ
hf : Continuous[inst, _] f
h : b ≠ 0 ∨ ∀ (a : α), f a ≠ 0
⊢ Continuous[inst, _] fun (x : α) ↦ b ^ f x

Tactic:
continuous_iff_continuousAt.2 fun a => hf.continuousAt.const_cpow <| h.imp id fun h => h a

Premises used: Iff.mpr, id, Continuous.continuousAt, Or.imp, ContinuousAt.const_cpow, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
s : Set α
b : ℂ
hf : ContinuousOn f s
h : ∀ a ∈ s, f a ∈ slitPlane
⊢ ContinuousOn (Y := ℂ) (fun (x : α) ↦ f x ^ b) s

Tactic:
hf.cpow continuousOn_const h

Premises used: continuousOn_const, ContinuousOn.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
inst : NeZero z
⊢ Continuous (Y := ℂ) fun (s : ℂ) ↦ z ^ s

Tactic:
continuous_id.const_cpow (.inl <| NeZero.ne z)

Premises used: continuous_id, Continuous.const_cpow, Or.inl, NeZero.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ ((↑a : ℂ) ^ (↑x : ℂ)).re) b

Tactic:
Complex.continuous_re.continuousAt.comp ?_

Premises used: Complex.continuous_re, Continuous.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℝ
h : a ≠ 0
refine : ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) ^ (↑x : ℂ)) b
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ ((↑a : ℂ) ^ (↑x : ℂ)).re) b

Tactic:
refine Complex.continuous_re.continuousAt.comp ?_

Premises used: Complex.continuous_re, Continuous.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) ^ (↑x : ℂ)) b

Tactic:
(continuousAt_const_cpow ?_).comp Complex.continuous_ofReal.continuousAt

Premises used: continuousAt_const_cpow, Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℝ
h : a ≠ 0
refine : (↑a : ℂ) ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) ^ (↑x : ℂ)) b

Tactic:
refine (continuousAt_const_cpow ?_).comp Complex.continuous_ofReal.continuousAt

Premises used: continuousAt_const_cpow, Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℝ
h : a ≠ 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬a = 0
⊢ (↑a : ℂ) ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ ((↑a : ℂ) ^ (↑x : ℂ)).re) b

Tactic:
Complex.continuous_re.continuousAt.comp ?_

Premises used: Complex.continuous_re, Continuous.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℝ
h : b ≠ 0
refine : ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) ^ (↑x : ℂ)) b
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ ((↑a : ℂ) ^ (↑x : ℂ)).re) b

Tactic:
refine Complex.continuous_re.continuousAt.comp ?_

Premises used: Complex.continuous_re, Continuous.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) ^ (↑x : ℂ)) b

Tactic:
(continuousAt_const_cpow' ?_).comp Complex.continuous_ofReal.continuousAt

Premises used: Continuous.continuousAt, continuousAt_const_cpow', Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℝ
h : b ≠ 0
refine : (↑b : ℂ) ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) ^ (↑x : ℂ)) b

Tactic:
refine (continuousAt_const_cpow' ?_).comp Complex.continuous_ofReal.continuousAt

Premises used: Continuous.continuousAt, continuousAt_const_cpow', Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℝ
h : b ≠ 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬b = 0
⊢ (↑b : ℂ) ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp_fst : p.1 < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0
x : ℝ × ℝ
hx : x.1 < 0
rw rw₁ : rexp (log x.1 * x.2) * cos (x.2 * π) = rexp (log x.1 * x.2) * cos (x.2 * π)
⊢ x.1 ^ x.2 = rexp (log x.1 * x.2) * cos (x.2 * π)

Tactic:
rw [rpow_def_of_neg hx]

Premises used: Real.rpow_def_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp_fst : p.1 < 0
suffices : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0
⊢ (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)

Tactic:
suffices ∀ᶠ x : ℝ × ℝ in 𝓝 p, x.1 < 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [rpow_def_of_neg hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp_fst : p.1 < 0
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0

Tactic:
IsOpen.eventually_mem (isOpen_lt continuous_fst continuous_const) hp_fst

Premises used: isOpen_lt, Set.Mem, IsOpen.eventually_mem, continuous_const, continuous_fst
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp_fst : p.1 < 0
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0

Tactic:
exact IsOpen.eventually_mem (isOpen_lt continuous_fst continuous_const) hp_fst

Premises used: isOpen_lt, IsOpen.eventually_mem, continuous_const, continuous_fst
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp_fst : 0 < p.1
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1
x : ℝ × ℝ
hx : 0 < x.1
rw rw₁ : rexp (log x.1 * x.2) = rexp (log x.1 * x.2)
⊢ x.1 ^ x.2 = rexp (log x.1 * x.2)

Tactic:
rw [rpow_def_of_pos hx]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp_fst : 0 < p.1
suffices : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1
⊢ (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)

Tactic:
suffices ∀ᶠ x : ℝ × ℝ in 𝓝 p, 0 < x.1 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [rpow_def_of_pos hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp_fst : 0 < p.1
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1

Tactic:
IsOpen.eventually_mem (isOpen_lt continuous_const continuous_fst) hp_fst

Premises used: isOpen_lt, Set.Mem, IsOpen.eventually_mem, continuous_const, continuous_fst
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp_fst : 0 < p.1
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1

Tactic:
exact IsOpen.eventually_mem (isOpen_lt continuous_const continuous_fst) hp_fst

Premises used: isOpen_lt, IsOpen.eventually_mem, continuous_const, continuous_fst
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : p.1 ≠ 0
⊢ p.1 < 0 ∨ 0 < p.1

Tactic:
rw [ne_iff_lt_or_gt] at hp

Premises used: ne_iff_lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : p.1 < 0
inl : ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)) p
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p

Tactic:
rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]

Premises used: Real.rpow_eq_nhds_of_neg, continuousAt_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ cos (x.2 * π)) p

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : p.1 < 0
inl : ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)) p
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)) p

Tactic:
refine ContinuousAt.mul ?_ (by fun_prop)

Premises used: ContinuousAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)) p

Tactic:
continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)

Premises used: continuous_snd, Real.exp, Continuous.continuousAt, Real.continuous_exp, ContinuousAt.mul, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : p.1 < 0
inl : ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ log x.1) p
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)) p

Tactic:
refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)

Premises used: continuous_snd, Continuous.continuousAt, Real.continuous_exp, ContinuousAt.mul, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ log x.1) p

Tactic:
(continuousAt_log hp.ne).comp continuous_fst.continuousAt

Premises used: continuous_fst, Real.log, dite, Continuous.continuousAt, ContinuousAt.comp, Real.continuousAt_log, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ log x.1) p

Tactic:
exact (continuousAt_log hp.ne).comp continuous_fst.continuousAt

Premises used: continuous_fst, Continuous.continuousAt, ContinuousAt.comp, Real.continuousAt_log, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : 0 < p.1
inr : ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)) p
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p

Tactic:
rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]

Premises used: continuousAt_congr, Real.rpow_eq_nhds_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : 0 < p.1
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)) p

Tactic:
continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)

Premises used: continuous_snd, Real.exp, Continuous.continuousAt, Real.continuous_exp, ContinuousAt.mul, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : 0 < p.1
inr : ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ log x.1) p
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)) p

Tactic:
refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)

Premises used: continuous_snd, Continuous.continuousAt, Real.continuous_exp, ContinuousAt.mul, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : 0 < p.1
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ log x.1) p

Tactic:
(continuousAt_log ?_).comp continuous_fst.continuousAt

Premises used: continuous_fst, Real.log, dite, Continuous.continuousAt, ContinuousAt.comp, Real.continuousAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : 0 < p.1
inr : p.1 ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ log x.1) p

Tactic:
refine (continuousAt_log ?_).comp continuous_fst.continuousAt

Premises used: continuous_fst, Continuous.continuousAt, ContinuousAt.comp, Real.continuousAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : 0 < p.1
⊢ p.1 ≠ 0

Tactic:
hp.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : 0 < p.1
⊢ p.1 ≠ 0

Tactic:
exact hp.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : p.1 < 0 ∨ 0 < p.1
inl : ∀ (hp : p.1 < 0), ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
inr : ∀ (hp : 0 < p.1), ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p

Tactic:
cases hp with
  | inl hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
    refine ContinuousAt.mul ?_ (by fun_prop)
    · refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
      exact (continuousAt_log hp.ne).comp continuous_fst.continuousAt
  | inr hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
    refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
    refine (continuousAt_log ?_).comp continuous_fst.continuousAt
    exact hp.ne'

Premises used: continuous_snd, continuous_fst, Continuous.continuousAt, Real.continuous_exp, ContinuousAt.mul, ContinuousAt.comp, Real.continuousAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
hp : 0 < p.2
obtain : ∀ (x y : ℝ) (hp : 0 < (x, y).2), ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (x, y)
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p

Tactic:
obtain ⟨x, y⟩ := p
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ
hp : 0 < y
inl : ∀ (hx : x ≠ 0), ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (x, y)
inr : ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (0, y)
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (x, y)

Tactic:
obtain hx | rfl := ne_or_eq x 0

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ
hp : 0 < y
hx : x ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (x, y)

Tactic:
continuousAt_rpow_of_ne (x, y) hx

Premises used: Prod.mk, Real.continuousAt_rpow_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x y : ℝ
hp : 0 < y
hx : x ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (x, y)

Tactic:
exact continuousAt_rpow_of_ne (x, y) hx

Premises used: Prod.mk, Real.continuousAt_rpow_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
hp : 0 < y
⊢ Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ rexp (log p.1 * p.2)) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)

Tactic:
have A : Tendsto (fun p : ℝ × ℝ => exp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0) :=
    tendsto_exp_atBot.comp
      ((tendsto_log_nhdsNE_zero.comp tendsto_fst).atBot_mul_pos hp tendsto_snd)
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
hp : 0 < y
A : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ rexp (log p.1 * p.2)) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)

Tactic:
have B : Tendsto (fun p : ℝ × ℝ => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0) :=
    squeeze_zero_norm (fun p => abs_rpow_le_exp_log_mul p.1 p.2) A
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
hp : 0 < y
A : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ rexp (log p.1 * p.2)) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
B : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
rw : ∀ᶠ (a : ℝ) in 𝓝 y, HPow.hPow (α := ℝ) (0, a).1 (0, a).2 = 0
⊢ Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[{0}] 0) (𝓝 y)) (pure 0)

Tactic:
rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]

Premises used: nhdsWithin_singleton, Filter.pure_prod, Filter.eventually_map, Filter.tendsto_pure
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
hp : 0 < y
A : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ rexp (log p.1 * p.2)) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
B : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
⊢ ∀ᶠ (a : ℝ) in 𝓝 y, HPow.hPow (α := ℝ) (0, a).1 (0, a).2 = 0

Tactic:
(lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'

Premises used: Real.zero_rpow, Filter.Eventually.mono, LT.lt.ne', lt_mem_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
hp : 0 < y
A : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ rexp (log p.1 * p.2)) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
B : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
⊢ ∀ᶠ (a : ℝ) in 𝓝 y, HPow.hPow (α := ℝ) (0, a).1 (0, a).2 = 0

Tactic:
exact (lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'

Premises used: Real.zero_rpow, Filter.Eventually.mono, LT.lt.ne', lt_mem_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
hp : 0 < y
A : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ rexp (log p.1 * p.2)) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
B : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[{0}] 0) (𝓝 y)) (pure 0)

Tactic:
have C : Tendsto (fun p : ℝ × ℝ => p.1 ^ p.2) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0) := by
    rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]
    exact (lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℝ
hp : 0 < y
A : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ rexp (log p.1 * p.2)) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
B : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
C : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[{0}] 0) (𝓝 y)) (pure 0)
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (0, y)

Tactic:
simpa only [← sup_prod, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ, nhds_prod_eq,
    ContinuousAt, zero_rpow hp.ne'] using B.sup (C.mono_right (pure_le_nhds _))

Premises used: nhdsWithin_univ, ContinuousAt, pure_le_nhds, Real.zero_rpow, LT.lt.ne', Filter.Tendsto.sup, nhdsWithin_union, nhds_prod_eq, Set.compl_union_self, Filter.Tendsto.mono_right, Filter.sup_prod
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℝ × ℝ
h : p.1 ≠ 0 ∨ 0 < p.2
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p

Tactic:
h.elim (fun h => continuousAt_rpow_of_ne p h) fun h => continuousAt_rpow_of_pos p h

Premises used: Real.continuousAt_rpow_of_pos, Real.continuousAt_rpow_of_ne, Or.elim
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x q : ℝ
h : x ≠ 0 ∨ 0 ≤ q
⊢ (x ≠ 0 ∨ 0 < q) ∨ 0 = q

Tactic:
rw [le_iff_lt_or_eq, ← or_assoc] at h

Premises used: le_iff_lt_or_eq, or_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x q : ℝ
h : (x ≠ 0 ∨ 0 < q) ∨ 0 = q
inl : ∀ (h : x ≠ 0 ∨ 0 < q), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ q) x
inr : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0) x
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ q) x

Tactic:
obtain h | rfl := h

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ q) x

Tactic:
(continuousAt_rpow (x, q) h).comp₂ continuousAt_id continuousAt_const

Premises used: ContinuousAt.comp₂, continuousAt_const, continuousAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ q) x

Tactic:
exact (continuousAt_rpow (x, q) h).comp₂ continuousAt_id continuousAt_const

Premises used: ContinuousAt.comp₂, continuousAt_const, continuousAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
inr : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1) x
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0) x

Tactic:
simp_rw [rpow_zero]

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

Tactic:
continuousAt_const

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

Tactic:
exact continuousAt_const

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

Tactic:
continuous_iff_continuousAt.mpr fun x ↦ continuousAt_rpow_const x q (.inr h)

Premises used: Iff.mpr, Real.continuousAt_rpow_const, Or.inr, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a : ℝ
h : a ≠ 0
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ a ^ x

Tactic:
continuous_iff_continuousAt.mpr fun _ ↦ continuousAt_const_rpow h

Premises used: Iff.mpr, Real.continuousAt_const_rpow, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
x y : ℝ
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
h : x ≠ 0 ∨ 0 < y
⊢ Tendsto (fun (t : α) ↦ f t ^ g t) l (𝓝 (x ^ y))

Tactic:
(Real.continuousAt_rpow (x, y) h).tendsto.comp (hf.prodMk_nhds hg)

Premises used: Prod.mk, ContinuousAt.tendsto, Real.continuousAt_rpow, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
x p : ℝ
hf : Tendsto f l (𝓝 x)
h : x ≠ 0 ∨ 0 ≤ p
h0 : 0 = p
⊢ Tendsto (fun (a : α) ↦ HPow.hPow (β := ℝ) (f a) 0) l (𝓝 (HPow.hPow (β := ℝ) x 0))

Tactic:
simp [tendsto_const_nhds]

Premises used: tendsto_const_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
p : ℝ
hf : Tendsto f l (𝓝 0)
hp : 0 < p
⊢ Tendsto (β := ℝ) (fun (t : α) ↦ f t ^ p) l (𝓝 0)

Tactic:
Real.zero_rpow hp.ne' ▸ hf.rpow_const (.inr hp.le)

Premises used: Eq.rec, LT.lt.le, Filter.Tendsto.rpow_const, Real.zero_rpow, LT.lt.ne', Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f g : α → ℝ
x : α
hf : ContinuousAt f x
hg : ContinuousAt g x
h : f x ≠ 0 ∨ 0 < g x
⊢ ContinuousAt (Y := ℝ) (fun (t : α) ↦ f t ^ g t) x

Tactic:
hf.rpow hg h

Premises used: ContinuousAt, Filter.Tendsto.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f g : α → ℝ
s : Set α
x : α
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
h : f x ≠ 0 ∨ 0 < g x
⊢ ContinuousWithinAt (Y := ℝ) (fun (t : α) ↦ f t ^ g t) s x

Tactic:
hf.rpow hg h

Premises used: ContinuousWithinAt, Filter.Tendsto.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f g : α → ℝ
s : Set α
hf : ContinuousOn f s
hg : ContinuousOn g s
h : ∀ x ∈ s, f x ≠ 0 ∨ 0 < g x
⊢ ContinuousOn (Y := ℝ) (fun (t : α) ↦ f t ^ g t) s

Tactic:
fun t ht =>
  (hf t ht).rpow (hg t ht) (h t ht)

Premises used: ContinuousOn, ContinuousWithinAt.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f g : α → ℝ
hf : Continuous[inst, _] f
hg : Continuous[inst, _] g
h : ∀ (x : α), f x ≠ 0 ∨ 0 < g x
⊢ Continuous[inst, _] fun (x : α) ↦ f x ^ g x

Tactic:
continuous_iff_continuousAt.2 fun x => hf.continuousAt.rpow hg.continuousAt (h x)

Premises used: Iff.mpr, ContinuousAt.rpow, Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
s : Set α
x : α
p : ℝ
hf : ContinuousWithinAt f s x
h : f x ≠ 0 ∨ 0 ≤ p
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : α) ↦ f x ^ p) s x

Tactic:
hf.rpow_const h

Premises used: ContinuousWithinAt, Filter.Tendsto.rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
x : α
p : ℝ
hf : ContinuousAt f x
h : f x ≠ 0 ∨ 0 ≤ p
⊢ ContinuousAt (Y := ℝ) (fun (x : α) ↦ f x ^ p) x

Tactic:
hf.rpow_const h

Premises used: ContinuousAt, Filter.Tendsto.rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
s : Set α
p : ℝ
hf : ContinuousOn f s
h : ∀ x ∈ s, f x ≠ 0 ∨ 0 ≤ p
⊢ ContinuousOn (Y := ℝ) (fun (x : α) ↦ f x ^ p) s

Tactic:
fun x hx => (hf x hx).rpow_const (h x hx)

Premises used: ContinuousWithinAt.rpow_const, ContinuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
p : ℝ
hf : Continuous[inst, _] f
h : ∀ (x : α), f x ≠ 0 ∨ 0 ≤ p
⊢ Continuous[inst, _] fun (x : α) ↦ f x ^ p

Tactic:
continuous_iff_continuousAt.2 fun x => hf.continuousAt.rpow_const (h x)

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.rpow_const, continuous_iff_continuousAt