-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem nthRoots_nodup {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) {a : R} (ha : a ≠ 0) :
    (nthRoots n a).Nodup

Proof state:
case pos.intro
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
⊢ (nthRoots n a).Nodup

Tactic:
by_cases hα' : α = 0

Result:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : α = 0
⊢ (nthRoots n a).Nodup

case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : ¬α = 0
⊢ (nthRoots n a).Nodup

Proof state:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ¬∃ α, α ^ n = a
⊢ (nthRoots n a).Nodup

Tactic:
suffices nthRoots n a = 0 by simp [this]

Result:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ¬∃ α, α ^ n = a
⊢ nthRoots n a = 0

Proof state:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ¬∃ α, α ^ n = a
this : nthRoots n a = 0
⊢ (nthRoots n a).Nodup

Tactic:
simp [this]

Result:
no goals

Proof state:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ∃ α, α ^ n = a
⊢ (nthRoots n a).Nodup

Tactic:
obtain ⟨α, hα⟩ := h

Result:
case pos.intro
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
⊢ (nthRoots n a).Nodup

Proof state:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : ¬α = 0
⊢ ∀ x ∈ Multiset.range n, ∀ y ∈ Multiset.range n, ζ ^ x * α = ζ ^ y * α → x = y

Tactic:
exact h.injOn_pow_mul hα'

Result:
no goals

Proof state:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ∀ (α : R), α ^ n ≠ a
⊢ nthRoots n a = 0

Tactic:
simpa only [Multiset.card_eq_zero, Multiset.eq_zero_iff_forall_not_mem, mem_nthRoots hn]

Result:
no goals

Proof state:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : ¬α = 0
⊢ (nthRoots n a).Nodup

Tactic:
rw [nthRoots_eq h hα, Multiset.nodup_map_iff_inj_on (Multiset.nodup_range n)]

Result:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : ¬α = 0
⊢ ∀ x ∈ Multiset.range n, ∀ y ∈ Multiset.range n, ζ ^ x * α = ζ ^ y * α → x = y

Proof state:
case inr
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
⊢ (nthRoots n a).Nodup

Tactic:
by_cases h : ∃ α, α ^ n = a

Result:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ∃ α, α ^ n = a
⊢ (nthRoots n a).Nodup

case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ¬∃ α, α ^ n = a
⊢ (nthRoots n a).Nodup

Proof state:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
⊢ (nthRoots n a).Nodup

Tactic:
obtain (rfl | hn) := n.eq_zero_or_pos

Result:
case inl
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ a : R
ha : a ≠ 0
h : IsPrimitiveRoot ζ 0
⊢ (nthRoots 0 a).Nodup

case inr
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
⊢ (nthRoots n a).Nodup

Proof state:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ¬∃ α, α ^ n = a
⊢ nthRoots n a = 0

Tactic:
push_neg at h

Result:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ∀ (α : R), α ^ n ≠ a
⊢ nthRoots n a = 0

Proof state:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : α = 0
⊢ a = 0

Tactic:
rwa [hα', zero_pow hn.ne', eq_comm] at hα

Result:
no goals

Proof state:
case inl
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ a : R
ha : a ≠ 0
h : IsPrimitiveRoot ζ 0
⊢ (nthRoots 0 a).Nodup

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : α = 0
⊢ (nthRoots n a).Nodup

Tactic:
exact (ha (by rwa [hα', zero_pow hn.ne', eq_comm] at hα)).elim

Result:
no goals