-- Mathlib/RingTheory/RootsOfUnity/Complex.lean
theorem mem_rootsOfUnity (n : ℕ) [NeZero n] (x : Units ℂ) :
    x ∈ rootsOfUnity n ℂ ↔ ∃ i < n, exp (2 * π * I * (i / n)) = x

Proof state:
case mpr.intro.intro
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
i : ℕ
left✝ : i < n
H : cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
⊢ ↑x ^ n = 1

Tactic:
rw [← H, ← exp_nat_mul, exp_eq_one_iff]

Result:
case mpr.intro.intro
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
i : ℕ
left✝ : i < n
H : cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)

Proof state:
case h
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
i : ℕ
left✝ : i < n
H : cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
⊢ ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑↑i * (2 * ↑π * I)

Tactic:
field_simp [hn0, mul_comm ((n : ℕ) : ℂ), mul_comm (i : ℂ)]

Result:
no goals

Proof state:
case mp.intro.intro
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Tactic:
refine ⟨i, hi, ?_⟩

Result:
case mp.intro.intro
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Proof state:
case mp.intro.intro
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Tactic:
rw [← H, ← exp_nat_mul]

Result:
case mp.intro.intro
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (↑i * (2 * ↑π * I / ↑n))

Proof state:
case mpr.intro.intro
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
i : ℕ
left✝ : i < n
H : cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)

Tactic:
use i

Result:
case h
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
i : ℕ
left✝ : i < n
H : cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
⊢ ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑↑i * (2 * ↑π * I)

Proof state:
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
⊢ ∃ i < n, cexp (2 * ↑π * I / ↑n) ^ i = ↑x

Tactic:
simpa only using (isPrimitiveRoot_exp n NeZero.out).eq_pow_of_pow_eq_one h

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
x : ℂˣ
⊢ ↑x ^ n = 1 ↔ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Tactic:
have hn0 : (n : ℂ) ≠ 0 := mod_cast NeZero.out

Result:
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ ↑x ^ n = 1 ↔ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Proof state:
case mpr
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ (∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x) → ↑x ^ n = 1

Tactic:
rintro ⟨i, _, H⟩

Result:
case mpr.intro.intro
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
i : ℕ
left✝ : i < n
H : cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
⊢ ↑x ^ n = 1

Proof state:
case mp.intro.intro.e_z
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ 2 * ↑π * I * (↑i / ↑n) = ↑i * (2 * ↑π * I / ↑n)

Tactic:
field_simp [hn0, mul_comm (i : ℂ)]

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ ↑x ^ n = 1 ↔ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Tactic:
constructor

Result:
case mp
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ ↑x ^ n = 1 → ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

case mpr
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ (∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x) → ↑x ^ n = 1

Proof state:
n : ℕ
inst✝ : NeZero n
x : ℂˣ
⊢ x ∈ rootsOfUnity n ℂ ↔ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Tactic:
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one]

Result:
n : ℕ
inst✝ : NeZero n
x : ℂˣ
⊢ ↑x ^ n = 1 ↔ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Proof state:
case mp
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ ↑x ^ n = 1 → ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Tactic:
intro h

Result:
case mp
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
⊢ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Proof state:
case mp.intro.intro
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (↑i * (2 * ↑π * I / ↑n))

Tactic:
congr 1

Result:
case mp.intro.intro.e_z
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ 2 * ↑π * I * (↑i / ↑n) = ↑i * (2 * ↑π * I / ↑n)

Proof state:
case mp
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
⊢ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x

Tactic:
obtain ⟨i, hi, H⟩ : ∃ i < (n : ℕ), exp (2 * π * I / n) ^ i = x := by
  simpa only using (isPrimitiveRoot_exp n NeZero.out).eq_pow_of_pow_eq_one h

Result:
case mp.intro.intro
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
h : ↑x ^ n = 1
i : ℕ
hi : i < n
H : cexp (2 * ↑π * I / ↑n) ^ i = ↑x
⊢ ∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x