Theorem: RuesDiffEqualsExpSum (NazgandLean4/RootOfUnityExponentialSum.lean)

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]
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

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))
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

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₀]
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

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₀
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

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]
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

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))) _
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

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
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

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₁
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

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₂]
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

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₂
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

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]
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

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
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

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]
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

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₃
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

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
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

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
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

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
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

State before:
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
Tactic:
simp_rw [h₄]
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 (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n

State before:
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 (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Tactic:
clear h₄
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 (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n

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 (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Tactic:
have h₅ := RouGeometricSumEqIte n (↑k + m)
State after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n

State before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Tactic:
have h₆ : ∀ (x : ℕ), (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I) = (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) := by
  intros x
  simp only [Int.cast_add, Int.cast_natCast]
  ring_nf
State after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑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 (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n

State before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑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 (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Tactic:
simp_rw [h₆, h₅]
State after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (z ^ k / ↑k.factorial * if ↑↑n ∣ ↑k + m then ↑↑n else 0) / ↑↑n

State before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (z ^ k / ↑k.factorial * if ↑↑n ∣ ↑k + m then ↑↑n else 0) / ↑↑n
Tactic:
simp only [mul_ite, mul_zero]
State after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n

State before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n
Tactic:
have hem := Classical.em (↑↑n ∣ ↑k + m)
State after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hem : ↑↑n ∣ ↑k + m ∨ ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n

State before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hem : ↑↑n ∣ ↑k + m ∨ ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n
Tactic:
rcases hem with hemt | hemf
State after:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n

case e_f.h.inr
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemf : ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n

State before:
n : ℕ+
m : ℤ
z : ℂ
⊢ ∀ (k : ℕ),
    cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) =
      ∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial
Tactic:
intros k
State after:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
⊢ cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) = ∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial

State before:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
⊢ cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) = ∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial
Tactic:
exact ExpTsumForm (z * cexp (2 * ↑π * (↑k / ↑↑n) * I))
State after:
no goals

State before:
n : ℕ+
m : ℤ
z : ℂ
⊢ ∀ x ∈ range ↑n,
    Summable fun x_1 =>
      (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)
Tactic:
intros k _
State after:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
a✝ : k ∈ range ↑n
⊢ Summable fun x_1 => (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑k / ↑↑n) * I)

State before:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
a✝ : k ∈ range ↑n
⊢ Summable fun x_1 => (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑k / ↑↑n) * I)
Tactic:
exact Summable.smul_const (ExpTaylorSeriesSummable (z * cexp (2 * ↑π * (↑k / ↑↑n) * I))) _
State after:
no goals

State before:
n : ℕ+
m : ℤ
z : ℂ
⊢ ∀ (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))
Tactic:
intros b x
State after:
n : ℕ+
m : ℤ
z : ℂ
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))

State before:
n : ℕ+
m : ℤ
z : ℂ
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))
Tactic:
ring_nf
State after:
no goals

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

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

State before:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
⊢ ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
Tactic:
intros x
State after:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
x : ℕ
⊢ 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)

State before:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
x : ℕ
⊢ 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
Tactic:
simp only [Int.cast_add, Int.cast_natCast]
State after:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
x : ℕ
⊢ 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n * I)

State before:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
x : ℕ
⊢ 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n * I)
Tactic:
ring_nf
State after:
no goals

State before:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n
Tactic:
simp_rw [if_pos hemt]
State after:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ z ^ k / ↑k.factorial = z ^ k / ↑k.factorial * ↑↑n / ↑↑n

State before:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ z ^ k / ↑k.factorial = z ^ k / ↑k.factorial * ↑↑n / ↑↑n
Tactic:
ring_nf
State after:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ z ^ k * (↑k.factorial)⁻¹ = z ^ k * (↑k.factorial)⁻¹ * ↑↑n * (↑↑n)⁻¹

State before:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ z ^ k * (↑k.factorial)⁻¹ = z ^ k * (↑k.factorial)⁻¹ * ↑↑n * (↑↑n)⁻¹
Tactic:
simp only [ne_eq, Nat.cast_eq_zero, PNat.ne_zero, not_false_eq_true, mul_inv_cancel_right₀]
State after:
no goals

State before:
case e_f.h.inr
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemf : ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n
Tactic:
simp_rw [if_neg hemf]
State after:
case e_f.h.inr
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemf : ¬↑↑n ∣ ↑k + m
⊢ 0 = 0 / ↑↑n

State before:
case e_f.h.inr
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemf : ¬↑↑n ∣ ↑k + m
⊢ 0 = 0 / ↑↑n
Tactic:
simp only [zero_div]
State after:
no goals