-- Mathlib/RingTheory/RootsOfUnity/Complex.lean
theorem isPrimitiveRoot_iff (ζ : ℂ) (n : ℕ) (hn : n ≠ 0) :
    IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ _ : i.Coprime n, exp (2 * π * I * (i / n)) = ζ

Proof state:
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Tactic:
constructor

Result:
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n

Proof state:
case mp.intro.intro.e_z
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ 2 * ↑π * I * (↑i / ↑n) = ↑i * (2 * ↑π * I / ↑n)

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

Result:
no goals

Proof state:
ζ : ℂ
n : ℕ
hn : n ≠ 0
⊢ IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Tactic:
have hn0 : (n : ℂ) ≠ 0 := mod_cast hn

Result:
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Proof state:
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
h : IsPrimitiveRoot ζ n
⊢ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Tactic:
have : NeZero n := ⟨hn⟩

Result:
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
h : IsPrimitiveRoot ζ n
this : NeZero n
⊢ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Proof state:
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n

Tactic:
swap

Result:
case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n

case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Proof state:
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (2 * ↑π * I / ↑n) ^ i

Tactic:
rw [← exp_nat_mul]

Result:
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (↑i * (2 * ↑π * I / ↑n))

Proof state:
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Tactic:
intro h

Result:
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
h : IsPrimitiveRoot ζ n
⊢ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Proof state:
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (↑i * (2 * ↑π * I / ↑n))

Tactic:
congr 1

Result:
case mp.intro.intro.e_z
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ 2 * ↑π * I * (↑i / ↑n) = ↑i * (2 * ↑π * I / ↑n)

Proof state:
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
h : IsPrimitiveRoot ζ n
this : NeZero n
⊢ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Tactic:
obtain ⟨i, hi, rfl⟩ :=
  (isPrimitiveRoot_exp n hn).eq_pow_of_pow_eq_one h.pow_eq_one

Result:
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ ∃ i_1 < n, ∃ (_ : i_1.Coprime n), cexp (2 * ↑π * I * (↑i_1 / ↑n)) = cexp (2 * ↑π * I / ↑n) ^ i

Proof state:
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ ∃ i_1 < n, ∃ (_ : i_1.Coprime n), cexp (2 * ↑π * I * (↑i_1 / ↑n)) = cexp (2 * ↑π * I / ↑n) ^ i

Tactic:
refine ⟨i, hi, ((isPrimitiveRoot_exp n hn).pow_iff_coprime (Nat.pos_of_ne_zero hn) i).mp h, ?_⟩

Result:
case mp.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
this : NeZero n
i : ℕ
hi : i < n
h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (2 * ↑π * I / ↑n) ^ i

Proof state:
case mpr
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ) → IsPrimitiveRoot ζ n

Tactic:
rintro ⟨i, -, hi, rfl⟩

Result:
case mpr.intro.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i.Coprime n
⊢ IsPrimitiveRoot (cexp (2 * ↑π * I * (↑i / ↑n))) n

Proof state:
case mpr.intro.intro.intro
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
i : ℕ
hi : i.Coprime n
⊢ IsPrimitiveRoot (cexp (2 * ↑π * I * (↑i / ↑n))) n

Tactic:
exact isPrimitiveRoot_exp_of_coprime i n hn hi

Result:
no goals