Theorem: RuesN1EqualsExp (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
⊢ Rues 1 = cexp
Tactic:
ext1 z
State after:
case h
z : ℂ
⊢ Rues 1 z = cexp z

State before:
case h
z : ℂ
⊢ Rues 1 z = cexp z
Tactic:
rw [Rues, ExpTsumForm]
State after:
case h
z : ℂ
⊢ ∑' (k : ℕ), z ^ (↑1 * k) / ↑(↑1 * k).factorial = ∑' (k : ℕ), z ^ k / ↑k.factorial

State before:
case h
z : ℂ
⊢ ∑' (k : ℕ), z ^ (↑1 * k) / ↑(↑1 * k).factorial = ∑' (k : ℕ), z ^ k / ↑k.factorial
Tactic:
simp only [PNat.one_coe, one_mul]
State after:
no goals