-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem nthRoots_eq {n : ℕ} {ζ : R} (hζ : IsPrimitiveRoot ζ n) {α a : R} (e : α ^ n = a) :
    nthRoots n a = (Multiset.range n).map (ζ ^ · * α)

Proof state:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : 0 = a
hn : n > 0
hα : α = 0
⊢ nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)

Tactic:
simp only [hα, e.symm, nthRoots_zero_right, mul_zero,
  Finset.range_val, Multiset.map_const', Multiset.card_range]

Result:
no goals

Proof state:
case neg.h.intro.intro
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
m : ℕ
left✝ : m < n
⊢ ζ ^ m * α ∈ nthRoots n a

Tactic:
rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
  pow_mul, hζ.pow_eq_one, one_pow, one_mul]

Result:
no goals

Proof state:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : α = 0
⊢ nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)

Tactic:
rw [hα, zero_pow hn.ne'] at e

Result:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : 0 = a
hn : n > 0
hα : α = 0
⊢ nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)

Proof state:
case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ Multiset.map (fun x => ζ ^ x * α) (Multiset.range n) ≤ nthRoots n a

Tactic:
rw [← Finset.range_val,
  ← Finset.image_val_of_injOn (hζ.injOn_pow_mul hα), Finset.val_le_iff_val_subset]

Result:
case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ (image (fun x => ζ ^ x * α) (range n)).val ⊆ nthRoots n a

Proof state:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)

Tactic:
symm

Result:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ Multiset.map (fun x => ζ ^ x * α) (Multiset.range n) = nthRoots n a

Proof state:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ Multiset.map (fun x => ζ ^ x * α) (Multiset.range n) = nthRoots n a

Tactic:
apply Multiset.eq_of_le_of_card_le

Result:
case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ Multiset.map (fun x => ζ ^ x * α) (Multiset.range n) ≤ nthRoots n a

case neg.a
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ (nthRoots n a).card ≤ (Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)).card

Proof state:
case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ (image (fun x => ζ ^ x * α) (range n)).val ⊆ nthRoots n a

Tactic:
intro x hx

Result:
case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
x : R
hx : x ∈ (image (fun x => ζ ^ x * α) (range n)).val
⊢ x ∈ nthRoots n a

Proof state:
case inl
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ α a : R
hζ : IsPrimitiveRoot ζ 0
e : α ^ 0 = a
⊢ nthRoots 0 a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range 0)

Tactic:
simp

Result:
no goals

Proof state:
case neg.a
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ (nthRoots n a).card ≤ (Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)).card

Tactic:
simpa only [Multiset.card_map, Multiset.card_range] using card_nthRoots n a

Result:
no goals

Proof state:
case inr
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
⊢ nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)

Tactic:
by_cases hα : α = 0

Result:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : α = 0
⊢ nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)

case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)

Proof state:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
⊢ nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)

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

Result:
case inl
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ α a : R
hζ : IsPrimitiveRoot ζ 0
e : α ^ 0 = a
⊢ nthRoots 0 a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range 0)

case inr
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
⊢ nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)

Proof state:
case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
x : R
hx : x ∈ (image (fun x => ζ ^ x * α) (range n)).val
⊢ x ∈ nthRoots n a

Tactic:
simp only [Finset.image_val, Finset.range_val, Multiset.mem_dedup, Multiset.mem_map,
  Multiset.mem_range] at hx

Result:
case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
x : R
hx : ∃ a < n, ζ ^ a * α = x
⊢ x ∈ nthRoots n a

Proof state:
case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
x : R
hx : ∃ a < n, ζ ^ a * α = x
⊢ x ∈ nthRoots n a

Tactic:
obtain ⟨m, _, rfl⟩ := hx

Result:
case neg.h.intro.intro
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
m : ℕ
left✝ : m < n
⊢ ζ ^ m * α ∈ nthRoots n a