[GOAL]
x : ℂ
⊢ x ^ 0 = 1
[PROOFSTEP]
simp [cpow_def]
[GOAL]
x y : ℂ
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp only [cpow_def]
[GOAL]
x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp [*, exp_ne_zero]
[GOAL]
case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp [*, exp_ne_zero]
[GOAL]
case neg
x y : ℂ
h✝ : ¬x = 0
⊢ exp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0
[PROOFSTEP]
simp [*, exp_ne_zero]
[GOAL]
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0
[PROOFSTEP]
simp [cpow_def, *]
[GOAL]
x a : ℂ
⊢ 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
x a : ℂ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
intro hyp
[GOAL]
case mp
x a : ℂ
hyp : 0 ^ x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
simp only [cpow_def, eq_self_iff_true, if_true] at hyp 
[GOAL]
case mp
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
by_cases x = 0
[GOAL]
case mp
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
by_cases x = 0
[GOAL]
case pos
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
subst h
[GOAL]
case pos
a : ℂ
hyp : (if 0 = 0 then 1 else 0) = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
[PROOFSTEP]
simp only [if_true, eq_self_iff_true] at hyp 
[GOAL]
case pos
a : ℂ
hyp : 1 = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
[PROOFSTEP]
right
[GOAL]
case pos.h
a : ℂ
hyp : 1 = a
⊢ 0 = 0 ∧ a = 1
[PROOFSTEP]
exact ⟨rfl, hyp.symm⟩
[GOAL]
case neg
x a : ℂ
hyp : (if x = 0 then 1 else 0) = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
rw [if_neg h] at hyp 
[GOAL]
case neg
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
left
[GOAL]
case neg.h
x a : ℂ
hyp : 0 = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0
[PROOFSTEP]
exact ⟨h, hyp.symm⟩
[GOAL]
case mpr
x a : ℂ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a
[PROOFSTEP]
rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case mpr.inl.intro
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0
[PROOFSTEP]
exact zero_cpow h
[GOAL]
case mpr.inr.intro
⊢ 0 ^ 0 = 1
[PROOFSTEP]
exact cpow_zero _
[GOAL]
x a : ℂ
⊢ a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
[PROOFSTEP]
rw [← zero_cpow_eq_iff, eq_comm]
[GOAL]
x : ℂ
hx : x = 0
⊢ x ^ 1 = x
[PROOFSTEP]
simp [hx, cpow_def]
[GOAL]
x : ℂ
hx : ¬x = 0
⊢ x ^ 1 = x
[PROOFSTEP]
rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]
[GOAL]
x : ℂ
⊢ 1 ^ x = 1
[PROOFSTEP]
rw [cpow_def]
[GOAL]
x : ℂ
⊢ (if 1 = 0 then if x = 0 then 1 else 0 else exp (log 1 * x)) = 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x : ℂ
h✝¹ : 1 = 0
h✝ : x = 0
⊢ 1 = 1
[PROOFSTEP]
simp_all [one_ne_zero]
[GOAL]
case neg
x : ℂ
h✝¹ : 1 = 0
h✝ : ¬x = 0
⊢ 0 = 1
[PROOFSTEP]
simp_all [one_ne_zero]
[GOAL]
case neg
x : ℂ
h✝ : ¬1 = 0
⊢ exp (log 1 * x) = 1
[PROOFSTEP]
simp_all [one_ne_zero]
[GOAL]
x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z
[PROOFSTEP]
simp only [cpow_def, ite_mul, boole_mul, mul_ite, mul_boole]
[GOAL]
x y z : ℂ
hx : x ≠ 0
⊢ (if x = 0 then if y + z = 0 then 1 else 0 else exp (log x * (y + z))) =
    if x = 0 then
      if z = 0 then if x = 0 then if y = 0 then 1 * 1 else 0 * 1 else exp (log x * y) * 1
      else if x = 0 then if y = 0 then 1 * 0 else 0 * 0 else exp (log x * y) * 0
    else if x = 0 then if y = 0 then 1 * exp (log x * z) else 0 * exp (log x * z) else exp (log x * y) * exp (log x * z)
[PROOFSTEP]
simp_all [exp_add, mul_add]
[GOAL]
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ x ^ (y * z) = (x ^ y) ^ z
[PROOFSTEP]
simp only [cpow_def]
[GOAL]
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else exp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)) = 0 then if z = 0 then 1 else 0
    else exp (log (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)) * z)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : z = 0
⊢ 1 = 1
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : ¬z = 0
⊢ 1 = 0
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : y * z = 0
h✝¹ : y = 0
h✝ : ¬1 = 0
⊢ 1 = exp (log 1 * z)
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : z = 0
⊢ 1 = 1
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : ¬z = 0
⊢ 1 = 0
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : y * z = 0
h✝¹ : ¬y = 0
h✝ : ¬0 = 0
⊢ 1 = exp (log 0 * z)
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : z = 0
⊢ 0 = 1
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : y = 0
h✝¹ : 1 = 0
h✝ : ¬z = 0
⊢ 0 = 0
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : ¬y * z = 0
h✝¹ : y = 0
h✝ : ¬1 = 0
⊢ 0 = exp (log 1 * z)
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : z = 0
⊢ 0 = 1
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝⁴ : x = 0
h✝³ : ¬y * z = 0
h✝² : ¬y = 0
h✝¹ : 0 = 0
h✝ : ¬z = 0
⊢ 0 = 0
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝³ : x = 0
h✝² : ¬y * z = 0
h✝¹ : ¬y = 0
h✝ : ¬0 = 0
⊢ 0 = exp (log 0 * z)
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case pos
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝² : ¬x = 0
h✝¹ : exp (log x * y) = 0
h✝ : z = 0
⊢ exp (log x * (y * z)) = 1
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝² : ¬x = 0
h✝¹ : exp (log x * y) = 0
h✝ : ¬z = 0
⊢ exp (log x * (y * z)) = 0
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
case neg
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h✝¹ : ¬x = 0
h✝ : ¬exp (log x * y) = 0
⊢ exp (log x * (y * z)) = exp (log (exp (log x * y)) * z)
[PROOFSTEP]
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]
[GOAL]
x y : ℂ
⊢ x ^ (-y) = (x ^ y)⁻¹
[PROOFSTEP]
simp only [cpow_def, neg_eq_zero, mul_neg]
[GOAL]
x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else exp (-(log x * y))) =
    (if x = 0 then if y = 0 then 1 else 0 else exp (log x * y))⁻¹
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 1⁻¹
[PROOFSTEP]
simp [exp_neg]
[GOAL]
case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0⁻¹
[PROOFSTEP]
simp [exp_neg]
[GOAL]
case neg
x y : ℂ
h✝ : ¬x = 0
⊢ exp (-(log x * y)) = (exp (log x * y))⁻¹
[PROOFSTEP]
simp [exp_neg]
[GOAL]
x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y - z) = x ^ y / x ^ z
[PROOFSTEP]
rw [sub_eq_add_neg, cpow_add _ _ hx, cpow_neg, div_eq_mul_inv]
[GOAL]
x : ℂ
⊢ x ^ (-1) = x⁻¹
[PROOFSTEP]
simpa using cpow_neg x 1
[GOAL]
x : ℂ
⊢ x ^ ↑0 = x ^ 0
[PROOFSTEP]
simp
[GOAL]
x : ℂ
n : ℕ
hx : x = 0
⊢ x ^ ↑(n + 1) = x ^ (n + 1)
[PROOFSTEP]
simp only [hx, pow_succ, Complex.zero_cpow (Nat.cast_ne_zero.2 (Nat.succ_ne_zero _)), zero_mul]
[GOAL]
x : ℂ
n : ℕ
hx : ¬x = 0
⊢ x ^ ↑(n + 1) = x ^ (n + 1)
[PROOFSTEP]
simp [cpow_add, hx, pow_add, cpow_nat_cast x n]
[GOAL]
x : ℂ
⊢ x ^ 2 = x ^ 2
[PROOFSTEP]
rw [← cpow_nat_cast]
[GOAL]
x : ℂ
⊢ x ^ 2 = x ^ ↑2
[PROOFSTEP]
simp only [Nat.cast_ofNat]
[GOAL]
x : ℂ
n : ℕ
⊢ x ^ ↑↑n = x ^ ↑n
[PROOFSTEP]
simp
[GOAL]
x : ℂ
n : ℕ
⊢ x ^ ↑-[n+1] = x ^ -[n+1]
[PROOFSTEP]
rw [zpow_negSucc]
[GOAL]
x : ℂ
n : ℕ
⊢ x ^ ↑-[n+1] = (x ^ (n + 1))⁻¹
[PROOFSTEP]
simp only [Int.negSucc_coe, Int.cast_neg, Complex.cpow_neg, inv_eq_one_div, Int.cast_ofNat, cpow_nat_cast]
[GOAL]
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x
[PROOFSTEP]
suffices im (log x * (n⁻¹ : ℂ)) ∈ Ioc (-π) π
  by
  rw [← cpow_nat_cast, ← cpow_mul _ this.1 this.2, inv_mul_cancel, cpow_one]
  exact_mod_cast hn
[GOAL]
x : ℂ
n : ℕ
hn : n ≠ 0
this : (log x * (↑n)⁻¹).im ∈ Set.Ioc (-π) π
⊢ (x ^ (↑n)⁻¹) ^ n = x
[PROOFSTEP]
rw [← cpow_nat_cast, ← cpow_mul _ this.1 this.2, inv_mul_cancel, cpow_one]
[GOAL]
x : ℂ
n : ℕ
hn : n ≠ 0
this : (log x * (↑n)⁻¹).im ∈ Set.Ioc (-π) π
⊢ ↑n ≠ 0
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (log x * (↑n)⁻¹).im ∈ Set.Ioc (-π) π
[PROOFSTEP]
rw [mul_comm, ← ofReal_nat_cast, ← ofReal_inv, ofReal_mul_im, ← div_eq_inv_mul]
[GOAL]
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
[PROOFSTEP]
rw [← pos_iff_ne_zero] at hn 
[GOAL]
x : ℂ
n : ℕ
hn : 0 < n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
[PROOFSTEP]
have hn' : 0 < (n : ℝ) := by assumption_mod_cast
[GOAL]
x : ℂ
n : ℕ
hn : 0 < n
⊢ 0 < ↑n
[PROOFSTEP]
assumption_mod_cast
[GOAL]
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
[PROOFSTEP]
have hn1 : 1 ≤ (n : ℝ) := by exact_mod_cast Nat.succ_le_iff.2 hn
[GOAL]
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ 1 ≤ ↑n
[PROOFSTEP]
exact_mod_cast Nat.succ_le_iff.2 hn
[GOAL]
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
[PROOFSTEP]
constructor
[GOAL]
case left
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ -π < (log x).im / ↑n
[PROOFSTEP]
rw [lt_div_iff hn']
[GOAL]
case left
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ -π * ↑n < (log x).im
[PROOFSTEP]
calc
  -π * n ≤ -π * 1 := mul_le_mul_of_nonpos_left hn1 (neg_nonpos.2 Real.pi_pos.le)
  _ = -π := (mul_one _)
  _ < im (log x) := neg_pi_lt_log_im _
[GOAL]
case right
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im / ↑n ≤ π
[PROOFSTEP]
rw [div_le_iff hn']
[GOAL]
case right
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im ≤ π * ↑n
[PROOFSTEP]
calc
  im (log x) ≤ π := log_im_le_pi _
  _ = π * 1 := (mul_one π).symm
  _ ≤ π * n := mul_le_mul_of_nonneg_left hn1 Real.pi_pos.le
[GOAL]
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
rcases eq_or_ne r 0 with (rfl | hr)
[GOAL]
case inl
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (↑a * ↑b) ^ 0 = ↑a ^ 0 * ↑b ^ 0
[PROOFSTEP]
simp only [cpow_zero, mul_one]
[GOAL]
case inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
rcases eq_or_lt_of_le ha with (rfl | ha')
[GOAL]
case inr.inl
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : 0 ≤ 0
⊢ (↑0 * ↑b) ^ r = ↑0 ^ r * ↑b ^ r
[PROOFSTEP]
rw [ofReal_zero, zero_mul, zero_cpow hr, zero_mul]
[GOAL]
case inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
rcases eq_or_lt_of_le hb with (rfl | hb')
[GOAL]
case inr.inr.inl
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : 0 ≤ 0
⊢ (↑a * ↑0) ^ r = ↑a ^ r * ↑0 ^ r
[PROOFSTEP]
rw [ofReal_zero, mul_zero, zero_cpow hr, mul_zero]
[GOAL]
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
have ha'' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha'.ne'
[GOAL]
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
have hb'' : (b : ℂ) ≠ 0 := ofReal_ne_zero.mpr hb'.ne'
[GOAL]
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
hb'' : ↑b ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
[PROOFSTEP]
rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha, add_mul, exp_add, ←
  cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']
[GOAL]
x n : ℂ
⊢ x⁻¹ ^ n = if arg x = π then ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹
[PROOFSTEP]
simp_rw [Complex.cpow_def, log_inv_eq_ite, inv_eq_zero, map_eq_zero, ite_mul, neg_mul, IsROrC.conj_inv, apply_ite conj,
  apply_ite exp, apply_ite Inv.inv, map_zero, map_one, exp_neg, inv_one, inv_zero, ← exp_conj, map_mul, conj_conj]
[GOAL]
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if arg x = π then (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹ else (exp (log x * n))⁻¹) =
    if arg x = π then if x = 0 then if n = 0 then 1 else 0 else (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (exp (log x * n))⁻¹
[PROOFSTEP]
split_ifs with hx hn ha ha
[GOAL]
case pos
x n : ℂ
hx : x = 0
hn : n = 0
ha : arg x = π
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hx : x = 0
hn : n = 0
ha : ¬arg x = π
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case pos
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : arg x = π
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : ¬arg x = π
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case pos
x n : ℂ
hx : ¬x = 0
h✝ : arg x = π
⊢ (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹ = (exp (↑(starRingEnd ℂ) (log x) * n))⁻¹
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hx : ¬x = 0
h✝ : ¬arg x = π
⊢ (exp (log x * n))⁻¹ = (exp (log x * n))⁻¹
[PROOFSTEP]
rfl
[GOAL]
x n : ℂ
hx : arg x ≠ π
⊢ x⁻¹ ^ n = (x ^ n)⁻¹
[PROOFSTEP]
rw [inv_cpow_eq_ite, if_neg hx]
[GOAL]
x n : ℂ
⊢ (x ^ n)⁻¹ = if arg x = π then ↑(starRingEnd ℂ) (x⁻¹ ^ ↑(starRingEnd ℂ) n) else x⁻¹ ^ n
[PROOFSTEP]
rw [inv_cpow_eq_ite, apply_ite conj, conj_conj, conj_conj]
[GOAL]
x n : ℂ
⊢ (x ^ n)⁻¹ =
    if arg x = π then if arg x = π then (x ^ n)⁻¹ else ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)⁻¹ else x⁻¹ ^ n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
x n : ℂ
h : arg x = π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
h : ¬arg x = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n
[PROOFSTEP]
rw [inv_cpow _ _ h]
[GOAL]
x n : ℂ
⊢ ↑(starRingEnd ℂ) x ^ n = if arg x = π then x ^ n else ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)
[PROOFSTEP]
simp_rw [cpow_def, map_eq_zero, apply_ite conj, map_one, map_zero, ← exp_conj, map_mul, conj_conj, log_conj_eq_ite]
[GOAL]
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else exp ((if arg x = π then log x else ↑(starRingEnd ℂ) (log x)) * n)) =
    if arg x = π then if x = 0 then if n = 0 then 1 else 0 else exp (log x * n)
    else if x = 0 then if n = 0 then 1 else 0 else exp (↑(starRingEnd ℂ) (log x) * n)
[PROOFSTEP]
split_ifs with hcx hn hx
[GOAL]
case pos
x n : ℂ
hcx : x = 0
hn : n = 0
hx : arg x = π
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hcx : x = 0
hn : n = 0
hx : ¬arg x = π
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case pos
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h✝ : arg x = π
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h✝ : ¬arg x = π
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case pos
x n : ℂ
hcx : ¬x = 0
h✝ : arg x = π
⊢ exp (log x * n) = exp (log x * n)
[PROOFSTEP]
rfl
[GOAL]
case neg
x n : ℂ
hcx : ¬x = 0
h✝ : ¬arg x = π
⊢ exp (↑(starRingEnd ℂ) (log x) * n) = exp (↑(starRingEnd ℂ) (log x) * n)
[PROOFSTEP]
rfl
[GOAL]
x n : ℂ
hx : arg x ≠ π
⊢ ↑(starRingEnd ℂ) x ^ n = ↑(starRingEnd ℂ) (x ^ ↑(starRingEnd ℂ) n)
[PROOFSTEP]
rw [conj_cpow_eq_ite, if_neg hx]
[GOAL]
x n : ℂ
hx : arg x ≠ π
⊢ x ^ ↑(starRingEnd ℂ) n = ↑(starRingEnd ((fun x => ℂ) x)) (↑(starRingEnd ℂ) x ^ n)
[PROOFSTEP]
rw [conj_cpow _ _ hx, conj_conj]
