internlm/Lean-Github huggingface dataset:
Theorem: RouGeometricSumEqIte
Proof state before:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑k₂ * I)) ^ x = 1
Tactic:
suffices h₃ : cexp (2 * ↑π * (↑k₂ * I)) = 1
Proof state after:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
h₃ : cexp (2 * ↑π * (↑k₂ * I)) = 1
⊢ cexp (2 * ↑π * (↑k₂ * I)) ^ x = 1

case h₃
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑k₂ * I)) = 1
Theorem: RouGeometricSumEqIte
Proof state before:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
h₃ : cexp (2 * ↑π * (↑k₂ * I)) = 1
⊢ cexp (2 * ↑π * (↑k₂ * I)) ^ x = 1
Tactic:
rw [h₃]
Proof state after:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
h₃ : cexp (2 * ↑π * (↑k₂ * I)) = 1
⊢ 1 ^ x = 1
Theorem: RouGeometricSumEqIte
Proof state before:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
h₃ : cexp (2 * ↑π * (↑k₂ * I)) = 1
⊢ 1 ^ x = 1
Tactic:
simp only [one_pow]
Proof state after:
no goals
Theorem: RouGeometricSumEqIte
Proof state before:
case h₃
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑k₂ * I)) = 1
Tactic:
refine Complex.exp_eq_one_iff.mpr ?h₃.a
Proof state after:
case h₃.a
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ ∃ n, 2 * ↑π * (↑k₂ * I) = ↑n * (2 * ↑π * I)
Theorem: RouGeometricSumEqIte
Proof state before:
case h₃.a
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ ∃ n, 2 * ↑π * (↑k₂ * I) = ↑n * (2 * ↑π * I)
Tactic:
use k₂
Proof state after:
case h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ 2 * ↑π * (↑k₂ * I) = ↑k₂ * (2 * ↑π * I)
Theorem: RouGeometricSumEqIte
Proof state before:
case h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ 2 * ↑π * (↑k₂ * I) = ↑k₂ * (2 * ↑π * I)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RouGeometricSumEqIte
Proof state before:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
rw [if_neg hemf]
Proof state after:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 0
Theorem: RouGeometricSumEqIte
Proof state before:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 0
Tactic:
have h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1 := by
  by_contra h
  rw [Complex.exp_eq_one_iff] at h
  obtain ⟨m, h⟩ := h
  rw [(show 2 * ↑π * (↑k / ↑↑n * I) = (↑k / ↑↑n) * (2 * ↑π * I) by ring)] at h
  have h₃ := mul_right_cancel₀ Complex.two_pi_I_ne_zero h
  field_simp at h₃
  have h₄ : k = m * n := by
    exact mod_cast h₃
  have h₅ : (n : ℤ) ∣ k := by
    exact Dvd.intro_left m (id (Eq.symm h₄))
  apply hemf
  exact h₅
Proof state after:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 0
Theorem: RouGeometricSumEqIte
Proof state before:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 0
Tactic:
rw [geom_sum_eq h₀]
Proof state after:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ (cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ ↑n - 1) / (cexp (2 * ↑π * (↑k / ↑↑n * I)) - 1) = 0
Theorem: RouGeometricSumEqIte
Proof state before:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ (cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ ↑n - 1) / (cexp (2 * ↑π * (↑k / ↑↑n * I)) - 1) = 0
Tactic:
suffices h₁ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ (n : ℕ) = 1
Proof state after:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
h₁ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ ↑n = 1
⊢ (cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ ↑n - 1) / (cexp (2 * ↑π * (↑k / ↑↑n * I)) - 1) = 0

case h₁
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ ↑n = 1
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
Tactic:
by_contra h
Proof state after:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h : cexp (2 * ↑π * (↑k / ↑↑n * I)) = 1
⊢ False
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h : cexp (2 * ↑π * (↑k / ↑↑n * I)) = 1
⊢ False
Tactic:
rw [Complex.exp_eq_one_iff] at h
Proof state after:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h : ∃ n_1, 2 * ↑π * (↑k / ↑↑n * I) = ↑n_1 * (2 * ↑π * I)
⊢ False
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h : ∃ n_1, 2 * ↑π * (↑k / ↑↑n * I) = ↑n_1 * (2 * ↑π * I)
⊢ False
Tactic:
obtain ⟨m, h⟩ := h
Proof state after:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : 2 * ↑π * (↑k / ↑↑n * I) = ↑m * (2 * ↑π * I)
⊢ False
Theorem: RouGeometricSumEqIte
Proof state before:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : 2 * ↑π * (↑k / ↑↑n * I) = ↑m * (2 * ↑π * I)
⊢ False
Tactic:
rw [(show 2 * ↑π * (↑k / ↑↑n * I) = (↑k / ↑↑n) * (2 * ↑π * I) by ring)] at h
Proof state after:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
⊢ False
Theorem: RouGeometricSumEqIte
Proof state before:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
⊢ False
Tactic:
have h₃ := mul_right_cancel₀ Complex.two_pi_I_ne_zero h
Proof state after:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k / ↑↑n = ↑m
⊢ False
Theorem: RouGeometricSumEqIte
Proof state before:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k / ↑↑n = ↑m
⊢ False
Tactic:
field_simp at h₃
Proof state after:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k = ↑m * ↑↑n
⊢ False
Theorem: RouGeometricSumEqIte
Proof state before:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k = ↑m * ↑↑n
⊢ False
Tactic:
have h₄ : k = m * n := by
  exact mod_cast h₃
Proof state after:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k = ↑m * ↑↑n
h₄ : k = m * ↑↑n
⊢ False
Theorem: RouGeometricSumEqIte
Proof state before:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k = ↑m * ↑↑n
h₄ : k = m * ↑↑n
⊢ False
Tactic:
have h₅ : (n : ℤ) ∣ k := by
  exact Dvd.intro_left m (id (Eq.symm h₄))
Proof state after:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k = ↑m * ↑↑n
h₄ : k = m * ↑↑n
h₅ : ↑↑n ∣ k
⊢ False
Theorem: RouGeometricSumEqIte
Proof state before:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k = ↑m * ↑↑n
h₄ : k = m * ↑↑n
h₅ : ↑↑n ∣ k
⊢ False
Tactic:
apply hemf
Proof state after:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k = ↑m * ↑↑n
h₄ : k = m * ↑↑n
h₅ : ↑↑n ∣ k
⊢ ↑↑n ∣ k
Theorem: RouGeometricSumEqIte
Proof state before:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k = ↑m * ↑↑n
h₄ : k = m * ↑↑n
h₅ : ↑↑n ∣ k
⊢ ↑↑n ∣ k
Tactic:
exact h₅
Proof state after:
no goals
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : 2 * ↑π * (↑k / ↑↑n * I) = ↑m * (2 * ↑π * I)
⊢ 2 * ↑π * (↑k / ↑↑n * I) = ↑k / ↑↑n * (2 * ↑π * I)
Tactic:
ring
Proof state after:
no goals
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k = ↑m * ↑↑n
⊢ k = m * ↑↑n
Tactic:
exact mod_cast h₃
Proof state after:
no goals
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
h₃ : ↑k = ↑m * ↑↑n
h₄ : k = m * ↑↑n
⊢ ↑↑n ∣ k
Tactic:
exact Dvd.intro_left m (id (Eq.symm h₄))
Proof state after:
no goals
Theorem: RouGeometricSumEqIte
Proof state before:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
h₁ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ ↑n = 1
⊢ (cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ ↑n - 1) / (cexp (2 * ↑π * (↑k / ↑↑n * I)) - 1) = 0
Tactic:
rw [h₁]
Proof state after:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
h₁ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ ↑n = 1
⊢ (1 - 1) / (cexp (2 * ↑π * (↑k / ↑↑n * I)) - 1) = 0
Theorem: RouGeometricSumEqIte
Proof state before:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
h₁ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ ↑n = 1
⊢ (1 - 1) / (cexp (2 * ↑π * (↑k / ↑↑n * I)) - 1) = 0
Tactic:
simp only [sub_self, zero_div]
Proof state after:
no goals
Theorem: RouGeometricSumEqIte
Proof state before:
case h₁
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ ↑n = 1
Tactic:
rw [(Complex.exp_nat_mul _ n).symm]
Proof state after:
case h₁
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ cexp (↑↑n * (2 * ↑π * (↑k / ↑↑n * I))) = 1
Theorem: RouGeometricSumEqIte
Proof state before:
case h₁
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ cexp (↑↑n * (2 * ↑π * (↑k / ↑↑n * I))) = 1
Tactic:
refine Complex.exp_eq_one_iff.mpr ?h₁.a
Proof state after:
case h₁.a
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ ∃ n_1, ↑↑n * (2 * ↑π * (↑k / ↑↑n * I)) = ↑n_1 * (2 * ↑π * I)
Theorem: RouGeometricSumEqIte
Proof state before:
case h₁.a
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ ∃ n_1, ↑↑n * (2 * ↑π * (↑k / ↑↑n * I)) = ↑n_1 * (2 * ↑π * I)
Tactic:
use k
Proof state after:
case h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ ↑↑n * (2 * ↑π * (↑k / ↑↑n * I)) = ↑k * (2 * ↑π * I)
Theorem: RouGeometricSumEqIte
Proof state before:
case h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ ↑↑n * (2 * ↑π * (↑k / ↑↑n * I)) = ↑k * (2 * ↑π * I)
Tactic:
field_simp
Proof state after:
case h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ 2 * ↑π * (↑k * I) = ↑k * (2 * ↑π * I)
Theorem: RouGeometricSumEqIte
Proof state before:
case h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h₀ : cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
⊢ 2 * ↑π * (↑k * I) = ↑k * (2 * ↑π * I)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z = (∑ k₀ ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑m * 2 * ↑π * (↑k₀ / ↑↑n) * I)) / ↑↑n
Tactic:
simp_rw [Complex.exp_add]
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) / ↑↑n
Tactic:
have h₀ : ∀ (k : ℕ), cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) = ∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ k_1 / ↑(Nat.factorial k_1) := by
  intros k
  exact ExpTsumForm (z * cexp (2 * ↑π * (↑k / ↑↑n) * I))
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
h₀ :
  ∀ (k : ℕ),
    cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) =
      ∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
h₀ :
  ∀ (k : ℕ),
    cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) =
      ∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) / ↑↑n
Tactic:
simp_rw [h₀]
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
h₀ :
  ∀ (k : ℕ),
    cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) =
      ∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        (∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial) *
          cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
h₀ :
  ∀ (k : ℕ),
    cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) =
      ∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        (∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial) *
          cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Tactic:
clear h₀
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        (∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial) *
          cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        (∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial) *
          cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Tactic:
simp_rw [←tsum_mul_right]
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        ∑' (x_1 : ℕ),
          (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        ∑' (x_1 : ℕ),
          (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Tactic:
have h₁ : ∀ x ∈ range ↑n, Summable (λ (x_1 : ℕ) => (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑(Nat.factorial x_1) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) := by
  intros k _
  exact Summable.smul_const (ExpTaylorSeriesSummable (z * cexp (2 * ↑π * (↑k / ↑↑n) * I))) _
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
h₁ :
  ∀ x ∈ range ↑n,
    Summable fun x_1 =>
      (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        ∑' (x_1 : ℕ),
          (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
h₁ :
  ∀ x ∈ range ↑n,
    Summable fun x_1 =>
      (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        ∑' (x_1 : ℕ),
          (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Tactic:
have h₂ := (tsum_sum h₁).symm
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
h₁ :
  ∀ x ∈ range ↑n,
    Summable fun x_1 =>
      (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)
h₂ :
  ∑ i ∈ range ↑n,
      ∑' (b : ℕ), (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I) =
    ∑' (b : ℕ),
      ∑ i ∈ range ↑n, (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I)
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        ∑' (x_1 : ℕ),
          (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
h₁ :
  ∀ x ∈ range ↑n,
    Summable fun x_1 =>
      (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)
h₂ :
  ∑ i ∈ range ↑n,
      ∑' (b : ℕ), (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I) =
    ∑' (b : ℕ),
      ∑ i ∈ range ↑n, (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I)
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        ∑' (x_1 : ℕ),
          (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Tactic:
clear h₁
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
h₂ :
  ∑ i ∈ range ↑n,
      ∑' (b : ℕ), (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I) =
    ∑' (b : ℕ),
      ∑ i ∈ range ↑n, (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I)
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        ∑' (x_1 : ℕ),
          (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
h₂ :
  ∑ i ∈ range ↑n,
      ∑' (b : ℕ), (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I) =
    ∑' (b : ℕ),
      ∑ i ∈ range ↑n, (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I)
⊢ RuesDiff n m z =
    (∑ x ∈ range ↑n,
        ∑' (x_1 : ℕ),
          (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Tactic:
simp_rw [h₂]
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
h₂ :
  ∑ i ∈ range ↑n,
      ∑' (b : ℕ), (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I) =
    ∑' (b : ℕ),
      ∑ i ∈ range ↑n, (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I)
⊢ RuesDiff n m z =
    (∑' (b : ℕ),
        ∑ i ∈ range ↑n, (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
h₂ :
  ∑ i ∈ range ↑n,
      ∑' (b : ℕ), (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I) =
    ∑' (b : ℕ),
      ∑ i ∈ range ↑n, (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I)
⊢ RuesDiff n m z =
    (∑' (b : ℕ),
        ∑ i ∈ range ↑n, (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n
Tactic:
clear h₂
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z =
    (∑' (b : ℕ),
        ∑ i ∈ range ↑n, (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z =
    (∑' (b : ℕ),
        ∑ i ∈ range ↑n, (z * cexp (2 * ↑π * (↑i / ↑↑n) * I)) ^ b / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n
Tactic:
simp_rw [mul_pow, ←Complex.exp_nat_mul]
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z =
    (∑' (b : ℕ),
        ∑ x ∈ range ↑n,
          z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z =
    (∑' (b : ℕ),
        ∑ x ∈ range ↑n,
          z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Tactic:
have h₃ : ∀ (b x : ℕ), z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑(Nat.factorial b) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I) =
          (z ^ b / ↑(Nat.factorial b)) * (cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) := by
  intros b x
  ring_nf
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
h₃ :
  ∀ (b x : ℕ),
    z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I) =
      z ^ b / ↑b.factorial * (cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I))
⊢ RuesDiff n m z =
    (∑' (b : ℕ),
        ∑ x ∈ range ↑n,
          z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
h₃ :
  ∀ (b x : ℕ),
    z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I) =
      z ^ b / ↑b.factorial * (cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I))
⊢ RuesDiff n m z =
    (∑' (b : ℕ),
        ∑ x ∈ range ↑n,
          z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n
Tactic:
simp_rw [h₃, ←Finset.mul_sum, ←Complex.exp_add, ←tsum_div_const, RuesDiff]
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
h₃ :
  ∀ (b x : ℕ),
    z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I) =
      z ^ b / ↑b.factorial * (cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I))
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (x : ℕ),
      (z ^ x / ↑x.factorial *
          ∑ x_1 ∈ range ↑n, cexp (↑x * (2 * ↑π * (↑x_1 / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x_1 / ↑↑n) * I)) /
        ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
h₃ :
  ∀ (b x : ℕ),
    z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I) =
      z ^ b / ↑b.factorial * (cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I))
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (x : ℕ),
      (z ^ x / ↑x.factorial *
          ∑ x_1 ∈ range ↑n, cexp (↑x * (2 * ↑π * (↑x_1 / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x_1 / ↑↑n) * I)) /
        ↑↑n
Tactic:
clear h₃
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (x : ℕ),
      (z ^ x / ↑x.factorial *
          ∑ x_1 ∈ range ↑n, cexp (↑x * (2 * ↑π * (↑x_1 / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x_1 / ↑↑n) * I)) /
        ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (x : ℕ),
      (z ^ x / ↑x.factorial *
          ∑ x_1 ∈ range ↑n, cexp (↑x * (2 * ↑π * (↑x_1 / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x_1 / ↑↑n) * I)) /
        ↑↑n
Tactic:
congr
Proof state after:
case e_f
n : ℕ+
m : ℤ
z : ℂ
⊢ (fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = fun x =>
    (z ^ x / ↑x.factorial *
        ∑ x_1 ∈ range ↑n, cexp (↑x * (2 * ↑π * (↑x_1 / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x_1 / ↑↑n) * I)) /
      ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f
n : ℕ+
m : ℤ
z : ℂ
⊢ (fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = fun x =>
    (z ^ x / ↑x.factorial *
        ∑ x_1 ∈ range ↑n, cexp (↑x * (2 * ↑π * (↑x_1 / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x_1 / ↑↑n) * I)) /
      ↑↑n
Tactic:
ext1 k
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I)) / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I)) / ↑↑n
Tactic:
have h₄ : ∀ (x : ℕ), ↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I = (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I) := by
  intros x
  ring_nf
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₄ : ∀ (x : ℕ), ↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I = 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I)) / ↑↑n