Theorem: RuesArgumentSumRule (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
z₀ z₁ : ℂ
⊢ Rues n (z₀ + z₁) = ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁
Tactic:
rw [←RuesDiffM0EqualsRues, RuesDiffArgumentSumRule]
State after:
n : ℕ+
z₀ z₁ : ℂ
⊢ ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁ =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁

State before:
n : ℕ+
z₀ z₁ : ℂ
⊢ ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁ =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁
Tactic:
congr
State after:
case e_f
n : ℕ+
z₀ z₁ : ℂ
⊢ (fun k => RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁) = fun k => RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁

State before:
case e_f
n : ℕ+
z₀ z₁ : ℂ
⊢ (fun k => RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁) = fun k => RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁
Tactic:
ext k
State after:
case e_f.h
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁ = RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁

State before:
case e_f.h
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (↑k) z₀ * RuesDiff n (0 - ↑k) z₁ = RuesDiff n (↑k) z₀ * RuesDiff n (↑↑n - ↑k) z₁
Tactic:
congr 1
State after:
case e_f.h.e_a
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (0 - ↑k) z₁ = RuesDiff n (↑↑n - ↑k) z₁

State before:
case e_f.h.e_a
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (0 - ↑k) z₁ = RuesDiff n (↑↑n - ↑k) z₁
Tactic:
rw [RuesDiffMPeriodic n (0 - ↑k) 1]
State after:
case e_f.h.e_a
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (0 - ↑k + 1 * ↑↑n) z₁ = RuesDiff n (↑↑n - ↑k) z₁

State before:
case e_f.h.e_a
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ RuesDiff n (0 - ↑k + 1 * ↑↑n) z₁ = RuesDiff n (↑↑n - ↑k) z₁
Tactic:
congr 1
State after:
case e_f.h.e_a.e_m
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ 0 - ↑k + 1 * ↑↑n = ↑↑n - ↑k

State before:
case e_f.h.e_a.e_m
n : ℕ+
z₀ z₁ : ℂ
k : ℕ
⊢ 0 - ↑k + 1 * ↑↑n = ↑↑n - ↑k
Tactic:
ring_nf
State after:
no goals