Theorem: Complex.cpow_natCast_add_one_ne_zero (EulerProducts/LSeriesUnique.lean)

State before:
n : ℕ
z : ℂ
H : ↑n + 1 = 0 ∧ z ≠ 0
⊢ False
Tactic:
norm_cast at H
State after:
n : ℕ
z : ℂ
H : False ∧ ¬z = 0
⊢ False

State before:
n : ℕ
z : ℂ
H : False ∧ ¬z = 0
⊢ False
Tactic:
exact H.1
State after:
no goals