Theorem: ExpSumOfRuesDiff (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
k : ℕ+
z : ℂ
⊢ cexp z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z
Tactic:
rw [←RuesN1EqualsExp, ←RuesDiffM0EqualsRues]
State after:
k : ℕ+
z : ℂ
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z

State before:
k : ℕ+
z : ℂ
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z
Tactic:
have h₀ := RuesDiffSumOfRuesDiff 1 k 0 z
State after:
k : ℕ+
z : ℂ
h₀ : RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff (1 * k) (↑↑1 * ↑k₀ + 0) z
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z

State before:
k : ℕ+
z : ℂ
h₀ : RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff (1 * k) (↑↑1 * ↑k₀ + 0) z
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z
Tactic:
simp only [one_mul, PNat.val_ofNat, Nat.cast_one, add_zero] at h₀
State after:
k : ℕ+
z : ℂ
h₀ : RuesDiff 1 0 z = ∑ x ∈ range ↑k, RuesDiff k (↑x) z
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z

State before:
k : ℕ+
z : ℂ
h₀ : RuesDiff 1 0 z = ∑ x ∈ range ↑k, RuesDiff k (↑x) z
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z
Tactic:
assumption
State after:
no goals