z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (0, z)
z : ℂ
hz : 0 < z.re
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (0, z)
have hz₀ : z ≠ 0 := ne_of_apply_ne re hz.ne'
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun e => ‖e.fst ^ e.snd‖) (𝓝 (0, z)) (𝓝 0)
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ContinuousAt (fun x => x.fst ^ x.snd) (0, z)
rw [ContinuousAt, zero_cpow hz₀, tendsto_zero_iff_norm_tendsto_zero]
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re / Real.exp (arg x.fst * x.snd.im)) (𝓝 (0, z)) (𝓝 0)
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun e => ‖e.fst ^ e.snd‖) (𝓝 (0, z)) (𝓝 0)
refine' squeeze_zero (fun _ => norm_nonneg _) (fun _ => abs_cpow_le _ _) _
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re * Real.exp (-(arg x.fst * x.snd.im))) (𝓝 (0, z)) (𝓝 0)
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re / Real.exp (arg x.fst * x.snd.im)) (𝓝 (0, z)) (𝓝 0)
simp only [div_eq_mul_inv, ← Real.exp_neg]
case refine'_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re) (𝓝 (0, z)) (𝓝 0)

case refine'_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) ((fun x => ‖x‖) ∘ fun x => Real.exp (-(arg x.fst * x.snd.im)))
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re * Real.exp (-(arg x.fst * x.snd.im))) (𝓝 (0, z)) (𝓝 0)
refine' Tendsto.zero_mul_isBoundedUnder_le _ _
no goals
case refine'_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x => ↑abs x.fst ^ x.snd.re) (𝓝 (0, z)) (𝓝 0)
convert
    (continuous_fst.norm.tendsto ((0 : ℂ), z)).rpow
      ((continuous_re.comp continuous_snd).tendsto _) _ <;>
  simp [hz, Real.zero_rpow hz.ne']
case refine'_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) fun x => Real.exp (-(arg x.fst * x.snd.im))
case refine'_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) ((fun x => ‖x‖) ∘ fun x => Real.exp (-(arg x.fst * x.snd.im)))
simp only [Function.comp, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
case refine'_2.intro
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : Abs.abs z.im < C
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) fun x => Real.exp (-(arg x.fst * x.snd.im))
case refine'_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) fun x => Real.exp (-(arg x.fst * x.snd.im))
rcases exists_gt (|im z|) with ⟨C, hC⟩
case refine'_2.intro
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : Abs.abs z.im < C
⊢ ∀ᶠ (a : ℂ × ℂ) in 𝓝 (0, z), (fun x x_1 => x ≤ x_1) (Real.exp (-(arg a.fst * a.snd.im))) (Real.exp (π * C))
case refine'_2.intro
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : Abs.abs z.im < C
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝 (0, z)) fun x => Real.exp (-(arg x.fst * x.snd.im))
refine' ⟨Real.exp (π * C), eventually_map.2 _⟩
case refine'_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : Abs.abs z✝.im < C
z : ℂ × ℂ
hz : Abs.abs ((im ∘ Prod.snd) z) < C
⊢ Abs.abs (arg z.fst * z.snd.im) ≤ π * C
case refine'_2.intro
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : Abs.abs z.im < C
⊢ ∀ᶠ (a : ℂ × ℂ) in 𝓝 (0, z), (fun x x_1 => x ≤ x_1) (Real.exp (-(arg a.fst * a.snd.im))) (Real.exp (π * C))
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_self _).trans _
case refine'_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : Abs.abs z✝.im < C
z : ℂ × ℂ
hz : Abs.abs ((im ∘ Prod.snd) z) < C
⊢ Abs.abs (arg z.fst) * Abs.abs z.snd.im ≤ π * C
case refine'_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : Abs.abs z✝.im < C
z : ℂ × ℂ
hz : Abs.abs ((im ∘ Prod.snd) z) < C
⊢ Abs.abs (arg z.fst * z.snd.im) ≤ π * C
rw [_root_.abs_mul]
no goals
case refine'_2.intro
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : Abs.abs z✝.im < C
z : ℂ × ℂ
hz : Abs.abs ((im ∘ Prod.snd) z) < C
⊢ Abs.abs (arg z.fst) * Abs.abs z.snd.im ≤ π * C
exact
  mul_le_mul (abs_le.2 ⟨(neg_pi_lt_arg _).le, arg_le_pi _⟩) hz.le (_root_.abs_nonneg _)
    Real.pi_pos.le