Theorem: RouGeometricSumEqIte (NazgandLean4/RootOfUnityExponentialSum.lean)

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

State before:
n : ℕ+
k : ℤ
h₀ : ∀ (x : ℕ), 2 * ↑π * (↑k * ↑x / ↑↑n * I) = ↑x * (2 * ↑π * (↑k / ↑↑n * I))
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k * ↑x / ↑↑n * I)) = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
simp_rw [h₀, Complex.exp_nat_mul]
State after:
n : ℕ+
k : ℤ
h₀ : ∀ (x : ℕ), 2 * ↑π * (↑k * ↑x / ↑↑n * I) = ↑x * (2 * ↑π * (↑k / ↑↑n * I))
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0

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

State before:
n : ℕ+
k : ℤ
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
have hem := Classical.em (↑↑n ∣ k)
State after:
n : ℕ+
k : ℤ
hem : ↑↑n ∣ k ∨ ¬↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0

State before:
n : ℕ+
k : ℤ
hem : ↑↑n ∣ k ∨ ¬↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
have h₂ : (n : ℂ) ≠ 0 := by exact Ne.symm (NeZero.ne' (n : ℂ))
State after:
n : ℕ+
k : ℤ
hem : ↑↑n ∣ k ∨ ¬↑↑n ∣ k
h₂ : ↑↑n ≠ 0
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0

State before:
n : ℕ+
k : ℤ
hem : ↑↑n ∣ k ∨ ¬↑↑n ∣ k
h₂ : ↑↑n ≠ 0
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
rcases hem with hemt | hemf
State after:
case inl
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0

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

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

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

State before:
n : ℕ+
k : ℤ
hem : ↑↑n ∣ k ∨ ¬↑↑n ∣ k
⊢ ↑↑n ≠ 0
Tactic:
exact Ne.symm (NeZero.ne' (n : ℂ))
State after:
no goals

State before:
case inl
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
h₁ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = ∑ x ∈ range ↑n, 1
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
rw [h₁, if_pos hemt]
State after:
case inl
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
h₁ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = ∑ x ∈ range ↑n, 1
⊢ ∑ x ∈ range ↑n, 1 = ↑↑n

State before:
case inl
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
h₁ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = ∑ x ∈ range ↑n, 1
⊢ ∑ x ∈ range ↑n, 1 = ↑↑n
Tactic:
simp only [sum_const, card_range, nsmul_eq_mul, mul_one]
State after:
no goals

State before:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = ∑ x ∈ range ↑n, 1
Tactic:
congr
State after:
case e_f
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
⊢ (fun x => cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x) = fun x => 1

State before:
case e_f
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
⊢ (fun x => cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x) = fun x => 1
Tactic:
ext1 x
State after:
case e_f.h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
x : ℕ
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 1

State before:
case e_f.h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
x : ℕ
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 1
Tactic:
obtain ⟨k₂, kDiv⟩ := hemt
State after:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 1

State before:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 1
Tactic:
rw [kDiv]
State after:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑(↑↑n * k₂) / ↑↑n * I)) ^ x = 1

State before:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑(↑↑n * k₂) / ↑↑n * I)) ^ x = 1
Tactic:
field_simp
State after:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑k₂ * I)) ^ x = 1

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

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

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]
State after:
no goals

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
State after:
case h₃.a
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ ∃ n, 2 * ↑π * (↑k₂ * I) = ↑n * (2 * ↑π * I)

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₂
State after:
case h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ 2 * ↑π * (↑k₂ * I) = ↑k₂ * (2 * ↑π * I)

State before:
case h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ 2 * ↑π * (↑k₂ * I) = ↑k₂ * (2 * ↑π * I)
Tactic:
ring_nf
State after:
no goals

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]
State after:
case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 0

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

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

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

State before:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ≠ 1
Tactic:
by_contra h
State after:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h : cexp (2 * ↑π * (↑k / ↑↑n * I)) = 1
⊢ False

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
State after:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
h : ∃ n_1, 2 * ↑π * (↑k / ↑↑n * I) = ↑n_1 * (2 * ↑π * I)
⊢ False

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
State after:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : 2 * ↑π * (↑k / ↑↑n * I) = ↑m * (2 * ↑π * I)
⊢ False

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
State after:
case intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
m : ℤ
h : ↑k / ↑↑n * (2 * ↑π * I) = ↑m * (2 * ↑π * I)
⊢ False

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

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

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

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

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

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₅
State after:
no goals

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
State after:
no goals

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₃
State after:
no goals

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₄))
State after:
no goals

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

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]
State after:
no goals

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

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

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

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

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
State after:
no goals