awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ ζ ^ m * α ∈ nthRoots n a
have neg₃ : ζ ^ (m * n) * a = a
Tactic: rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ ζ ^ m * α ∈ nthRoots n a
have neg₄ : ζ ^ (n * m) * a = a
Tactic: rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ ζ ^ m * α ∈ nthRoots n a
have neg₅ : (ζ ^ n) ^ m * a = a
Tactic: rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ ζ ^ m * α ∈ nthRoots n a
have neg₆ : HPow.hPow (α := R) 1 m * a = a
Tactic: rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ ζ ^ m * α ∈ nthRoots n a
have neg₇ : 1 * a = a
Tactic: rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ ζ ^ m * α ∈ nthRoots n a
have neg₈ : a = a
Tactic: rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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 = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
have neg : Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) = nthRoots n a
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
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
have neg₂ : Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) ≤ nthRoots n a
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
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
have neg₃ : (nthRoots n a).card ≤ Multiset.card.{u_4} (α := R) (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
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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₂)
⊢ Eq (α := Subalgebra S R) S[ζ₁, ζ₂] S[ζ]
have this : NeZero (k₁.lcm k₂)
Tactic: have : NeZero (k₁.lcm k₂) := ⟨Nat.lcm_ne_zero hk₁ hk₂⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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[ζ]
have refine_1 : {ζ₁, ζ₂} ⊆ (↑S[ζ] : Set R)
Tactic: refine le_antisymm (Algebra.adjoin_le ?_) (Algebra.adjoin_le ?_)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
⊢ Eq (α := Subalgebra S R) S[ζ₁, ζ₂] S[ζ]
have refine_2 : {ζ} ⊆ (↑S[ζ₁, ζ₂] : Set R)
Tactic: refine le_antisymm (Algebra.adjoin_le ?_) (Algebra.adjoin_le ?_)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
have refine_1 : ζ₁ ∈ (↑S[ζ] : Set R)
Tactic: refine Set.pair_subset_iff.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
⊢ {ζ₁, ζ₂} ⊆ (↑S[ζ] : Set R)
have refine_1₁ : ζ₂ ∈ (↑S[ζ] : Set R)
Tactic: refine Set.pair_subset_iff.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
have refine_1 : ∀ w < k₁.lcm k₂, ∀ (hζ₂ : IsPrimitiveRoot (ζ ^ w) k₂), ζ ^ w ∈ (↑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₂
Cleared hypotheses: ζ₂, hζ₂
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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)
have hζ' : IsPrimitiveRoot (ζ₁ ^ (k₁ / k₁.factorizationLCMLeft k₂) * ζ₂ ^ (k₂ / k₁.factorizationLCMRight k₂)) (k₁.lcm k₂)
Tactic: have hζ' := IsPrimitiveRoot.pow_mul_pow_lcm hζ₁ hζ₂ hk₁ hk₂
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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₂)
⊢ {ζ} ⊆ (↑S[ζ₁, ζ₂] : Set R)
have 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)
Tactic: obtain ⟨_, _, rfl⟩ := hζ'.eq_pow_of_pow_eq_one hζ.pow_eq_one
Cleared hypotheses: ζ, hζ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
⊢ (nthRoots n a).card = if ∃ (α : R), α ^ n = a then n else 0
have pos : ∀ (h : ∃ (α : R), α ^ n = a), (nthRoots n a).card = n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ (nthRoots n a).card = if ∃ (α : R), α ^ n = a then n else 0
have neg : ∀ (h : ¬∃ (α : R), α ^ n = a), (nthRoots n a).card = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
h : ∃ (α : R), α ^ n = a
⊢ (nthRoots n a).card = n
have pos : ∀ (α : R) (hα : α ^ n = a), (nthRoots n a).card = n
Tactic: obtain ⟨α, hα⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a α : R
hα : α ^ n = a
⊢ (nthRoots n a).card = n
have pos : Multiset.card.{u_4} (α := R) (Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)) = n
Tactic: rw [nthRoots_eq hζ hα, Multiset.card_map, Multiset.card_range]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a α : R
hα : α ^ n = a
pos : Multiset.card.{u_4} (α := R) (Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)) = n
⊢ (nthRoots n a).card = n
have pos₁ : (Multiset.range n).card = n
Tactic: rw [nthRoots_eq hζ hα, Multiset.card_map, Multiset.card_range]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a α : R
hα : α ^ n = a
pos : Multiset.card.{u_4} (α := R) (Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)) = n
pos₁ : (Multiset.range n).card = n
⊢ (nthRoots n a).card = n
have pos₂ : n = n
Tactic: rw [nthRoots_eq hζ hα, Multiset.card_map, Multiset.card_range]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
h : ¬∃ (α : R), α ^ n = a
⊢ (nthRoots n a).card = 0
have neg : ∀ (hζ : IsPrimitiveRoot ζ 0) (h : ¬∃ (α : R), HPow.hPow (β := ℕ) α 0 = a), (nthRoots 0 a).card = 0
Tactic: obtain (rfl | hn) := n.eq_zero_or_pos
Cleared hypotheses: n, hζ, h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
h : ¬∃ (α : R), α ^ n = a
neg : ∀ (hζ : IsPrimitiveRoot ζ 0) (h : ¬∃ (α : R), HPow.hPow (β := ℕ) α 0 = a), (nthRoots 0 a).card = 0
⊢ (nthRoots n a).card = 0
have neg₁ : ∀ (hn : n > 0), (nthRoots n a).card = 0
Tactic: obtain (rfl | hn) := n.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
h : ¬∃ (α : R), α ^ n = a
hn : n > 0
⊢ (nthRoots n a).card = 0
have h₁ : ∀ (α : R), α ^ n ≠ a
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
ζ : Rˣ
inst_1 : IsDomain R
n : ℕ
inst_2 : NeZero n
h : IsPrimitiveRoot ζ n
e : ZMod n ≃+ Additive ↥(Subgroup.zpowers ζ) := h.zmodEquivZPowers
⊢ Fintype.card.{u_4} ↥(rootsOfUnity n R) = n
have have : ∀ (this : Fintype ↥(Subgroup.zpowers ζ)), Fintype.card.{u_4} ↥(rootsOfUnity n R) = n
Tactic: have : Fintype (Subgroup.zpowers ζ) := Fintype.ofEquiv _ e.toEquiv
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
ζ : Rˣ
inst_1 : IsDomain R
n : ℕ
inst_2 : NeZero n
h : IsPrimitiveRoot ζ n
e : ZMod n ≃+ Additive ↥(Subgroup.zpowers ζ) := h.zmodEquivZPowers
this : Fintype ↥(Subgroup.zpowers ζ)
⊢ ↥(rootsOfUnity n R) ≃ ↥(Subgroup.zpowers ζ)
have rw : ↥(rootsOfUnity n R) ≃ ↥(rootsOfUnity n R)
Tactic: rw [h.zpowers_eq]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
inst_2 : NeZero n
h : IsPrimitiveRoot ζ n
⊢ Fintype.card.{u_4} ↥(rootsOfUnity n R) = n
have obtain : ∀ (ζ_1 : Rˣ) (hζ : (↑ζ_1 : R) = ζ), Fintype.card.{u_4} ↥(rootsOfUnity n R) = n
Tactic: obtain ⟨ζ, hζ⟩ := h.isUnit NeZero.out
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ_1 : R
n : ℕ
inst_2 : NeZero n
h : IsPrimitiveRoot ζ_1 n
ζ : Rˣ
hζ : (↑ζ : R) = ζ_1
⊢ Fintype.card.{u_4} ↥(rootsOfUnity n R) = n
have h₁ : IsPrimitiveRoot ζ n
Tactic: rw [← hζ, IsPrimitiveRoot.coe_units_iff] at h
Cleared hypotheses: h, hζ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
inst_2 : NeZero n
⊢ Fintype.card.{u_4} ↥(rootsOfUnity n R) = n ↔ ∃ (ζ : R), IsPrimitiveRoot ζ n
have refine : ∀ (h : Fintype.card.{u_4} ↥(rootsOfUnity n R) = n), ∃ (ζ : R), IsPrimitiveRoot ζ n
Tactic: refine ⟨fun h ↦ ?_, fun ⟨ζ, hζ⟩ ↦ hζ.card_rootsOfUnity⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
inst_2 : NeZero n
h : Fintype.card.{u_4} ↥(rootsOfUnity n R) = n
⊢ ∃ (ζ : R), IsPrimitiveRoot ζ n
have obtain : ∀ (ζ : Rˣ) (hζ' : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ)
  (hζ :
    orderOf (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) x) ζ hζ') =
      Nat.card.{u_4} ↥(rootsOfUnity n R)),
  ∃ (ζ : R), IsPrimitiveRoot ζ n
Tactic: obtain ⟨⟨ζ, hζ'⟩, hζ⟩ := (rootsOfUnity.isCyclic R n).exists_ofOrder_eq_natCard
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
inst_2 : NeZero n
h : Fintype.card.{u_4} ↥(rootsOfUnity n R) = n
ζ : Rˣ
hζ' : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ
hζ :
  orderOf (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) x) ζ hζ') =
    Nat.card.{u_4} ↥(rootsOfUnity n R)
⊢ ∃ (ζ : R), IsPrimitiveRoot ζ n
have hζ₁ : IsPrimitiveRoot
  (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) x) ζ hζ') : Rˣ) : R) n
Tactic: rw [Nat.card_eq_fintype_card, h, ← IsPrimitiveRoot.iff_orderOf, ← coe_submonoidClass_iff,
    ← IsPrimitiveRoot.coe_units_iff] at hζ
Cleared hypotheses: hζ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
inst_2 : NeZero n
h : Fintype.card.{u_4} ↥(rootsOfUnity n R) = n
ζ : Rˣ
hζ' : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ
hζ :
  IsPrimitiveRoot
    (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) x) ζ hζ') : Rˣ) : R) n
⊢ ∃ (ζ : R), IsPrimitiveRoot ζ n
have w : R
Tactic: use ζ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
inst_2 : NeZero n
h : Fintype.card.{u_4} ↥(rootsOfUnity n R) = n
ζ : Rˣ
hζ' : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) ζ
hζ :
  IsPrimitiveRoot
    (↑(↑(Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity n R) x) ζ hζ') : Rˣ) : R) n
w : R
⊢ ∃ (ζ : R), IsPrimitiveRoot ζ n
have h₁ : IsPrimitiveRoot (↑ζ : R) n
Tactic: use ζ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ Multiset.card.{u_4} (α := R) (nthRoots n 1) = n
have rw : (if ∃ (α : R), α ^ n = 1 then n else 0) = n
Tactic: rw [card_nthRoots h, if_pos ⟨ζ, h.pow_eq_one⟩]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
rw : (if ∃ (α : R), α ^ n = 1 then n else 0) = n
⊢ Multiset.card.{u_4} (α := R) (nthRoots n 1) = n
have rw₁ : n = n
Tactic: rw [card_nthRoots h, if_pos ⟨ζ, h.pow_eq_one⟩]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
⊢ (nthRoots n a).Nodup
have inl : ∀ (h : IsPrimitiveRoot ζ 0), (nthRoots 0 a).Nodup
Tactic: obtain (rfl | hn) := n.eq_zero_or_pos
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
inl : ∀ (h : IsPrimitiveRoot ζ 0), (nthRoots 0 a).Nodup
⊢ (nthRoots n a).Nodup
have inr : ∀ (hn : n > 0), (nthRoots n a).Nodup
Tactic: obtain (rfl | hn) := n.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
⊢ (nthRoots n a).Nodup
have pos : ∀ (h : ∃ (α : R), α ^ n = a), (nthRoots n a).Nodup
Tactic: by_cases! h : ∃ α, α ^ n = a
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
pos : ∀ (h : ∃ (α : R), α ^ n = a), (nthRoots n a).Nodup
⊢ (nthRoots n a).Nodup
have neg : ∀ (h : ∀ (α : R), α ^ n ≠ a), (nthRoots n a).Nodup
Tactic: by_cases! h : ∃ α, α ^ n = a
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h_1 : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ∃ (α : R), α ^ n = a
⊢ (nthRoots n a).Nodup
have pos : ∀ (α : R) (hα : α ^ n = a), (nthRoots n a).Nodup
Tactic: obtain ⟨α, hα⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
⊢ (nthRoots n a).Nodup
have pos : ∀ (hα' : α = 0), (nthRoots n a).Nodup
Tactic: by_cases hα' : α = 0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
pos : ∀ (hα' : α = 0), (nthRoots n a).Nodup
⊢ (nthRoots n a).Nodup
have neg : ∀ (hα' : ¬α = 0), (nthRoots n a).Nodup
Tactic: by_cases hα' : α = 0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : α = 0
⊢ a = 0
have rwa : ∀ (hα : HPow.hPow (α := R) 0 n = a) (hα' : α = 0), a = 0
Tactic: rwa [hα', zero_pow hn.ne', eq_comm] at hα
Cleared hypotheses: hα, hα'
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : α = 0
rwa : ∀ (hα : HPow.hPow (α := R) 0 n = a) (hα' : α = 0), a = 0
⊢ a = 0
have rwa₁ : ∀ (hα : 0 = a) (hα' : α = 0), a = 0
Tactic: rwa [hα', zero_pow hn.ne', eq_comm] at hα
Cleared hypotheses: hα, hα'
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : α = 0
rwa : ∀ (hα : HPow.hPow (α := R) 0 n = a) (hα' : α = 0), a = 0
rwa₁ : ∀ (hα : 0 = a) (hα' : α = 0), a = 0
⊢ a = 0
have rwa₂ : ∀ (hα : a = 0) (hα' : α = 0), a = 0
Tactic: rwa [hα', zero_pow hn.ne', eq_comm] at hα
Cleared hypotheses: hα, hα'
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : 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
have neg : ∀ x ∈ Multiset.range n, ∀ y ∈ Multiset.range n, ζ ^ x * α = ζ ^ y * α → x = y
Tactic: rw [nthRoots_eq h hα, Multiset.nodup_map_iff_inj_on (Multiset.nodup_range n)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h_1 : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ∀ (α : R), α ^ n ≠ a
⊢ (nthRoots n a).Nodup
have neg : nthRoots n a = 0
Tactic: suffices nthRoots n a = 0 by simp [this]