case inr
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ (↑x ^ ↑y).re = exp (log x * y) * cos (y * π)
x : ℝ
hx : x ≤ 0
y : ℝ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else exp (log x * y) * cos (y * π)
split_ifs with h <;> simp [rpow_def, *]
no goals
case inr
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ (↑x ^ ↑y).re = exp (log x * y) * cos (y * π)
exact rpow_def_of_neg (lt_of_le_of_ne hx h) _