Theorem: RouNot0 (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
rou : ℂ
h : rou ^ ↑n = 1
⊢ rou ≠ 0
Tactic:
by_contra h₁
State after:
n : ℕ+
rou : ℂ
h : rou ^ ↑n = 1
h₁ : rou = 0
⊢ False

State before:
n : ℕ+
rou : ℂ
h : rou ^ ↑n = 1
h₁ : rou = 0
⊢ False
Tactic:
rw [h₁] at h
State after:
n : ℕ+
rou : ℂ
h : 0 ^ ↑n = 1
h₁ : rou = 0
⊢ False

State before:
n : ℕ+
rou : ℂ
h : 0 ^ ↑n = 1
h₁ : rou = 0
⊢ False
Tactic:
simp only [ne_eq, PNat.ne_zero, not_false_eq_true, zero_pow, zero_ne_one] at h
State after:
no goals