-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem nthRoots_one_eq_biUnion_primitiveRoots' [DecidableEq R] {n : ℕ} [NeZero n] :
    nthRootsFinset n R = (Nat.divisors n).biUnion fun i ↦ primitiveRoots i R

Proof state:
case h
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
⊢ x ^ n = 1 ↔ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R

Tactic:
constructor

Result:
case h.mp
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
⊢ x ^ n = 1 → ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R

case h.mpr
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
⊢ (∃ a, a ∣ n ∧ x ∈ primitiveRoots a R) → x ^ n = 1

Proof state:
case h.mpr.intro.intro.intro
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : n = a * d
hazero : 0 < a
⊢ x ^ n = 1

Tactic:
rw [mem_primitiveRoots hazero] at ha

Result:
case h.mpr.intro.intro.intro
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : IsPrimitiveRoot x a
d : ℕ
hd : n = a * d
hazero : 0 < a
⊢ x ^ n = 1

Proof state:
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : n = a * d
ha₀ : a = 0
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
this : x ^ n = 1 ↔ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R
⊢ x ∈ nthRootsFinset n R ↔ x ∈ n.divisors.biUnion fun i => primitiveRoots i R

Tactic:
simpa [Polynomial.mem_nthRootsFinset (NeZero.pos n), (NeZero.ne n)]

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : IsPrimitiveRoot x a
d : ℕ
hd : n = a * d
hazero : 0 < a
⊢ x ^ n = 1

Tactic:
rw [hd, pow_mul, ha.pow_eq_one, one_pow]

Result:
no goals

Proof state:
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
⊢ nthRootsFinset n R = n.divisors.biUnion fun i => primitiveRoots i R

Tactic:
ext x

Result:
case h
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
⊢ x ∈ nthRootsFinset n R ↔ x ∈ n.divisors.biUnion fun i => primitiveRoots i R

Proof state:
case h.mp
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
H : x ^ n = 1
⊢ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R

Tactic:
obtain ⟨k, hk, hx⟩ := exists_pos H (NeZero.ne n)

Result:
case h.mp.intro.intro
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
H : x ^ n = 1
k : ℕ
hk : k > 0
hx : IsPrimitiveRoot x k
⊢ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R

Proof state:
case h.mp.intro.intro
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
H : x ^ n = 1
k : ℕ
hk : k > 0
hx : IsPrimitiveRoot x k
⊢ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R

Tactic:
exact ⟨k, hx.2 _ H, (mem_primitiveRoots hk).mpr hx⟩

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : n = a * d
⊢ x ^ n = 1

Tactic:
have hazero : 0 < a := Nat.pos_of_ne_zero fun ha₀ ↦ by simp_all

Result:
case h.mpr.intro.intro.intro
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : n = a * d
hazero : 0 < a
⊢ x ^ n = 1

Proof state:
case h
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
⊢ x ∈ nthRootsFinset n R ↔ x ∈ n.divisors.biUnion fun i => primitiveRoots i R

Tactic:
suffices x ^ n = 1 ↔ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R by
  simpa [Polynomial.mem_nthRootsFinset (NeZero.pos n), (NeZero.ne n)]

Result:
case h
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
⊢ x ^ n = 1 ↔ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R

Proof state:
case h.mp
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
⊢ x ^ n = 1 → ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R

Tactic:
intro H

Result:
case h.mp
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
H : x ^ n = 1
⊢ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R

Proof state:
case h.mpr
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
⊢ (∃ a, a ∣ n ∧ x ∈ primitiveRoots a R) → x ^ n = 1

Tactic:
rintro ⟨a, ⟨d, hd⟩, ha⟩

Result:
case h.mpr.intro.intro.intro
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : n = a * d
⊢ x ^ n = 1