Theorem: pow_mul_nat (Ray/Misc/Pow.lean)

State before:
z w : ℂ
n : ℕ
⊢ (z ^ w) ^ n = z ^ (w * ↑n)
Tactic:
by_cases z0 : z = 0
State after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
⊢ (z ^ w) ^ n = z ^ (w * ↑n)

case neg
z w : ℂ
n : ℕ
z0 : ¬z = 0
⊢ (z ^ w) ^ n = z ^ (w * ↑n)

State before:
case neg
z w : ℂ
n : ℕ
z0 : ¬z = 0
⊢ (z ^ w) ^ n = z ^ (w * ↑n)
Tactic:
simp only [Complex.cpow_def_of_ne_zero z0, ← Complex.exp_nat_mul]
State after:
case neg
z w : ℂ
n : ℕ
z0 : ¬z = 0
⊢ (↑n * (z.log * w)).exp = (z.log * (w * ↑n)).exp

State before:
case neg
z w : ℂ
n : ℕ
z0 : ¬z = 0
⊢ (↑n * (z.log * w)).exp = (z.log * (w * ↑n)).exp
Tactic:
ring_nf
State after:
no goals

State before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
⊢ (z ^ w) ^ n = z ^ (w * ↑n)
Tactic:
rw [z0]
State after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)

State before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
by_cases w0 : w = 0
State after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : w = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)

case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)

State before:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
by_cases n0 : n = 0
State after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : n = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)

case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)

State before:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
have wn0 : w * n ≠ 0 := mul_ne_zero w0 (Nat.cast_ne_zero.mpr n0)
State after:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)

State before:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
rw [Complex.zero_cpow w0]
State after:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ 0 ^ n = 0 ^ (w * ↑n)

State before:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ 0 ^ n = 0 ^ (w * ↑n)
Tactic:
rw [Complex.zero_cpow wn0]
State after:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ 0 ^ n = 0

State before:
case neg
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : ¬n = 0
wn0 : w * ↑n ≠ 0
⊢ 0 ^ n = 0
Tactic:
exact zero_pow n0
State after:
no goals

State before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : w = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
rw [w0]
State after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : w = 0
⊢ (0 ^ 0) ^ n = 0 ^ (0 * ↑n)

State before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : w = 0
⊢ (0 ^ 0) ^ n = 0 ^ (0 * ↑n)
Tactic:
simp
State after:
no goals

State before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : n = 0
⊢ (0 ^ w) ^ n = 0 ^ (w * ↑n)
Tactic:
rw [n0]
State after:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : n = 0
⊢ (0 ^ w) ^ 0 = 0 ^ (w * ↑0)

State before:
case pos
z w : ℂ
n : ℕ
z0 : z = 0
w0 : ¬w = 0
n0 : n = 0
⊢ (0 ^ w) ^ 0 = 0 ^ (w * ↑0)
Tactic:
simp
State after:
no goals