Help with lemma

Stream: new members

[Mark Gerads]

I am working on this lemma and need some help.

import all

open complex finset
open_locale classical big_operators nat

lemma ruGeomSumEqIte (n k:ℕ) (h:n>0) (z:ℂ) :
    ∑ m in range n, (complex.exp (2 * real.pi * (k / n) * I)) ^ m = ite (n ∣ k) n 0 :=
begin
  have h: n ∣ k ∨ ¬n ∣ k,
  exact em (n ∣ k),
  cases h,
  {
    have h2 : ∑ (m : ℕ) in range n, exp (2 * ↑real.pi * (↑k / ↑n) * I) ^ m =
              ∑ (m : ℕ) in range n, 1,
    congr,
    ext1,
    sorry, -- need to replace k with a multiple of n to proceed
    rw h2,
    simp only [sum_const, card_range, nat.smul_one_eq_coe],
    sorry, -- need to evaluate ite with h_1
  },
  {
    rw geom_sum_eq,
    sorry,
    sorry,
  },
end

At the first sorry, the state is this, and I need to replace k with a multiple of n to proceed, but don't know how.
image.png
At the second sorry, I need to evaluate the ite and do not know how.
image.png