awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
h : ∃ (α : R), α ^ n = a
pos : ∀ (α : R) (hα : α ^ n = a), (nthRoots n a).card = n
⊢ (nthRoots n a).card = n

Tactic:
obtain ⟨α, hα⟩ := h
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
pos₂ pos₃ : n = n
⊢ (nthRoots n a).card = n

Tactic:
rw [nthRoots_eq hζ hα, Multiset.card_map, Multiset.card_range]

Premises used: Multiset.card_range, IsPrimitiveRoot.nthRoots_eq, 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
h : ¬∃ (α : R), α ^ n = a
neg : ∀ (hζ : IsPrimitiveRoot ζ 0) (h : ¬∃ (α : R), HPow.hPow (β := ℕ) α 0 = a), (nthRoots 0 a).card = 0
neg₁ : ∀ (hn : n > 0), (nthRoots n a).card = 0
⊢ (nthRoots n a).card = 0

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
h : ¬∃ (α : R), HPow.hPow (β := ℕ) α 0 = a
⊢ (nthRoots 0 a).card = 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
h : ¬∃ (α : R), α ^ n = a
hn : n > 0
⊢ ∀ (α : R), α ^ n ≠ a

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
hn : n > 0
h : ∀ (α : R), α ^ n ≠ a
⊢ (nthRoots n a).card = 0

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

Premises used: Multiset.card_eq_zero, Multiset.eq_zero_iff_forall_notMem, Polynomial.mem_nthRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
have : ∀ (this : Fintype ↥(Subgroup.zpowers ζ)), Fintype.card.{u_4} ↥(rootsOfUnity n R) = n
⊢ Fintype.card.{u_4} ↥(rootsOfUnity n R) = n

Tactic:
have : Fintype (Subgroup.zpowers ζ) := Fintype.ofEquiv _ e.toEquiv
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 ζ)
rw rw₁ : ↥(rootsOfUnity n R) ≃ ↥(rootsOfUnity n R)
⊢ ↥(rootsOfUnity n R) ≃ ↥(Subgroup.zpowers ζ)

Tactic:
rw [h.zpowers_eq]

Premises used: IsPrimitiveRoot.zpowers_eq
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 ζ)
⊢ Fintype.card.{u_4} ↥(Subgroup.zpowers ζ) = Fintype.card (ZMod n)

Tactic:
Fintype.card_congr e.toEquiv.symm

Premises used: Fintype.card_congr, AddEquiv.toEquiv, Equiv.symm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 ζ)
⊢ Fintype.card (ZMod n) = n

Tactic:
ZMod.card n

Premises used: ZMod.card
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 ζ)
⊢ Fintype.card.{u_4} ↥(rootsOfUnity n R) = n

Tactic:
calc
    Fintype.card (rootsOfUnity n R) = Fintype.card (Subgroup.zpowers ζ) :=
      Fintype.card_congr <| by rw [h.zpowers_eq]
    _ = Fintype.card (ZMod n) := Fintype.card_congr e.toEquiv.symm
    _ = n := ZMod.card n

Premises used: Fintype.card_congr, Membership.mem, Fintype.card, Subtype, rootsOfUnity, ZMod, Subgroup.zpowers, AddEquiv.toEquiv, Equiv.symm, ZMod.card
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
inst_2 : NeZero n
h : IsPrimitiveRoot ζ n
obtain : ∀ (ζ_1 : Rˣ) (hζ : (↑ζ_1 : R) = ζ), Fintype.card.{u_4} ↥(rootsOfUnity n R) = n
⊢ Fintype.card.{u_4} ↥(rootsOfUnity n R) = n

Tactic:
obtain ⟨ζ, hζ⟩ := 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
ζ_1 : R
n : ℕ
inst_2 : NeZero n
h : IsPrimitiveRoot ζ_1 n
ζ : Rˣ
hζ : (↑ζ : R) = ζ_1
⊢ IsPrimitiveRoot ζ n

Tactic:
rw [← hζ, IsPrimitiveRoot.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
ζ_1 : R
n : ℕ
inst_2 : NeZero n
h : IsPrimitiveRoot ζ_1 n
ζ : Rˣ
hζ : (↑ζ : R) = ζ_1
h₁ : IsPrimitiveRoot ζ n
⊢ (↑ζ : R) = ζ_1

Tactic:
rw [← hζ, IsPrimitiveRoot.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
ζ_1 : R
n : ℕ
inst_2 : NeZero n
ζ : Rˣ
h : IsPrimitiveRoot ζ n
hζ : (↑ζ : R) = ζ_1
⊢ Fintype.card.{u_4} ↥(rootsOfUnity n R) = n

Tactic:
h.card_rootsOfUnity'

Premises used: IsPrimitiveRoot.card_rootsOfUnity'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ_1 : R
n : ℕ
inst_2 : NeZero n
ζ : Rˣ
h : IsPrimitiveRoot ζ n
hζ : (↑ζ : R) = ζ_1
⊢ Fintype.card.{u_4} ↥(rootsOfUnity n R) = n

Tactic:
exact h.card_rootsOfUnity'

Premises used: IsPrimitiveRoot.card_rootsOfUnity'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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

Tactic:
⟨fun h ↦ ?_, fun ⟨ζ, hζ⟩ ↦ hζ.card_rootsOfUnity⟩

Premises used: Membership.mem, _private.0.card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot.match_1, IsPrimitiveRoot.card_rootsOfUnity, Fintype.card, Subtype, rootsOfUnity, Iff.intro, Eq
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
inst_2 : NeZero n
refine : ∀ (h : Fintype.card.{u_4} ↥(rootsOfUnity n R) = n), ∃ (ζ : R), IsPrimitiveRoot ζ n
⊢ Fintype.card.{u_4} ↥(rootsOfUnity n R) = n ↔ ∃ (ζ : R), IsPrimitiveRoot ζ n

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨ζ, hζ⟩ ↦ hζ.card_rootsOfUnity⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
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
⊢ ∃ (ζ : R), IsPrimitiveRoot ζ n

Tactic:
obtain ⟨⟨ζ, hζ'⟩, hζ⟩ := (rootsOfUnity.isCyclic R n).exists_ofOrder_eq_natCard

Premises used: IsCyclic.exists_ofOrder_eq_natCard
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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)
⊢ 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ζ

Premises used: IsPrimitiveRoot.coe_units_iff, IsPrimitiveRoot.iff_orderOf, IsPrimitiveRoot.coe_submonoidClass_iff, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
h₁ : IsPrimitiveRoot (↑ζ : R) n
⊢ ∃ (ζ : R), IsPrimitiveRoot ζ n

Tactic:
use ζ
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
rw₁ rw₂ : n = n
⊢ Multiset.card.{u_4} (α := R) (nthRoots n 1) = n

Tactic:
rw [card_nthRoots h, if_pos ⟨ζ, h.pow_eq_one⟩]

Premises used: if_pos, IsPrimitiveRoot.card_nthRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
inr : ∀ (hn : n > 0), (nthRoots n a).Nodup
⊢ (nthRoots n a).Nodup

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
ha : a ≠ 0
h : IsPrimitiveRoot ζ 0
⊢ (nthRoots 0 a).Nodup

Tactic:
simp
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
neg : ∀ (h : ∀ (α : R), α ^ n ≠ a), (nthRoots n a).Nodup
⊢ (nthRoots n a).Nodup

Tactic:
by_cases! h : ∃ α, α ^ n = a
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
pos : ∀ (α : R) (hα : α ^ n = a), (nthRoots n a).Nodup
⊢ (nthRoots n a).Nodup

Tactic:
obtain ⟨α, hα⟩ := h
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
neg : ∀ (hα' : ¬α = 0), (nthRoots n a).Nodup
⊢ (nthRoots n a).Nodup

Tactic:
by_cases hα' : α = 0
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hα : a = 0) (hα' : α = 0), a = 0
⊢ a = 0

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

Premises used: eq_comm, LT.lt.ne', zero_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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

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

Premises used: False.elim
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
neg : ∀ x ∈ Multiset.range n, ∀ y ∈ Multiset.range n, ζ ^ x * α = ζ ^ y * α → x = y
⊢ (nthRoots n a).Nodup

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

Premises used: Multiset.nodup_map_iff_inj_on, Multiset.nodup_range, IsPrimitiveRoot.nthRoots_eq
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
⊢ ∀ x ∈ Multiset.range n, ∀ y ∈ Multiset.range n, ζ ^ x * α = ζ ^ y * α → x = y

Tactic:
h.injOn_pow_mul hα'

Premises used: Set.Mem, setOf, Multiset.Mem, IsPrimitiveRoot.injOn_pow_mul, Set.InjOn
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
⊢ ∀ x ∈ Multiset.range n, ∀ y ∈ Multiset.range n, ζ ^ x * α = ζ ^ y * α → x = y

Tactic:
exact h.injOn_pow_mul hα'

Premises used: IsPrimitiveRoot.injOn_pow_mul
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
this : nthRoots n a = 0
⊢ (nthRoots n a).Nodup

Tactic:
simp [this]
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
neg : nthRoots n a = 0
⊢ (nthRoots n a).Nodup

Tactic:
suffices nthRoots n a = 0 by simp [this]
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 = 0

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

Premises used: Multiset.card_eq_zero, Multiset.eq_zero_iff_forall_notMem, Polynomial.mem_nthRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ Multiset.Nodup.{u_4} (α := R) (nthRoots n 1)

Tactic:
h.nthRoots_nodup one_ne_zero

Premises used: one_ne_zero, IsPrimitiveRoot.nthRoots_nodup
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
rw : card.{u_4} (α := R) (Multiset.toFinset (nthRoots n 1)) = n
rw₁ : #{ val := nthRoots n 1, nodup := ⋯ : Finset R } = n
rw₂ : Multiset.card.{u_4} (α := R) (nthRoots n 1) = n
rw₃ rw₄ : n = n
⊢ card.{u_4} (α := R) (nthRootsFinset n 1) = n

Tactic:
rw [nthRootsFinset, ← Multiset.toFinset_eq (nthRoots_one_nodup h), card_mk, h.card_nthRoots_one]

Premises used: IsPrimitiveRoot.nthRoots_one_nodup, Polynomial.nthRootsFinset, Finset.card_mk, IsPrimitiveRoot.card_nthRoots_one, Multiset.toFinset_eq
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
rw : card.{u_4} (α := R) (Multiset.toFinset (nthRoots n 1)) = n
rw₁ : #{ val := nthRoots n 1, nodup := ⋯ : Finset R } = n
rw₂ : Multiset.card.{u_4} (α := R) (nthRoots n 1) = n
rw₃ rw₄ : n = n
⊢ card.{u_4} (α := R) (nthRootsFinset n 1) = n

Tactic:
classical
  rw [nthRootsFinset, ← Multiset.toFinset_eq (nthRoots_one_nodup h), card_mk, h.card_nthRoots_one]

Premises used: Polynomial.nthRootsFinset, Finset.card_mk, IsPrimitiveRoot.card_nthRoots_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
pos : ∀ (h0 : k = 0), #(primitiveRoots k R) = φ k
neg : ∀ (h0 : ¬k = 0), #(primitiveRoots k R) = φ k
⊢ #(primitiveRoots k R) = φ k

Tactic:
by_cases h0 : k = 0
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : k = 0
⊢ #(primitiveRoots k R) = φ k

Tactic:
simp [h0]
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ NeZero k

Tactic:
have : NeZero k := ⟨h0⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
neg : φ k = #(primitiveRoots k R)
⊢ #(primitiveRoots k R) = φ k

Tactic:
symm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
⊢ φ k = #(primitiveRoots k R)

Tactic:
Finset.card_bij (fun i _ ↦ ζ ^ i) ?_ ?_ ?_

Premises used: Finset.card_bij, Nat.totient, HPow.hPow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
neg :
  ∀ (a : ℕ) (ha : a ∈ {a ∈ range k | k.Coprime a}),
    (fun (i : ℕ) (x : i ∈ {a ∈ range k | k.Coprime a}) ↦ ζ ^ i) a ha ∈ primitiveRoots k R
neg₁ :
  ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ {a ∈ range k | k.Coprime a}) (a₂ : ℕ) (ha₂ : a₂ ∈ {a ∈ range k | k.Coprime a}),
    Eq.{u_4 + 1} (α := R) ((fun (i : ℕ) (x : i ∈ {a ∈ range k | k.Coprime a}) ↦ ζ ^ i) a₁ ha₁)
        ((fun (i : ℕ) (x : i ∈ {a ∈ range k | k.Coprime a}) ↦ ζ ^ i) a₂ ha₂) →
      a₁ = a₂
neg₂ :
  ∀ b ∈ primitiveRoots k R,
    ∃ (a : ℕ) (ha : a ∈ {a ∈ range k | k.Coprime a}),
      (fun (i : ℕ) (x : i ∈ {a ∈ range k | k.Coprime a}) ↦ ζ ^ i) a ha = b
⊢ φ k = #(primitiveRoots k R)

Tactic:
refine Finset.card_bij (fun i _ ↦ ζ ^ i) ?_ ?_ ?_

Premises used: Finset.card_bij, HPow.hPow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
neg : ∀ a < k, k.Coprime a → ζ ^ a ∈ primitiveRoots k R
⊢ ∀ (a : ℕ) (ha : a ∈ {a ∈ range k | k.Coprime a}),
    (fun (i : ℕ) (x : i ∈ {a ∈ range k | k.Coprime a}) ↦ ζ ^ i) a ha ∈ primitiveRoots k R

Tactic:
simp only [and_imp, mem_filter, mem_range]

Premises used: and_imp, Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
i : ℕ
hi : k.Coprime i
neg : IsPrimitiveRoot (ζ ^ i) k
⊢ ζ ^ i ∈ primitiveRoots k R

Tactic:
rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0)]

Premises used: Nat.pos_of_ne_zero, mem_primitiveRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
i : ℕ
hi : k.Coprime i
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
h.pow_of_coprime i hi.symm

Premises used: Nat.Coprime.symm, IsPrimitiveRoot.pow_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
i : ℕ
hi : k.Coprime i
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
exact h.pow_of_coprime i hi.symm

Premises used: Nat.Coprime.symm, IsPrimitiveRoot.pow_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
neg : ∀ a₁ < k, k.Coprime a₁ → ∀ a₂ < k, k.Coprime a₂ → ζ ^ a₁ = ζ ^ a₂ → a₁ = a₂
⊢ ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ {a ∈ range k | k.Coprime a}) (a₂ : ℕ) (ha₂ : a₂ ∈ {a ∈ range k | k.Coprime a}),
    Eq.{u_4 + 1} (α := R) ((fun (i : ℕ) (x : i ∈ {a ∈ range k | k.Coprime a}) ↦ ζ ^ i) a₁ ha₁)
        ((fun (i : ℕ) (x : i ∈ {a ∈ range k | k.Coprime a}) ↦ ζ ^ i) a₂ ha₂) →
      a₁ = a₂

Tactic:
simp only [and_imp, mem_filter, mem_range]

Premises used: and_imp, Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
i : ℕ
hi : i < k
j : ℕ
hj : j < k
H : ζ ^ i = ζ ^ j
⊢ i = j

Tactic:
h.pow_inj hi hj H

Premises used: IsPrimitiveRoot.pow_inj
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
i : ℕ
hi : i < k
j : ℕ
hj : j < k
H : ζ ^ i = ζ ^ j
⊢ i = j

Tactic:
exact h.pow_inj hi hj H

Premises used: IsPrimitiveRoot.pow_inj
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
neg : ∀ b ∈ primitiveRoots k R, ∃ (a : ℕ), (a < k ∧ k.Coprime a) ∧ ζ ^ a = b
⊢ ∀ b ∈ primitiveRoots k R,
    ∃ (a : ℕ) (ha : a ∈ {a ∈ range k | k.Coprime a}),
      (fun (i : ℕ) (x : i ∈ {a ∈ range k | k.Coprime a}) ↦ ζ ^ i) a ha = b

Tactic:
simp only [exists_prop, mem_filter, mem_range]

Premises used: Finset.mem_range, exists_prop, Finset.mem_filter
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
hξ : ξ ∈ primitiveRoots k R
⊢ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ

Tactic:
rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0), h.isPrimitiveRoot_iff] at hξ

Premises used: Nat.pos_of_ne_zero, IsPrimitiveRoot.isPrimitiveRoot_iff, mem_primitiveRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
hξ : ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
neg : ∀ (i : ℕ) (hin : i < k) (hi : i.Coprime k) (H : ζ ^ i = ξ), ∃ (a : ℕ), (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ
⊢ ∃ (a : ℕ), (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Tactic:
rcases hξ with ⟨i, hin, hi, H⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
i : ℕ
hin : i < k
hi : i.Coprime k
H : ζ ^ i = ξ
⊢ ∃ (a : ℕ), (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Tactic:
⟨i, ⟨hin, hi.symm⟩, H⟩

Premises used: Nat.Coprime.symm, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
i : ℕ
hin : i < k
hi : i.Coprime k
H : ζ ^ i = ξ
⊢ ∃ (a : ℕ), (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Tactic:
exact ⟨i, ⟨hin, hi.symm⟩, H⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing R
ζ : Rˣ
h_1 : IsPrimitiveRoot ζ k
inst_4 : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
by_contra! : ∀ (h : n ≤ 0), False
⊢ 0 < n

Tactic:
by_contra! h
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing R
ζ : Rˣ
h_1 : IsPrimitiveRoot ζ k
inst_4 : IsDomain R
a b n : ℕ
h_2 : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
h : n ≤ 0
mk : ∀ val ∈ primitiveRoots n R, False
⊢ False

Tactic:
cases x
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing R
ζ : Rˣ
h_1 : IsPrimitiveRoot ζ k
inst_4 : IsDomain R
a b n : ℕ
h_2 : a * b ≡ 1 [MOD n]
h : n ≤ 0
val : R
property : val ∈ primitiveRoots n R
⊢ False

Tactic:
simp_all