Theorem: RuesNEqualsExpSum (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
z : ℂ
⊢ Rues n z = (∑ m ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑m / ↑↑n) * I))) / ↑↑n
Tactic:
rw [←RuesDiffM0EqualsRues, RuesDiffEqualsExpSum]
State after:
n : ℕ+
z : ℂ
⊢ (∑ k₀ ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k₀ / ↑↑n) * I)) / ↑↑n =
    (∑ m ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑m / ↑↑n) * I))) / ↑↑n

State before:
n : ℕ+
z : ℂ
⊢ (∑ k₀ ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k₀ / ↑↑n) * I)) / ↑↑n =
    (∑ m ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑m / ↑↑n) * I))) / ↑↑n
Tactic:
congr
State after:
case e_a.e_f
n : ℕ+
z : ℂ
⊢ (fun k₀ => cexp (z * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k₀ / ↑↑n) * I)) = fun m =>
    cexp (z * cexp (2 * ↑π * (↑m / ↑↑n) * I))

State before:
case e_a.e_f
n : ℕ+
z : ℂ
⊢ (fun k₀ => cexp (z * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k₀ / ↑↑n) * I)) = fun m =>
    cexp (z * cexp (2 * ↑π * (↑m / ↑↑n) * I))
Tactic:
ext1 k
State after:
case e_a.e_f.h
n : ℕ+
z : ℂ
k : ℕ
⊢ cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k / ↑↑n) * I) = cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I))

State before:
case e_a.e_f.h
n : ℕ+
z : ℂ
k : ℕ
⊢ cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k / ↑↑n) * I) = cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I))
Tactic:
simp only [Int.cast_zero, zero_mul, add_zero]
State after:
no goals