awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
refine_2 : HPow.hPow (β := ℤ) ζ (↑i₀ : ℤ) = ζ ^ n
refine_2₁ : ζ ^ i = ζ ^ n
refine_2₂ : ζ ^ i = ζ ^ (n % (↑k : ℤ) + (↑k : ℤ) * (n / (↑k : ℤ)))
refine_2₃ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * ζ ^ ((↑k : ℤ) * (n / (↑k : ℤ)))
refine_2₄ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * HPow.hPow (β := ℤ) ζ (↑k : ℤ) ^ (n / (↑k : ℤ))
refine_2₅ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * HPow.hPow (α := Rˣ) 1 (n / (↑k : ℤ))
refine_2₆ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * 1
refine_2₇ refine_2₈ : ζ ^ i = ζ ^ (n % (↑k : ℤ))
⊢ ζ ^ i₀ = ζ ^ n

Tactic:
rw [← zpow_natCast, hi₀, ← Int.emod_add_mul_ediv n k, zpow_add, zpow_mul, h.zpow_eq_one,
      one_zpow, mul_one]

Premises used: zpow_natCast, zpow_add, zpow_mul, one_zpow, Nat.cast, IsPrimitiveRoot.zpow_eq_one, Int.emod_add_mul_ediv, mul_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
hξ : ξ ^ k = 1
⊢ IsUnit ζ

Tactic:
h.isUnit NeZero.out

Premises used: IsPrimitiveRoot.isUnit, NeZero.out
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
hξ : ξ ^ k = 1
lift : ∀ (ζ : Rˣ) (h : IsPrimitiveRoot (↑ζ : R) k), ∃ i < k, (↑ζ : R) ^ i = ξ
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
lift ζ to Rˣ using h.isUnit NeZero.out

Premises used: IsPrimitiveRoot.isUnit, NeZero.out
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ξ : R
hξ : ξ ^ k = 1
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ : R) k
⊢ IsUnit ξ

Tactic:
.of_pow_eq_one hξ <| NeZero.ne k

Premises used: IsUnit.of_pow_eq_one, NeZero.ne
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ξ : R
hξ : ξ ^ k = 1
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ : R) k
lift : ∀ (ξ : Rˣ) (hξ : (↑ξ : R) ^ k = 1), ∃ i < k, (↑ζ : R) ^ i = (↑ξ : R)
⊢ ∃ i < k, (↑ζ : R) ^ i = ξ

Tactic:
lift ξ to Rˣ using .of_pow_eq_one hξ <| NeZero.ne k

Premises used: NeZero.ne
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ : R) k
ξ : Rˣ
hξ : (↑ξ : R) ^ k = 1
simp : ∃ i < k, ζ ^ i = ξ
⊢ ∃ i < k, (↑ζ : R) ^ i = (↑ξ : R)

Tactic:
simp only [← Units.val_pow_eq_pow_val, ← Units.ext_iff]

Premises used: Units.ext_iff, Units.val_pow_eq_pow_val
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ : R) k
ξ : Rˣ
hξ : (↑ξ : R) ^ k = 1
rw : ∀ (h : IsPrimitiveRoot ζ k) (ξ : Rˣ) (hξ : (↑ξ : R) ^ k = 1), ∃ i < k, ζ ^ i = ξ
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
rw [coe_units_iff] at h

Premises used: IsPrimitiveRoot.coe_units_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
ξ : Rˣ
hξ : (↑ξ : R) ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
h.eq_pow_of_mem_rootsOfUnity <| (mem_rootsOfUnity' k ξ).mpr hξ

Premises used: Iff.mpr, IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity, mem_rootsOfUnity'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
ξ : Rˣ
hξ : (↑ξ : R) ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
exact h.eq_pow_of_mem_rootsOfUnity <| (mem_rootsOfUnity' k ξ).mpr hξ

Premises used: Iff.mpr, IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity, mem_rootsOfUnity'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
mp : IsPrimitiveRoot ξ k → ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
mpr : (∃ i < k, i.Coprime k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ k
⊢ IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
constructor
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
hξ : IsPrimitiveRoot ξ k
mp : ∀ (i : ℕ) (hik : i < k) (hξ : IsPrimitiveRoot (ζ ^ i) k), ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i
⊢ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_mem_rootsOfUnity hξ.pow_eq_one

Premises used: IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity, IsPrimitiveRoot.pow_eq_one, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : IsPrimitiveRoot (ζ ^ i) k
⊢ i.Coprime k

Tactic:
rw [h.pow_iff_coprime <| NeZero.pos k] at hξ

Premises used: IsPrimitiveRoot.pow_iff_coprime, NeZero.pos
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : i.Coprime k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i

Tactic:
⟨i, hik, hξ, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : i.Coprime k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i

Tactic:
exact ⟨i, hik, hξ, rfl⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
h.pow_of_coprime i hi

Premises used: IsPrimitiveRoot.pow_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
exact h.pow_of_coprime i hi

Premises used: IsPrimitiveRoot.pow_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
mp : IsPrimitiveRoot ξ k → ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
mpr : (∃ i < k, i.Coprime k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ k
⊢ IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
constructor
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
hξ : IsPrimitiveRoot ξ k
mp : ∀ (i : ℕ) (hik : i < k) (hξ : IsPrimitiveRoot (ζ ^ i) k), ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i
⊢ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_pow_eq_one hξ.pow_eq_one

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one, IsPrimitiveRoot.pow_eq_one, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : R
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : IsPrimitiveRoot (ζ ^ i) k
⊢ i.Coprime k

Tactic:
rw [h.pow_iff_coprime <| NeZero.pos k] at hξ

Premises used: IsPrimitiveRoot.pow_iff_coprime, NeZero.pos
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : R
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : i.Coprime k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i

Tactic:
⟨i, hik, hξ, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : R
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : i.Coprime k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i

Tactic:
exact ⟨i, hik, hξ, rfl⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : R
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
h.pow_of_coprime i hi

Premises used: IsPrimitiveRoot.pow_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : R
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
exact h.pow_of_coprime i hi

Premises used: IsPrimitiveRoot.pow_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
inl :
  ∀ (hζ : IsPrimitiveRoot ζ 0) (e : HPow.hPow (β := ℕ) α 0 = a),
    nthRoots 0 a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range 0)
inr : ∀ (hn : n > 0), nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)

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

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ α a : R
hζ : IsPrimitiveRoot ζ 0
e : HPow.hPow (β := ℕ) α 0 = a
⊢ nthRoots 0 a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
pos : ∀ (hα : α = 0), nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
neg : ∀ (hα : ¬α = 0), nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)

Tactic:
by_cases hα : α = 0
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : α = 0
⊢ 0 = a

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

Premises used: LT.lt.ne', zero_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : α = 0
e₁ : 0 = a
⊢ n > 0

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

Premises used: LT.lt.ne', zero_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : α = 0
e₁ : 0 = a
hn₁ : n > 0
⊢ α = 0

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

Premises used: LT.lt.ne', zero_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : 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,
      Multiset.map_const', Multiset.card_range]

Premises used: Polynomial.nthRoots_zero_right, Multiset.card_range, MulZeroClass.mul_zero, Eq.symm, Multiset.map_const'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
neg : Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) = nthRoots n a
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)

Tactic:
symm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
neg : Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) ≤ nthRoots n a
neg₁ : (nthRoots n a).card ≤ Multiset.card.{u_4} (α := R) (Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n))
⊢ Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) = nthRoots n a

Tactic:
apply Multiset.eq_of_le_of_card_le

Premises used: Multiset.eq_of_le_of_card_le
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
neg : val (image (fun (x : ℕ) ↦ ζ ^ x * α) (range n)) ⊆ nthRoots n a
⊢ 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]

Premises used: Finset.range_val, IsPrimitiveRoot.injOn_pow_mul, Finset.image_val_of_injOn, Finset.val_le_iff_val_subset
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
x : R
hx : Membership.mem (γ := Multiset R) (val (image (fun (x : ℕ) ↦ ζ ^ x * α) (range n))) x
⊢ ∃ a < n, ζ ^ a * α = x

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

Premises used: Finset.range_val, Multiset.mem_map, Multiset.mem_dedup, Multiset.mem_range, Finset.image_val
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
x : R
hx : ∃ a < n, ζ ^ a * α = x
neg : ∀ m < n, ζ ^ m * α ∈ nthRoots n a
⊢ x ∈ nthRoots n a

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

Premises used: rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
m : ℕ
left : m < n
neg : (ζ ^ m * α) ^ n = a
neg₁ : (ζ ^ m) ^ n * α ^ n = a
neg₂ : (ζ ^ m) ^ n * a = a
neg₃ : ζ ^ (m * n) * a = a
neg₄ : ζ ^ (n * m) * a = a
neg₅ : (ζ ^ n) ^ m * a = a
neg₆ : HPow.hPow (α := R) 1 m * a = a
neg₇ : 1 * a = a
neg₈ neg₉ : a = a
⊢ ζ ^ 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]

Premises used: one_pow, pow_mul, mul_comm, Polynomial.mem_nthRoots, mul_pow, IsPrimitiveRoot.pow_eq_one, one_mul
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ (nthRoots n a).card ≤ Multiset.card.{u_4} (α := R) (Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n))

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

Premises used: Multiset.card_range, Polynomial.card_nthRoots, Multiset.card_map
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
neg neg₁ : Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) = nthRoots n a
neg₂ : Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) ≤ nthRoots n a
neg₃ neg₄ :
  (nthRoots n a).card ≤ Multiset.card.{u_4} (α := R) (Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n))
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)

Tactic:
classical
  symm; apply Multiset.eq_of_le_of_card_le
  · rw [← Finset.range_val,
      ← Finset.image_val_of_injOn (hζ.injOn_pow_mul hα), Finset.val_le_iff_val_subset]
    intro x hx
    simp only [Finset.image_val, Finset.range_val, Multiset.mem_dedup, Multiset.mem_map,
      Multiset.mem_range] at hx
    obtain ⟨m, _, rfl⟩ := hx
    rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]
  · simpa only [Multiset.card_map, Multiset.card_range] using card_nthRoots n a

Premises used: Finset.range_val, one_pow, Multiset.mem_map, Multiset.card_range, Polynomial.card_nthRoots, Multiset.mem_dedup, Multiset.mem_range, pow_mul, Polynomial.mem_nthRoots, Finset.image_val, Multiset.eq_of_le_of_card_le, mul_pow, IsPrimitiveRoot.pow_eq_one, Finset.val_le_iff_val_subset, one_mul, rfl, Multiset.card_map
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
⊢ NeZero (k₁.lcm k₂)

Tactic:
have : NeZero (k₁.lcm k₂) := ⟨Nat.lcm_ne_zero hk₁ hk₂⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
⊢ Eq (α := Subalgebra S R) S[ζ₁, ζ₂] S[ζ]

Tactic:
le_antisymm (Algebra.adjoin_le ?_) (Algebra.adjoin_le ?_)

Premises used: le_antisymm, Algebra.adjoin_le
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
refine_1 : {ζ₁, ζ₂} ⊆ (↑S[ζ] : Set R)
refine_2 : {ζ} ⊆ (↑S[ζ₁, ζ₂] : Set R)
⊢ Eq (α := Subalgebra S R) S[ζ₁, ζ₂] S[ζ]

Tactic:
refine le_antisymm (Algebra.adjoin_le ?_) (Algebra.adjoin_le ?_)

Premises used: le_antisymm, Algebra.adjoin_le
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
⊢ {ζ₁, ζ₂} ⊆ (↑S[ζ] : Set R)

Tactic:
Set.pair_subset_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, Set.pair_subset_iff, And.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
refine_1 : ζ₁ ∈ (↑S[ζ] : Set R)
refine_1₁ : ζ₂ ∈ (↑S[ζ] : Set R)
⊢ {ζ₁, ζ₂} ⊆ (↑S[ζ] : Set R)

Tactic:
refine Set.pair_subset_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, Set.pair_subset_iff, And.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₂ : R
k₁ k₂ : ℕ
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
w : ℕ
left : w < k₁.lcm k₂
hζ₁ : IsPrimitiveRoot (ζ ^ w) k₁
⊢ ζ ^ w ∈ (↑S[ζ] : Set R)

Tactic:
Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _

Premises used: Subalgebra.pow_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₂ : R
k₁ k₂ : ℕ
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
w : ℕ
left : w < k₁.lcm k₂
hζ₁ : IsPrimitiveRoot (ζ ^ w) k₁
⊢ ζ ^ w ∈ (↑S[ζ] : Set R)

Tactic:
exact Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _

Premises used: Subalgebra.pow_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
refine_1 : ∀ w < k₁.lcm k₂, ∀ (hζ₂ : IsPrimitiveRoot (ζ ^ w) k₂), ζ ^ w ∈ (↑S[ζ] : Set R)
⊢ ζ₂ ∈ (↑S[ζ] : Set R)

Tactic:
obtain ⟨_, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one <|
        (hζ₂.pow_eq_one_iff_dvd _).mpr <| k₁.dvd_lcm_right k₂

Premises used: Iff.mpr, IsPrimitiveRoot.pow_eq_one_iff_dvd, IsPrimitiveRoot.eq_pow_of_pow_eq_one, Nat.dvd_lcm_right, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₁ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
w : ℕ
left : w < k₁.lcm k₂
hζ₂ : IsPrimitiveRoot (ζ ^ w) k₂
⊢ ζ ^ w ∈ (↑S[ζ] : Set R)

Tactic:
Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _

Premises used: Subalgebra.pow_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₁ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
w : ℕ
left : w < k₁.lcm k₂
hζ₂ : IsPrimitiveRoot (ζ ^ w) k₂
⊢ ζ ^ w ∈ (↑S[ζ] : Set R)

Tactic:
exact Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _

Premises used: Subalgebra.pow_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
⊢ IsPrimitiveRoot (ζ₁ ^ (k₁ / k₁.factorizationLCMLeft k₂) * ζ₂ ^ (k₂ / k₁.factorizationLCMRight k₂)) (k₁.lcm k₂)

Tactic:
have hζ' := IsPrimitiveRoot.pow_mul_pow_lcm hζ₁ hζ₂ hk₁ hk₂
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
hζ' : IsPrimitiveRoot (ζ₁ ^ (k₁ / k₁.factorizationLCMLeft k₂) * ζ₂ ^ (k₂ / k₁.factorizationLCMRight k₂)) (k₁.lcm k₂)
refine_2 :
  ∀ w < k₁.lcm k₂,
    ∀
      (hζ :
        IsPrimitiveRoot ((ζ₁ ^ (k₁ / k₁.factorizationLCMLeft k₂) * ζ₂ ^ (k₂ / k₁.factorizationLCMRight k₂)) ^ w)
          (k₁.lcm k₂)),
      {(ζ₁ ^ (k₁ / k₁.factorizationLCMLeft k₂) * ζ₂ ^ (k₂ / k₁.factorizationLCMRight k₂)) ^ w} ⊆ (↑S[ζ₁, ζ₂] : Set R)
⊢ {ζ} ⊆ (↑S[ζ₁, ζ₂] : Set R)

Tactic:
obtain ⟨_, _, rfl⟩ := hζ'.eq_pow_of_pow_eq_one hζ.pow_eq_one

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one, IsPrimitiveRoot.pow_eq_one, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
inst_2 : CommSemiring S
inst_3 : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
this : NeZero (k₁.lcm k₂)
hζ' : IsPrimitiveRoot (ζ₁ ^ (k₁ / k₁.factorizationLCMLeft k₂) * ζ₂ ^ (k₂ / k₁.factorizationLCMRight k₂)) (k₁.lcm k₂)
w : ℕ
left : w < k₁.lcm k₂
hζ :
  IsPrimitiveRoot ((ζ₁ ^ (k₁ / k₁.factorizationLCMLeft k₂) * ζ₂ ^ (k₂ / k₁.factorizationLCMRight k₂)) ^ w) (k₁.lcm k₂)
⊢ {(ζ₁ ^ (k₁ / k₁.factorizationLCMLeft k₂) * ζ₂ ^ (k₂ / k₁.factorizationLCMRight k₂)) ^ w} ⊆ (↑S[ζ₁, ζ₂] : Set R)

Tactic:
aesop
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
pos : ∀ (h : ∃ (α : R), α ^ n = a), (nthRoots n a).card = n
neg : ∀ (h : ¬∃ (α : R), α ^ n = a), (nthRoots n a).card = 0
⊢ (nthRoots n a).card = if ∃ (α : R), α ^ n = a then n else 0

Tactic:
split_ifs with h