-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_cpow_zero_of_re_pos {z : ℂ} (hz : 0 < z.re) :
    ContinuousAt (fun x : ℂ × ℂ => x.1 ^ x.2) (0, z)

Proof state:
case refine_2.intro
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:
refine ⟨Real.exp (π * C), eventually_map.2 ?_⟩

Result:
case refine_2.intro
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))

Proof state:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ‖x.1 ^ x.2‖) (𝓝 (0, z)) (𝓝 0)

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

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

Proof state:
case refine_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |z.1.arg * z.2.im| ≤ π * C

Tactic:
rw [_root_.abs_mul]

Result:
case refine_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |z.1.arg| * |z.2.im| ≤ π * C

Proof state:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ContinuousAt (fun x => x.1 ^ x.2) (0, z)

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

Result:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ‖x.1 ^ x.2‖) (𝓝 (0, z)) (𝓝 0)

Proof state:
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:
simp only [div_eq_mul_inv, ← Real.exp_neg]

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

Proof state:
case refine_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ 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 _)]

Result:
case refine_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 (0, z)) fun x => rexp (-(x.1.arg * x.2.im))

Proof state:
case refine_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ 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⟩

Result:
case refine_2.intro
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))

Proof state:
case refine_2.intro
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:
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 ?_

Result:
case refine_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |z.1.arg * z.2.im| ≤ π * C

Proof state:
z : ℂ
hz : 0 < z.re
⊢ ContinuousAt (fun x => x.1 ^ x.2) (0, z)

Tactic:
have hz₀ : z ≠ 0 := ne_of_apply_ne re hz.ne'

Result:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ContinuousAt (fun x => x.1 ^ x.2) (0, z)

Proof state:
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:
refine Tendsto.zero_mul_isBoundedUnder_le ?_ ?_

Result:
case refine_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ‖x.1‖ ^ x.2.re) (𝓝 (0, z)) (𝓝 0)

case refine_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 (0, z)) ((fun x => ‖x‖) ∘ fun x => rexp (-(x.1.arg * x.2.im)))

Proof state:
case refine_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ 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 _) _ <;>
  simp [hz, Real.zero_rpow hz.ne']

Result:
no goals

Proof state:
case refine_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.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

Result:
no goals