Theorem: RuesDiffArgumentSumRule (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ RuesDiff n m (z₀ + z₁) = ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
rw [RuesDiffEqualsExpSum]
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ k₀ ∈ range ↑n, cexp ((z₀ + z₁) * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑m * 2 * ↑π * (↑k₀ / ↑↑n) * I)) / ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ k₀ ∈ range ↑n, cexp ((z₀ + z₁) * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑m * 2 * ↑π * (↑k₀ / ↑↑n) * I)) / ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp_rw [Complex.exp_add, RightDistribClass.right_distrib, Complex.exp_add, ExpSumOfRuesDiff n (z₀ * _), ExpSumOfRuesDiff n (z₁ * _)]
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ((∑ k₀ ∈ range ↑n, RuesDiff n (↑k₀) (z₀ * cexp (2 * ↑π * (↑x / ↑↑n) * I))) *
            ∑ k₀ ∈ range ↑n, RuesDiff n (↑k₀) (z₁ * cexp (2 * ↑π * (↑x / ↑↑n) * I))) *
          cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ((∑ k₀ ∈ range ↑n, RuesDiff n (↑k₀) (z₀ * cexp (2 * ↑π * (↑x / ↑↑n) * I))) *
            ∑ k₀ ∈ range ↑n, RuesDiff n (↑k₀) (z₁ * cexp (2 * ↑π * (↑x / ↑↑n) * I))) *
          cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp_rw [RuesDiffRotationallySymmetric n _ _ _ (RouForm n _), Finset.sum_mul, Finset.mul_sum, Finset.sum_mul, ←Complex.exp_int_mul]
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          ∑ x_2 ∈ range ↑n,
            cexp (↑(-↑x_1) * (2 * ↑π * (↑x / ↑↑n) * I)) * RuesDiff n (↑x_1) z₀ *
                (cexp (↑(-↑x_2) * (2 * ↑π * (↑x / ↑↑n) * I)) * RuesDiff n (↑x_2) z₁) *
              cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          ∑ x_2 ∈ range ↑n,
            cexp (↑(-↑x_1) * (2 * ↑π * (↑x / ↑↑n) * I)) * RuesDiff n (↑x_1) z₀ *
                (cexp (↑(-↑x_2) * (2 * ↑π * (↑x / ↑↑n) * I)) * RuesDiff n (↑x_2) z₁) *
              cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
rw [Sum3Cycle]
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ b ∈ range ↑n,
        ∑ c ∈ range ↑n,
          ∑ a ∈ range ↑n,
            cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
                (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
              cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ b ∈ range ↑n,
        ∑ c ∈ range ↑n,
          ∑ a ∈ range ↑n,
            cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
                (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
              cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
have h₀ : ∀ (a b c : ℕ), cexp (↑(-(b : ℤ)) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ * (cexp (↑(-(c : ℤ)) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) * cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
    RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ * (cexp (↑(-(b : ℤ)) * (2 * ↑π * (↑a / ↑↑n) * I)) * (cexp (↑(-(c : ℤ)) * (2 * ↑π * (↑a / ↑↑n) * I))) * cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I)) := by
  intros a b c
  ring_nf
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₀ :
  ∀ (a b c : ℕ),
    cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
          (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
      RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
        (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
          cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
⊢ (∑ b ∈ range ↑n,
        ∑ c ∈ range ↑n,
          ∑ a ∈ range ↑n,
            cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
                (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
              cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₀ :
  ∀ (a b c : ℕ),
    cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
          (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
      RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
        (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
          cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
⊢ (∑ b ∈ range ↑n,
        ∑ c ∈ range ↑n,
          ∑ a ∈ range ↑n,
            cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
                (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
              cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp_rw [h₀, ←Complex.exp_add, ←Finset.mul_sum]
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₀ :
  ∀ (a b c : ℕ),
    cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
          (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
      RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
        (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
          cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ i ∈ range ↑n,
              cexp
                (↑(-↑x) * (2 * ↑π * (↑i / ↑↑n) * I) + ↑(-↑x_1) * (2 * ↑π * (↑i / ↑↑n) * I) +
                  ↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₀ :
  ∀ (a b c : ℕ),
    cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
          (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
      RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
        (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
          cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ i ∈ range ↑n,
              cexp
                (↑(-↑x) * (2 * ↑π * (↑i / ↑↑n) * I) + ↑(-↑x_1) * (2 * ↑π * (↑i / ↑↑n) * I) +
                  ↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
clear h₀
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ i ∈ range ↑n,
              cexp
                (↑(-↑x) * (2 * ↑π * (↑i / ↑↑n) * I) + ↑(-↑x_1) * (2 * ↑π * (↑i / ↑↑n) * I) +
                  ↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ i ∈ range ↑n,
              cexp
                (↑(-↑x) * (2 * ↑π * (↑i / ↑↑n) * I) + ↑(-↑x_1) * (2 * ↑π * (↑i / ↑↑n) * I) +
                  ↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp only [Int.cast_neg, Int.cast_natCast, neg_mul]
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n,
              cexp
                (-(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) +
                  ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n,
              cexp
                (-(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) +
                  ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
have h₁ : ∀ (x x_1 x_2 : ℕ), -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
    (2 * ↑π * (((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n) * I)) := by
  intros x x_1 x_2
  ring_nf
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₁ :
  ∀ (x x_1 x_2 : ℕ),
    -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
      2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n,
              cexp
                (-(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) +
                  ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₁ :
  ∀ (x x_1 x_2 : ℕ),
    -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
      2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n,
              cexp
                (-(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) +
                  ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp_rw [h₁]
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₁ :
  ∀ (x x_1 x_2 : ℕ),
    -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
      2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₁ :
  ∀ (x x_1 x_2 : ℕ),
    -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
      2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
clear h₁
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
have h₂ : ∀ (x x_1 : ℕ), (m : ℂ) - (x : ℂ) - (x_1 : ℂ) = @Int.cast ℂ Ring.toIntCast (m - (x : ℤ) - (x_1 : ℤ)) := by
  intros x x_1
  norm_cast
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₂ : ∀ (x x_1 : ℕ), ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₂ : ∀ (x x_1 : ℕ), ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp_rw [h₂, RouGeometricSumEqIte]
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₂ : ∀ (x x_1 : ℕ), ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n, RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ * if ↑↑n ∣ m - ↑x - ↑x_1 then ↑↑n else 0) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₂ : ∀ (x x_1 : ℕ), ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n, RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ * if ↑↑n ∣ m - ↑x - ↑x_1 then ↑↑n else 0) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
clear h₂
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n, RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ * if ↑↑n ∣ m - ↑x - ↑x_1 then ↑↑n else 0) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n, RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ * if ↑↑n ∣ m - ↑x - ↑x_1 then ↑↑n else 0) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp only [mul_ite, mul_zero, sum_range]
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ i : Fin ↑n,
        ∑ i_1 : Fin ↑n, if ↑↑n ∣ m - ↑↑i - ↑↑i_1 then RuesDiff n (↑↑i) z₀ * RuesDiff n (↑↑i_1) z₁ * ↑↑n else 0) /
      ↑↑n =
    ∑ i : Fin ↑n, RuesDiff n (↑↑i) z₀ * RuesDiff n (m - ↑↑i) z₁

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ i : Fin ↑n,
        ∑ i_1 : Fin ↑n, if ↑↑n ∣ m - ↑↑i - ↑↑i_1 then RuesDiff n (↑↑i) z₀ * RuesDiff n (↑↑i_1) z₁ * ↑↑n else 0) /
      ↑↑n =
    ∑ i : Fin ↑n, RuesDiff n (↑↑i) z₀ * RuesDiff n (m - ↑↑i) z₁
Tactic:
sorry
State after:
no goals

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ ∀ (a b c : ℕ),
    cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
          (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
      RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
        (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
          cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
Tactic:
intros a b c
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
a b c : ℕ
⊢ cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
        (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
      cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
    RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
      (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
a b c : ℕ
⊢ cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
        (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
      cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
    RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
      (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
Tactic:
ring_nf
State after:
no goals

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ ∀ (x x_1 x_2 : ℕ),
    -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
      2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
Tactic:
intros x x_1 x_2
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
x x_1 x_2 : ℕ
⊢ -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
    2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
x x_1 x_2 : ℕ
⊢ -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
    2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
Tactic:
ring_nf
State after:
no goals

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ ∀ (x x_1 : ℕ), ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
Tactic:
intros x x_1
State after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
x x_1 : ℕ
⊢ ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)

State before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
x x_1 : ℕ
⊢ ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
Tactic:
norm_cast
State after:
no goals