-- Mathlib/RingTheory/RootsOfUnity/Complex.lean
theorem isPrimitiveRoot_exp_of_coprime (i n : ℕ) (h0 : n ≠ 0) (hi : i.Coprime n) :
    IsPrimitiveRoot (exp (2 * π * I * (i / n))) n

Proof state:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
⊢ n ∣ l

Tactic:
have hz : 2 * ↑π * I ≠ 0 := by simp [pi_pos.ne.symm, I_ne_zero]

Result:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
hz : 2 * ↑π * I ≠ 0
⊢ n ∣ l

Proof state:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
this : n ∣ i * l
⊢ n ∣ l

Tactic:
exact hi.symm.dvd_of_dvd_mul_left this

Result:
no goals

Proof state:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
⊢ IsPrimitiveRoot (cexp (2 * ↑π * I * (↑i / ↑n))) n

Tactic:
rw [IsPrimitiveRoot.iff_def]

Result:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) ^ n = 1 ∧ ∀ (l : ℕ), cexp (2 * ↑π * I * (↑i / ↑n)) ^ l = 1 → n ∣ l

Proof state:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑(i * l) * (↑(2 * π) * I) = ↑x * (↑(2 * π) * I) * ↑n → n ∣ l

Tactic:
rintro l k hk

Result:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑k * (↑(2 * π) * I) * ↑n
⊢ n ∣ l

Proof state:
case left
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)

Tactic:
use i

Result:
case h
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑↑i * (2 * ↑π * I)

Proof state:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l

Tactic:
simp only [hn0, mul_right_comm _ _ ↑n, mul_left_inj' two_pi_I_ne_zero, Ne, not_false_iff,
  mul_comm _ (i : ℂ), ← mul_assoc _ (i : ℂ), exists_imp, field_simps]

Result:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑i * ↑l * (2 * ↑π * I) = ↑x * (2 * ↑π * I) * ↑n → n ∣ l

Proof state:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑i * ↑l = ↑n * ↑k
⊢ n ∣ l

Tactic:
norm_cast at hk

Result:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ n ∣ l

Proof state:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ ↑n ∣ k * ↑n

Tactic:
apply dvd_mul_left

Result:
no goals

Proof state:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
⊢ (∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧
    ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l

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

Result:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ (∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧
    ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l

Proof state:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
⊢ 2 * ↑π * I ≠ 0

Tactic:
simp [pi_pos.ne.symm, I_ne_zero]

Result:
no goals

Proof state:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
hz : 2 * ↑π * I ≠ 0
⊢ n ∣ l

Tactic:
field_simp [hz] at hk

Result:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑i * ↑l = ↑n * ↑k
⊢ n ∣ l

Proof state:
case h
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑↑i * (2 * ↑π * I)

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

Result:
no goals

Proof state:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ n ∣ l

Tactic:
have : n ∣ i * l := by rw [← Int.natCast_dvd_natCast, hk, mul_comm]; apply dvd_mul_left

Result:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
this : n ∣ i * l
⊢ n ∣ l

Proof state:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ n ∣ i * l

Tactic:
rw [← Int.natCast_dvd_natCast, hk, mul_comm]

Result:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hz : 2 * ↑π * I ≠ 0
hk : ↑(i * l) = ↑n * k
⊢ ↑n ∣ k * ↑n

Proof state:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
⊢ cexp (2 * ↑π * I * (↑i / ↑n)) ^ n = 1 ∧ ∀ (l : ℕ), cexp (2 * ↑π * I * (↑i / ↑n)) ^ l = 1 → n ∣ l

Tactic:
simp only [← exp_nat_mul, exp_eq_one_iff]

Result:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
⊢ (∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧
    ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l

Proof state:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑k * (↑(2 * π) * I) * ↑n
⊢ n ∣ l

Tactic:
conv_rhs at hk => rw [mul_comm, ← mul_assoc]

Result:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
l : ℕ
k : ℤ
hk : ↑(i * l) * (↑(2 * π) * I) = ↑n * ↑k * (↑(2 * π) * I)
⊢ n ∣ l

Proof state:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑i * ↑l * (2 * ↑π * I) = ↑x * (2 * ↑π * I) * ↑n → n ∣ l

Tactic:
norm_cast

Result:
case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ) (x : ℤ), ↑(i * l) * (↑(2 * π) * I) = ↑x * (↑(2 * π) * I) * ↑n → n ∣ l

Proof state:
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ (∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) ∧
    ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l

Tactic:
constructor

Result:
case left
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)

case right
i n : ℕ
h0 : n ≠ 0
hi : i.Coprime n
hn0 : ↑n ≠ 0
⊢ ∀ (l : ℕ), (∃ n_1, ↑l * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)) → n ∣ l