awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
⊢ z ≠ 0

Tactic:
have hz₀ : z ≠ 0 := ne_of_apply_ne re hz.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
rw : Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1 ^ x.2‖) (𝓝 (0, z)) (𝓝 0)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (0, z)

Tactic:
rw [ContinuousAt, zero_cpow hz₀, tendsto_zero_iff_norm_tendsto_zero]

Premises used: ContinuousAt, Complex.zero_cpow, tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1 ^ x.2‖) (𝓝 (0, z)) (𝓝 0)

Tactic:
squeeze_zero (fun _ => norm_nonneg _) (fun _ => norm_cpow_le _ _) ?_

Premises used: squeeze_zero, Prod.fst, HPow.hPow, Complex.norm_cpow_le, Prod.snd, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
refine : Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re / rexp (x.1.arg * x.2.im)) (𝓝 (0, z)) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1 ^ x.2‖) (𝓝 (0, z)) (𝓝 0)

Tactic:
refine squeeze_zero (fun _ => norm_nonneg _) (fun _ => norm_cpow_le _ _) ?_

Premises used: squeeze_zero, Complex.norm_cpow_le, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
simp : Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re * rexp (-(x.1.arg * x.2.im))) (𝓝 (0, z)) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re / rexp (x.1.arg * x.2.im)) (𝓝 (0, z)) (𝓝 0)

Tactic:
simp only [div_eq_mul_inv, ← Real.exp_neg]

Premises used: div_eq_mul_inv, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re * rexp (-(x.1.arg * x.2.im))) (𝓝 (0, z)) (𝓝 0)

Tactic:
Tendsto.zero_mul_isBoundedUnder_le ?_ ?_

Premises used: Filter.Tendsto.zero_mul_isBoundedUnder_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
refine_1 : Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re) (𝓝 (0, z)) (𝓝 0)
refine_2 :
  IsBoundedUnder (β := ℂ × ℂ) (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z))
    ((fun (x : ℝ) ↦ ‖x‖) ∘ fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im)))
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re * rexp (-(x.1.arg * x.2.im))) (𝓝 (0, z)) (𝓝 0)

Tactic:
refine Tendsto.zero_mul_isBoundedUnder_le ?_ ?_

Premises used: Filter.Tendsto.zero_mul_isBoundedUnder_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun (t : ℂ × ℂ) ↦ ‖t.1‖ ^ (re ∘ Prod.snd) t) (𝓝 (0, z))
    (𝓝 (Norm.norm (E := ℂ) (0, z).1 ^ Function.comp (α := ℂ × ℂ) re Prod.snd (0, z)))

Tactic:
(continuous_fst.norm.tendsto ((0 : ℂ), z)).rpow ((continuous_re.comp continuous_snd).tendsto _)
      _

Premises used: Complex.continuous_re, Continuous.comp, continuous_snd, continuous_fst, Prod.mk, Continuous.norm, Continuous.tendsto, Filter.Tendsto.rpow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
h : 0 = Norm.norm (E := ℂ) (0, z).1 ^ Function.comp (α := ℂ × ℂ) re Prod.snd (0, z)
refine_1 : Norm.norm (E := ℂ) (0, z).1 ≠ 0 ∨ 0 < Function.comp (α := ℂ × ℂ) re Prod.snd (0, z)
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re) (𝓝 (0, z)) (𝓝 0)

Tactic:
convert!
    (continuous_fst.norm.tendsto ((0 : ℂ), z)).rpow ((continuous_re.comp continuous_snd).tendsto _)
      _

Premises used: Complex.continuous_re, Continuous.comp, continuous_snd, continuous_fst, Prod.mk, Continuous.norm, Continuous.tendsto, Filter.Tendsto.rpow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ 0 = Norm.norm (E := ℂ) (0, z).1 ^ Function.comp (α := ℂ × ℂ) re Prod.snd (0, z)

Tactic:
simp [hz, Real.zero_rpow hz.ne']

Premises used: Real.zero_rpow, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Norm.norm (E := ℂ) (0, z).1 ≠ 0 ∨ 0 < Function.comp (α := ℂ × ℂ) re Prod.snd (0, z)

Tactic:
simp [hz, Real.zero_rpow hz.ne']

Premises used: Real.zero_rpow, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
refine_2 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z)) fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im))
⊢ IsBoundedUnder (β := ℂ × ℂ) (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z))
    ((fun (x : ℝ) ↦ ‖x‖) ∘ fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im)))

Tactic:
simp only [Function.comp_def, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]

Premises used: Function.comp_def, abs_of_pos, Real.norm_eq_abs, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
refine_2 :
  ∀ (C : ℝ) (hC : |z.im| < C),
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z)) fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im))
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z)) fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im))

Tactic:
rcases exists_gt |im z| with ⟨C, hC⟩

Premises used: abs, Complex.im, NoMaxOrder.exists_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z)) fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im))

Tactic:
⟨Real.exp (π * C), eventually_map.2 ?_⟩

Premises used: Iff.mpr, Real.pi, HMul.hMul, Filter.IsBounded, Real.exp, Filter.eventually_map, Exists.intro, Filter.IsBoundedUnder
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
refine_2 : ∀ᶠ (a : ℂ × ℂ) in 𝓝 (0, z), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (rexp (-(a.1.arg * a.2.im))) (rexp (π * C))
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z)) fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im))

Tactic:
refine ⟨Real.exp (π * C), eventually_map.2 ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
⊢ ∀ᶠ (a : ℂ × ℂ) in 𝓝 (0, z), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (rexp (-(a.1.arg * a.2.im))) (rexp (π * C))

Tactic:
(((continuous_im.comp continuous_snd).abs.tendsto (_, z)).eventually (gt_mem_nhds hC)).mono
        fun z hz => Real.exp_le_exp.2 <| (neg_le_abs _).trans ?_

Premises used: Iff.mpr, gt_mem_nhds, HMul.hMul, Complex.im, Continuous.comp, continuous_snd, Complex.arg, Continuous.abs, Prod.mk, Prod.fst, Filter.Eventually.mono, Continuous.tendsto, Real.exp_le_exp, neg_le_abs, Filter.Tendsto.eventually, LE.le.trans, Prod.snd, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
refine_2 : ∀ (z : ℂ × ℂ) (hz : |(im ∘ Prod.snd) z| < C), |z.1.arg * z.2.im| ≤ π * C
⊢ ∀ᶠ (a : ℂ × ℂ) in 𝓝 (0, z), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (rexp (-(a.1.arg * a.2.im))) (rexp (π * C))

Tactic:
refine
      (((continuous_im.comp continuous_snd).abs.tendsto (_, z)).eventually (gt_mem_nhds hC)).mono
        fun z hz => Real.exp_le_exp.2 <| (neg_le_abs _).trans ?_

Premises used: Iff.mpr, gt_mem_nhds, Continuous.comp, continuous_snd, Continuous.abs, Prod.mk, Filter.Eventually.mono, Continuous.tendsto, Real.exp_le_exp, neg_le_abs, Filter.Tendsto.eventually, LE.le.trans, Complex.continuous_im
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z_1 : ℂ
hz_1 : 0 < z_1.re
hz₀ : z_1 ≠ 0
C : ℝ
hC : |z_1.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
refine_2 : |z.1.arg| * |z.2.im| ≤ π * C
⊢ |z.1.arg * z.2.im| ≤ π * C

Tactic:
rw [_root_.abs_mul]

Premises used: abs_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z_1 : ℂ
hz_1 : 0 < z_1.re
hz₀ : z_1 ≠ 0
C : ℝ
hC : |z_1.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |z.1.arg| * |z.2.im| ≤ π * C

Tactic:
mul_le_mul (abs_le.2 ⟨(neg_pi_lt_arg _).le, arg_le_pi _⟩) hz.le (_root_.abs_nonneg _)
        Real.pi_pos.le

Premises used: Iff.mpr, Complex.arg_le_pi, abs_le, Real.pi_pos, LT.lt.le, Complex.neg_pi_lt_arg, mul_le_mul, And.intro, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z_1 : ℂ
hz_1 : 0 < z_1.re
hz₀ : z_1 ≠ 0
C : ℝ
hC : |z_1.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |z.1.arg| * |z.2.im| ≤ π * C

Tactic:
exact
      mul_le_mul (abs_le.2 ⟨(neg_pi_lt_arg _).le, arg_le_pi _⟩) hz.le (_root_.abs_nonneg _)
        Real.pi_pos.le

Premises used: Iff.mpr, Complex.arg_le_pi, abs_le, Real.pi_pos, LT.lt.le, Complex.neg_pi_lt_arg, mul_le_mul, And.intro, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℂ × ℂ
h₁ : 0 ≤ p.1.re ∨ p.1.im ≠ 0
h₂ : 0 < p.2.re
obtain :
  ∀ (z w : ℂ) (h₁ : 0 ≤ (z, w).1.re ∨ (z, w).1.im ≠ 0) (h₂ : 0 < (z, w).2.re),
    ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (z, w)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) p

Tactic:
obtain ⟨z, w⟩ := p
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z w : ℂ
h₁ : 0 ≤ (z, w).1.re ∨ (z, w).1.im ≠ 0
h₂ : 0 < (z, w).2.re
⊢ (0 < (z, w).1.re ∨ (z, w).1.im ≠ 0) ∨ (z, w).1 = 0

Tactic:
rw [← not_lt_zero_iff, lt_iff_le_and_ne, not_and_or, Ne, Classical.not_not,
    not_le_zero_iff] at h₁

Premises used: lt_iff_le_and_ne, Classical.not_not, Ne, Complex.not_le_zero_iff, not_and_or, Complex.not_lt_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z w : ℂ
h₁ : 0 ≤ (z, w).1.re ∨ (z, w).1.im ≠ 0
h₂ : 0 < (z, w).2.re
h₃ : (0 < (z, w).1.re ∨ (z, w).1.im ≠ 0) ∨ (z, w).1 = 0
⊢ 0 < (z, w).2.re

Tactic:
rw [← not_lt_zero_iff, lt_iff_le_and_ne, not_and_or, Ne, Classical.not_not,
    not_le_zero_iff] at h₁

Premises used: lt_iff_le_and_ne, Classical.not_not, Ne, Complex.not_le_zero_iff, not_and_or, Complex.not_lt_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z w : ℂ
h₁ : (0 < (z, w).1.re ∨ (z, w).1.im ≠ 0) ∨ (z, w).1 = 0
h₂ : 0 < (z, w).2.re
inl : ∀ (h₁ : 0 < (z, w).1.re ∨ (z, w).1.im ≠ 0), ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (z, w)
inr : ∀ (h₂ : 0 < (0, w).2.re), ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (0, w)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (z, w)

Tactic:
rcases h₁ with (h₁ | (rfl : z = 0))

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z w : ℂ
h₂ : 0 < (z, w).2.re
h₁ : 0 < (z, w).1.re ∨ (z, w).1.im ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (z, w)

Tactic:
continuousAt_cpow h₁

Premises used: continuousAt_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
w : ℂ
h₂ : 0 < (0, w).2.re
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (0, w)

Tactic:
continuousAt_cpow_zero_of_re_pos h₂

Premises used: Complex.continuousAt_cpow_zero_of_re_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z w : ℂ
h₂ : 0 < (z, w).2.re
h₁ : 0 < (z, w).1.re ∨ (z, w).1.im ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (z, w)

Tactic:
exacts [continuousAt_cpow h₁, continuousAt_cpow_zero_of_re_pos h₂]

Premises used: continuousAt_cpow, Complex.continuousAt_cpow_zero_of_re_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
z w : ℂ
hz : 0 ≤ z.re ∨ z.im ≠ 0
hw : 0 < w.re
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ x ^ w) z

Tactic:
Tendsto.comp (@continuousAt_cpow_of_re_pos (z, w) hz hw)
    (continuousAt_id.prodMk continuousAt_const)

Premises used: ContinuousAt, continuousAt_const, Filter.Tendsto.comp, Complex.continuousAt_cpow_of_re_pos, ContinuousAt.prodMk, continuousAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
inl : ∀ (hx : 0 < x), ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
inr : ∀ (h : 0 < y.re ∨ Ne (α := ℝ) 0 0), ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (0, y)
inr₁ : ∀ (hx : x < 0), ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)

Tactic:
rcases lt_trichotomy (0 : ℝ) x with (hx | rfl | hx)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (x, y)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (x, y)

Tactic:
have : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)

Tactic:
(continuousAt_cpow (Or.inl ?_)).comp this

Premises used: continuousAt_cpow, ContinuousAt.comp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (x, y)
inl : 0 < ((↑(x, y).1 : ℂ), (x, y).2).1.re
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)

Tactic:
refine (continuousAt_cpow (Or.inl ?_)).comp this

Premises used: continuousAt_cpow, ContinuousAt.comp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (x, y)
inl inl₁ inl₂ inl₃ : 0 < (x, y).1
⊢ 0 < ((↑(x, y).1 : ℂ), (x, y).2).1.re

Tactic:
rwa [ofReal_re]

Premises used: Complex.ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
hz : 0 < y.re
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ p.1 ^ p.2) (0, y)

Tactic:
apply continuousAt_cpow_zero_of_re_pos

Premises used: Complex.continuousAt_cpow_zero_of_re_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
hz : ∀ (h : 0 < y.re), 0 < y.re
hz₁ : ∀ (h : Ne (α := ℝ) 0 0), 0 < y.re
hz₂ hz₃ : ∀ (h : 0 < y.re), 0 < y.re
⊢ 0 < y.re

Tactic:
tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ p.1 ^ p.2) ((↑0 : ℂ), y)

Tactic:
have A : ContinuousAt (fun p => p.1 ^ p.2 : ℂ × ℂ → ℂ) ⟨↑(0 : ℝ), y⟩ := by
      rw [ofReal_zero]
      apply continuousAt_cpow_zero_of_re_pos
      tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
A : ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ p.1 ^ p.2) ((↑0 : ℂ), y)
⊢ ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (0, y)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
A : ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ p.1 ^ p.2) ((↑0 : ℂ), y)
⊢ ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (0, y)

Tactic:
have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ := by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
A : ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ p.1 ^ p.2) ((↑0 : ℂ), y)
B : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (0, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (0, y)

Tactic:
A.comp_of_eq B rfl

Premises used: ContinuousAt.comp_of_eq, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
A : ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ p.1 ^ p.2) ((↑0 : ℂ), y)
B : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (0, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (0, y)

Tactic:
exact A.comp_of_eq B rfl

Premises used: ContinuousAt.comp_of_eq, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)

Tactic:
this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) ?_)

Premises used: prod_mem_nhds, Iio_mem_nhds, ContinuousAt.congr, Filter.eventually_of_mem, Filter.univ_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) (x, y)
refine :
  ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set ℂ) (Set.Iio 0) Set.univ,
    Eq (α := ℂ) ((fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) x)
      ((fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) x)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)

Tactic:
refine this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) ?_)

Premises used: prod_mem_nhds, Iio_mem_nhds, ContinuousAt.congr, Filter.eventually_of_mem, Filter.univ_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) (x, y)
⊢ ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set ℂ) (Set.Iio 0) Set.univ,
    Eq (α := ℂ) ((fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) x)
      ((fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) x)

Tactic:
fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm

Premises used: Complex.ofReal_cpow_of_nonpos, le_of_lt, And.left, Eq.symm, Prod.snd
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) (x, y)
⊢ ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set ℂ) (Set.Iio 0) Set.univ,
    Eq (α := ℂ) ((fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) x)
      ((fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) x)

Tactic:
exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm

Premises used: Complex.ofReal_cpow_of_nonpos, le_of_lt, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
inr : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)

Tactic:
suffices ContinuousAt (fun p => (-(p.1 : ℂ)) ^ p.2 * exp (π * I * p.2) : ℝ × ℂ → ℂ) (x, y) by
      refine this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) ?_)
      exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)

Tactic:
have A : ContinuousAt (fun p => ⟨-↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
inr : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2) (x, y)
inr₁ : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ cexp ((↑π : ℂ) * I * p.2)) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) (x, y)

Tactic:
apply ContinuousAt.mul

Premises used: ContinuousAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2) (x, y)

Tactic:
(continuousAt_cpow (Or.inl ?_)).comp A

Premises used: continuousAt_cpow, ContinuousAt.comp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
inr : 0 < (-(↑(x, y).1 : ℂ), (x, y).2).1.re
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2) (x, y)

Tactic:
refine (continuousAt_cpow (Or.inl ?_)).comp A

Premises used: continuousAt_cpow, ContinuousAt.comp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
inr : 0 < -(↑(x, y).1 : ℂ).re
inr₁ : 0 < -(x, y).1
inr₂ inr₃ inr₄ inr₅ : (x, y).1 < 0
⊢ 0 < (-(↑(x, y).1 : ℂ), (x, y).2).1.re

Tactic:
rwa [neg_re, ofReal_re, neg_pos]

Premises used: neg_pos, Complex.neg_re, Complex.ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ cexp ((↑π : ℂ) * I * p.2)) (x, y)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (a : ℝ) ↦ a) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (a : ℝ) ↦ y) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
y : ℂ
hs : 0 < y.re
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ (↑x : ℂ) ^ y

Tactic:
continuous_iff_continuousAt.mpr fun x => continuousAt_ofReal_cpow_const x y (Or.inl hs)

Premises used: Iff.mpr, Or.inl, Complex.continuousAt_ofReal_cpow_const, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
h₁ :
  ∀ (p : ℝ≥0 × ℝ),
    (↑(p.1 ^ p.2) : ℝ) = (↑((toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) p) : ℝ)
⊢ 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))

Tactic:
ext p
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
h₁ : 0 ≤ (↑p.1 : ℝ) ^ p.2
⊢ (↑(p.1 ^ p.2) : ℝ) = (↑((toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) p) : ℝ)

Tactic:
simp only [coe_rpow, val_eq_coe, Function.comp_apply, coe_toNNReal', left_eq_sup]

Premises used: NNReal.coe_rpow, Real.coe_toNNReal', NNReal.val_eq_coe, left_eq_sup, Function.comp_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
⊢ 0 ≤ (↑p.1 : ℝ) ^ p.2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
⊢ 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))

Tactic:
have :
    (fun p : ℝ≥0 × ℝ => p.1 ^ p.2) =
      Real.toNNReal ∘ (fun p : ℝ × ℝ => p.1 ^ p.2) ∘ fun p : ℝ≥0 × ℝ => (p.1.1, p.2) := by
    ext p
    simp only [coe_rpow, val_eq_coe, Function.comp_apply, coe_toNNReal', left_eq_sup]
    positivity
-- 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))
rw : ContinuousAt (toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) (x, y)
⊢ ContinuousAt (Y := ℝ≥0) (fun (p : ℝ≥0 × ℝ) ↦ p.1 ^ p.2) (x, y)

Tactic:
rw [this]
-- 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 (toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) (x, y)

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

Premises used: Continuous.continuousAt, continuous_real_toNNReal, ContinuousAt.comp