case inr
w : ℂ
⊢ ↑abs (0 ^ w) ≤ 0 ^ w.re / Real.exp (arg 0 * w.im)
z w : ℂ
⊢ ↑abs (z ^ w) ≤ ↑abs z ^ w.re / Real.exp (arg z * w.im)
rcases ne_or_eq z 0 with (hz | rfl) <;> [exact (abs_cpow_of_ne_zero hz w).le; rw [map_zero]]
case inr.inl

⊢ ↑abs (0 ^ 0) ≤ 0 ^ 0.re / Real.exp (arg 0 * 0.im)

case inr.inr
w : ℂ
hw : w ≠ 0
⊢ ↑abs (0 ^ w) ≤ 0 ^ w.re / Real.exp (arg 0 * w.im)
case inr
w : ℂ
⊢ ↑abs (0 ^ w) ≤ 0 ^ w.re / Real.exp (arg 0 * w.im)
rcases eq_or_ne w 0 with (rfl | hw)
case inr.inr
w : ℂ
hw : w ≠ 0
⊢ 0 ≤ 0 ^ w.re / Real.exp (arg 0 * w.im)
case inr.inr
w : ℂ
hw : w ≠ 0
⊢ ↑abs (0 ^ w) ≤ 0 ^ w.re / Real.exp (arg 0 * w.im)
rw [zero_cpow hw, map_zero]
no goals
case inr.inr
w : ℂ
hw : w ≠ 0
⊢ 0 ≤ 0 ^ w.re / Real.exp (arg 0 * w.im)
exact div_nonneg (Real.rpow_nonneg_of_nonneg le_rfl _) (Real.exp_pos _).le
no goals
case inr.inl

⊢ ↑abs (0 ^ 0) ≤ 0 ^ 0.re / Real.exp (arg 0 * 0.im)
simp