Theorem: RuesDiffMPeriodic (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
m k : ℤ
⊢ RuesDiff n m = RuesDiff n (m + k * ↑↑n)
Tactic:
ext1 z
State after:
case h
n : ℕ+
m k : ℤ
z : ℂ
⊢ RuesDiff n m z = RuesDiff n (m + k * ↑↑n) z

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

State before:
case h
n : ℕ+
m k : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (k_1 : ℕ), if ↑↑n ∣ ↑k_1 + (m + k * ↑↑n) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
congr
State after:
case h.e_f
n : ℕ+
m k : ℤ
z : ℂ
⊢ (fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = fun k_1 =>
    if ↑↑n ∣ ↑k_1 + (m + k * ↑↑n) then z ^ k_1 / ↑k_1.factorial else 0

State before:
case h.e_f
n : ℕ+
m k : ℤ
z : ℂ
⊢ (fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = fun k_1 =>
    if ↑↑n ∣ ↑k_1 + (m + k * ↑↑n) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
ext1 K
State after:
case h.e_f.h
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (if ↑↑n ∣ ↑K + m then z ^ K / ↑K.factorial else 0) = if ↑↑n ∣ ↑K + (m + k * ↑↑n) then z ^ K / ↑K.factorial else 0

State before:
case h.e_f.h
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (if ↑↑n ∣ ↑K + m then z ^ K / ↑K.factorial else 0) = if ↑↑n ∣ ↑K + (m + k * ↑↑n) then z ^ K / ↑K.factorial else 0
Tactic:
congr 1
State after:
case h.e_f.h.e_c
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (↑↑n ∣ ↑K + m) = (↑↑n ∣ ↑K + (m + k * ↑↑n))

State before:
case h.e_f.h.e_c
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (↑↑n ∣ ↑K + m) = (↑↑n ∣ ↑K + (m + k * ↑↑n))
Tactic:
rw [Dvd.dvd.addMultiple (↑↑n) (↑K + m) k]
State after:
case h.e_f.h.e_c
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (↑↑n ∣ ↑K + m + k * ↑↑n) = (↑↑n ∣ ↑K + (m + k * ↑↑n))

State before:
case h.e_f.h.e_c
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (↑↑n ∣ ↑K + m + k * ↑↑n) = (↑↑n ∣ ↑K + (m + k * ↑↑n))
Tactic:
ring_nf
State after:
no goals