Theorem: RuesDiffM0EqualsRues (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
⊢ RuesDiff n 0 = Rues n
Tactic:
ext1 z
State after:
case h
n : ℕ+
z : ℂ
⊢ RuesDiff n 0 z = Rues n z

State before:
case h
n : ℕ+
z : ℂ
⊢ RuesDiff n 0 z = Rues n z
Tactic:
rw [Rues, RuesDiff]
State after:
case h
n : ℕ+
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + 0 then z ^ k / ↑k.factorial else 0) = ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial

State before:
case h
n : ℕ+
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + 0 then z ^ k / ↑k.factorial else 0) = ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
simp only [add_zero]
State after:
case h
n : ℕ+
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k then z ^ k / ↑k.factorial else 0) = ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial

State before:
case h
n : ℕ+
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k then z ^ k / ↑k.factorial else 0) = ∑' (k : ℕ), z ^ (↑n * k) / ↑(↑n * k).factorial
Tactic:
rw [NeedZeroCoeff (λ (k : ℕ) => z ^ k / (Nat.factorial k)) n]
State after:
no goals