Theorem: RuesDiffRotationallySymmetric (NazgandLean4/RootOfUnityExponentialSum.lean)

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

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

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

State before:
case e_f.h
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    rou ^ (-m) * if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0
Tactic:
simp only [zpow_neg, mul_ite, mul_zero]
State after:
case e_f.h
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0

State before:
case e_f.h
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0
Tactic:
have h₀ := Classical.em (↑↑n ∣ ↑k + m)
State after:
case e_f.h
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : ↑↑n ∣ ↑k + m ∨ ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0

State before:
case e_f.h
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀ : ↑↑n ∣ ↑k + m ∨ ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0
Tactic:
rcases h₀ with h₀a | h₀b
State after:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0

case e_f.h.inr
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀b : ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0

State before:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0
Tactic:
simp_rw [if_pos h₀a]
State after:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ (z * rou) ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)

State before:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ (z * rou) ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Tactic:
rw [mul_pow z rou k]
State after:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ z ^ k * rou ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)

State before:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ z ^ k * rou ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Tactic:
have h₁ : rou ^ k = (rou ^ m)⁻¹ := by
  obtain ⟨k₂, kmDiv⟩ := h₀a
  have h₂ : rou ^ (↑k + m) = 1 := by
    rw [kmDiv, zpow_mul]
    simp only [zpow_natCast, h, one_zpow]
  have h₃ := congrArg (λ (z₀ : ℂ) => z₀ * (rou ^ m)⁻¹) h₂
  simp only [one_mul, ne_eq, inv_eq_zero] at h₃
  have h₄ := RouNot0 n rou h
  rw [zpow_add₀ h₄ ↑k m] at h₃
  rw [←h₃]
  have h₅ : rou ^ m ≠ 0 := by
    exact zpow_ne_zero m h₄
  field_simp
State after:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
h₁ : rou ^ k = (rou ^ m)⁻¹
⊢ z ^ k * rou ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)

State before:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
h₁ : rou ^ k = (rou ^ m)⁻¹
⊢ z ^ k * rou ^ k / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Tactic:
rw [h₁]
State after:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
h₁ : rou ^ k = (rou ^ m)⁻¹
⊢ z ^ k * (rou ^ m)⁻¹ / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)

State before:
case e_f.h.inl
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
h₁ : rou ^ k = (rou ^ m)⁻¹
⊢ z ^ k * (rou ^ m)⁻¹ / ↑k.factorial = (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial)
Tactic:
ring
State after:
no goals

State before:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀a : ↑↑n ∣ ↑k + m
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
obtain ⟨k₂, kmDiv⟩ := h₀a
State after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
⊢ rou ^ k = (rou ^ m)⁻¹

State before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
have h₂ : rou ^ (↑k + m) = 1 := by
  rw [kmDiv, zpow_mul]
  simp only [zpow_natCast, h, one_zpow]
State after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
⊢ rou ^ k = (rou ^ m)⁻¹

State before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
have h₃ := congrArg (λ (z₀ : ℂ) => z₀ * (rou ^ m)⁻¹) h₂
State after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : (fun z₀ => z₀ * (rou ^ m)⁻¹) (rou ^ (↑k + m)) = (fun z₀ => z₀ * (rou ^ m)⁻¹) 1
⊢ rou ^ k = (rou ^ m)⁻¹

State before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : (fun z₀ => z₀ * (rou ^ m)⁻¹) (rou ^ (↑k + m)) = (fun z₀ => z₀ * (rou ^ m)⁻¹) 1
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
simp only [one_mul, ne_eq, inv_eq_zero] at h₃
State after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ (↑k + m) * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
⊢ rou ^ k = (rou ^ m)⁻¹

State before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ (↑k + m) * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
have h₄ := RouNot0 n rou h
State after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ (↑k + m) * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = (rou ^ m)⁻¹

State before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ (↑k + m) * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
rw [zpow_add₀ h₄ ↑k m] at h₃
State after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = (rou ^ m)⁻¹

State before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = (rou ^ m)⁻¹
Tactic:
rw [←h₃]
State after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹

State before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ k = rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹
Tactic:
have h₅ : rou ^ m ≠ 0 := by
  exact zpow_ne_zero m h₄
State after:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
h₅ : rou ^ m ≠ 0
⊢ rou ^ k = rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹

State before:
case intro
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
h₅ : rou ^ m ≠ 0
⊢ rou ^ k = rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹
Tactic:
field_simp
State after:
no goals

State before:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
⊢ rou ^ (↑k + m) = 1
Tactic:
rw [kmDiv, zpow_mul]
State after:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
⊢ (rou ^ ↑↑n) ^ k₂ = 1

State before:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
⊢ (rou ^ ↑↑n) ^ k₂ = 1
Tactic:
simp only [zpow_natCast, h, one_zpow]
State after:
no goals

State before:
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
k₂ : ℤ
kmDiv : ↑k + m = ↑↑n * k₂
h₂ : rou ^ (↑k + m) = 1
h₃ : rou ^ ↑k * rou ^ m * (rou ^ m)⁻¹ = (rou ^ m)⁻¹
h₄ : rou ≠ 0
⊢ rou ^ m ≠ 0
Tactic:
exact zpow_ne_zero m h₄
State after:
no goals

State before:
case e_f.h.inr
n : ℕ+
m : ℤ
z rou : ℂ
h : rou ^ ↑n = 1
k : ℕ
h₀b : ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then (z * rou) ^ k / ↑k.factorial else 0) =
    if ↑↑n ∣ ↑k + m then (rou ^ m)⁻¹ * (z ^ k / ↑k.factorial) else 0
Tactic:
simp_rw [if_neg h₀b]
State after:
no goals