awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₁ : A
hη₁ : η₁ ∈ (↑(nthRootsFinset p 1) : Set A)
η₂ : A
hη₂ : η₂ ∈ (↑(nthRootsFinset p 1) : Set A)
e : η₁ ≠ η₂
this : NeZero p
obtain :
  ∀ (i : ℕ) (hi : i < p) (hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)) (e : ζ ^ i ≠ η₂),
    Associated (ζ - 1) (ζ ^ i - η₂)
⊢ Associated (ζ - 1) (η₁ - η₂)

Tactic:
obtain ⟨i, hi, rfl⟩ :=
    hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos 1).1 hη₁)

Premises used: Nat.Prime.pos, Iff.mp, IsPrimitiveRoot.eq_pow_of_pow_eq_one, OfNat.ofNat, rfl, Polynomial.mem_nthRootsFinset
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₂ : A
hη₂ : η₂ ∈ (↑(nthRootsFinset p 1) : Set A)
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)
e : ζ ^ i ≠ η₂
obtain :
  ∀ (j : ℕ) (hj : j < p) (hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)) (e : ζ ^ i ≠ ζ ^ j),
    Associated (ζ - 1) (ζ ^ i - ζ ^ j)
⊢ Associated (ζ - 1) (ζ ^ i - η₂)

Tactic:
obtain ⟨j, hj, rfl⟩ :=
    hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos 1).1 hη₂)

Premises used: Nat.Prime.pos, Iff.mp, IsPrimitiveRoot.eq_pow_of_pow_eq_one, OfNat.ofNat, rfl, Polynomial.mem_nthRootsFinset
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)
e : ζ ^ i ≠ ζ ^ j
inr :
  ∀
    (this :
      ∀ {p : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_2 : IsDomain A] (hζ : IsPrimitiveRoot ζ p)
        (hp : Nat.Prime p) (this : NeZero p) (i : ℕ) (hi : i < p) (hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A))
        (j : ℕ) (hj : j < p) (hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)) (e : ζ ^ i ≠ ζ ^ j) (hij : j ≤ i),
        Associated (ζ - 1) (ζ ^ i - ζ ^ j))
    (hij : ¬j ≤ i), Associated (ζ - 1) (ζ ^ i - ζ ^ j)
wlog :
  ∀ {p : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_2 : IsDomain A] (hζ : IsPrimitiveRoot ζ p)
    (hp : Nat.Prime p) (this : NeZero p) (i : ℕ) (hi : i < p) (hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)) (j : ℕ)
    (hj : j < p) (hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)) (e : ζ ^ i ≠ ζ ^ j) (hij : j ≤ i),
    Associated (ζ - 1) (ζ ^ i - ζ ^ j)
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)

Tactic:
wlog hij : j ≤ i
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this_1 : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)
e : ζ ^ i ≠ ζ ^ j
this :
  ∀ {p : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_2 : IsDomain A] (hζ : IsPrimitiveRoot ζ p)
    (hp : Nat.Prime p) (this : NeZero p) (i : ℕ) (hi : i < p) (hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)) (j : ℕ)
    (hj : j < p) (hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)) (e : ζ ^ i ≠ ζ ^ j) (hij : j ≤ i),
    Associated (ζ - 1) (ζ ^ i - ζ ^ j)
hij : ¬j ≤ i
⊢ i ≤ j

Tactic:
lia
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p : ℕ
A : Type u_1
ζ : A
inst : CommRing A
inst_1 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this_1 : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)
e : ζ ^ i ≠ ζ ^ j
this :
  ∀ {p : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_2 : IsDomain A] (hζ : IsPrimitiveRoot ζ p)
    (hp : Nat.Prime p) (this : NeZero p) (i : ℕ) (hi : i < p) (hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)) (j : ℕ)
    (hj : j < p) (hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)) (e : ζ ^ i ≠ ζ ^ j) (hij : j ≤ i),
    Associated (ζ - 1) (ζ ^ i - ζ ^ j)
hij : ¬j ≤ i
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)

Tactic:
simpa using (this hζ ‹_› ‹_› _ hj ‹_› _ hi ‹_› e.symm (by lia)).neg_right

Premises used: Associated.neg_right, Ne.symm
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p_1 : ℕ
A_1 : Type u_1
ζ_1 : A_1
inst : CommRing A_1
inst_1 : IsDomain A_1
p : ℕ
A : Type u_1
ζ : A
inst_2 : CommRing A
inst_3 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
⊢ i - j ≠ 0

Tactic:
grind
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p_1 : ℕ
A_1 : Type u_1
ζ_1 : A_1
inst : CommRing A_1
inst_1 : IsDomain A_1
p : ℕ
A : Type u_1
ζ : A
inst_2 : CommRing A
inst_3 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
⊢ i - j < p

Tactic:
grind
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p_1 : ℕ
A_1 : Type u_1
ζ_1 : A_1
inst : CommRing A_1
inst_1 : IsDomain A_1
p : ℕ
A : Type u_1
ζ : A
inst_2 : CommRing A
inst_3 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
⊢ (i - j).Coprime p

Tactic:
have H : (i - j).Coprime p := (coprime_of_lt_prime (by grind) (by grind) hp).symm
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p_1 : ℕ
A_1 : Type u_1
ζ_1 : A_1
inst : CommRing A_1
inst_1 : IsDomain A_1
p : ℕ
A : Type u_1
ζ : A
inst_2 : CommRing A
inst_3 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
H : (i - j).Coprime p
obtain : ∀ (u : Aˣ) (h : (ζ - 1) * (↑u : A) = ζ ^ (j + (i - j)) - ζ ^ j), Associated (ζ - 1) (ζ ^ i - ζ ^ j)
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)

Tactic:
obtain ⟨u, h⟩ := hζ.associated_pow_add_sub_sub_one hp.two_le j H

Premises used: IsPrimitiveRoot.associated_pow_add_sub_sub_one, Nat.Prime.two_le
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p_1 : ℕ
A_1 : Type u_1
ζ_1 : A_1
inst : CommRing A_1
inst_1 : IsDomain A_1
p : ℕ
A : Type u_1
ζ : A
inst_2 : CommRing A
inst_3 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
H : (i - j).Coprime p
u : Aˣ
h : (ζ - 1) * (↑u : A) = ζ ^ (j + (i - j)) - ζ ^ j
⊢ (ζ - 1) * (↑u : A) = ζ ^ i - ζ ^ j

Tactic:
simp only [hij, add_tsub_cancel_of_le] at h

Premises used: add_tsub_cancel_of_le
-- Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
Goal:
p_1 : ℕ
A_1 : Type u_1
ζ_1 : A_1
inst : CommRing A_1
inst_1 : IsDomain A_1
p : ℕ
A : Type u_1
ζ : A
inst_2 : CommRing A
inst_3 : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ (↑(nthRootsFinset p 1) : Set A)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ (↑(nthRootsFinset p 1) : Set A)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
H : (i - j).Coprime p
u : Aˣ
h : (ζ - 1) * (↑u : A) = ζ ^ i - ζ ^ j
rw : Associated (ζ - 1) ((ζ - 1) * (↑u : A))
rw₁ rw₂ : Associated (ζ - 1) (ζ - 1)
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)

Tactic:
rw [← h, associated_mul_unit_right_iff]

Premises used: associated_mul_unit_right_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : HasEnoughRootsOfUnity M n
⊢ ∃ (ζ : M), IsPrimitiveRoot ζ n

Tactic:
HasEnoughRootsOfUnity.prim

Premises used: HasEnoughRootsOfUnity.prim
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : HasEnoughRootsOfUnity M n
⊢ IsCyclic.{u_1} ↥(rootsOfUnity n M)

Tactic:
HasEnoughRootsOfUnity.cyc

Premises used: HasEnoughRootsOfUnity.cyc
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
⊢ IsCyclic.{u_1} ↥(rootsOfUnity n M)

Tactic:
have := rootsOfUnity_isCyclic M n
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
this : IsCyclic.{u_1} ↥(rootsOfUnity n M)
obtain :
  ∀ (g : ↥(rootsOfUnity n M))
    (hg : ∀ (x : ↥(rootsOfUnity n M)), Membership.mem (γ := Subgroup ↥(rootsOfUnity n M)) (Subgroup.zpowers g) x),
    Finite.{u_1 + 1} ↥(rootsOfUnity n M)
⊢ Finite.{u_1 + 1} ↥(rootsOfUnity n M)

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := rootsOfUnity n M)

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
this : IsCyclic.{u_1} ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), Membership.mem (γ := Subgroup ↥(rootsOfUnity n M)) (Subgroup.zpowers g) x
⊢ g ^ n = 1

Tactic:
have hg' : g ^ n = 1 := OneMemClass.coe_eq_one.mp g.prop
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
this : IsCyclic.{u_1} ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), Membership.mem (γ := Subgroup ↥(rootsOfUnity n M)) (Subgroup.zpowers g) x
hg' : g ^ n = 1
f : (j : ZMod n) → ↥(rootsOfUnity n M) := fun (j : ZMod n) ↦ HPow.hPow (β := ℤ) g (↑j.val : ℤ)
⊢ Finite.{u_1 + 1} ↥(rootsOfUnity n M)

Tactic:
Finite.of_surjective f fun x ↦ ?_

Premises used: Finite.of_surjective
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
this : IsCyclic.{u_1} ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), Membership.mem (γ := Subgroup ↥(rootsOfUnity n M)) (Subgroup.zpowers g) x
hg' : g ^ n = 1
f : (j : ZMod n) → ↥(rootsOfUnity n M) := fun (j : ZMod n) ↦ HPow.hPow (β := ℤ) g (↑j.val : ℤ)
refine : ∀ (x : ↥(rootsOfUnity n M)), ∃ (a : ZMod n), f a = x
⊢ Finite.{u_1 + 1} ↥(rootsOfUnity n M)

Tactic:
refine Finite.of_surjective f fun x ↦ ?_

Premises used: Finite.of_surjective
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
this : IsCyclic.{u_1} ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), Membership.mem (γ := Subgroup ↥(rootsOfUnity n M)) (Subgroup.zpowers g) x
hg' : g ^ n = 1
f : (j : ZMod n) → ↥(rootsOfUnity n M) := fun (j : ZMod n) ↦ HPow.hPow (β := ℤ) g (↑j.val : ℤ)
x : ↥(rootsOfUnity n M)
obtain : ∀ (k : ℤ) (hk : g ^ k = x), ∃ (a : ZMod n), f a = x
⊢ ∃ (a : ZMod n), f a = x

Tactic:
obtain ⟨k, hk⟩ := Subgroup.mem_zpowers_iff.mp <| hg x

Premises used: Iff.mp, Subgroup.mem_zpowers_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
this : IsCyclic.{u_1} ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), Membership.mem (γ := Subgroup ↥(rootsOfUnity n M)) (Subgroup.zpowers g) x
hg' : g ^ n = 1
f : (j : ZMod n) → ↥(rootsOfUnity n M) := fun (j : ZMod n) ↦ HPow.hPow (β := ℤ) g (↑j.val : ℤ)
x : ↥(rootsOfUnity n M)
k : ℤ
hk : g ^ k = x
⊢ ∃ (a : ZMod n), f a = x

Tactic:
⟨k, ?_⟩

Premises used: Int.cast, Exists.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
this : IsCyclic.{u_1} ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), Membership.mem (γ := Subgroup ↥(rootsOfUnity n M)) (Subgroup.zpowers g) x
hg' : g ^ n = 1
f : (j : ZMod n) → ↥(rootsOfUnity n M) := fun (j : ZMod n) ↦ HPow.hPow (β := ℤ) g (↑j.val : ℤ)
x : ↥(rootsOfUnity n M)
k : ℤ
hk : g ^ k = x
refine : f (↑k : ZMod n) = x
⊢ ∃ (a : ZMod n), f a = x

Tactic:
refine ⟨k, ?_⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
this : IsCyclic.{u_1} ↥(rootsOfUnity n M)
g : ↥(rootsOfUnity n M)
hg : ∀ (x : ↥(rootsOfUnity n M)), Membership.mem (γ := Subgroup ↥(rootsOfUnity n M)) (Subgroup.zpowers g) x
hg' : g ^ n = 1
f : (j : ZMod n) → ↥(rootsOfUnity n M) := fun (j : ZMod n) ↦ HPow.hPow (β := ℤ) g (↑j.val : ℤ)
x : ↥(rootsOfUnity n M)
k : ℤ
hk : g ^ k = x
⊢ f (↑k : ZMod n) = x

Tactic:
simpa only [ZMod.natCast_val, ← hk, f, ZMod.coe_intCast] using (zpow_eq_zpow_emod' k hg').symm

Premises used: ZMod.natCast_val, zpow_eq_zpow_emod', ZMod.coe_intCast, Eq.symm
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
obtain : ∀ (ζ : M) (h : IsPrimitiveRoot ζ n), Nat.card.{u_1} ↥(rootsOfUnity n M) = n
⊢ Nat.card.{u_1} ↥(rootsOfUnity n M) = n

Tactic:
obtain ⟨ζ, h⟩ := exists_primitiveRoot M n

Premises used: HasEnoughRootsOfUnity.exists_primitiveRoot
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
rw : Monoid.exponent.{u_1} ↥(rootsOfUnity n M) = n
⊢ Nat.card.{u_1} ↥(rootsOfUnity n M) = n

Tactic:
rw [← IsCyclic.exponent_eq_card]

Premises used: IsCyclic.exponent_eq_card
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ Monoid.exponent.{u_1} ↥(rootsOfUnity n M) = n

Tactic:
dvd_antisymm ?_ ?_

Premises used: dvd_antisymm
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
refine_1 : Monoid.exponent.{u_1} ↥(rootsOfUnity n M) ∣ n
refine_2 : n ∣ Monoid.exponent.{u_1} ↥(rootsOfUnity n M)
⊢ Monoid.exponent.{u_1} ↥(rootsOfUnity n M) = n

Tactic:
refine dvd_antisymm ?_ ?_

Premises used: dvd_antisymm
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ Monoid.exponent.{u_1} ↥(rootsOfUnity n M) ∣ n

Tactic:
Monoid.exponent_dvd_of_forall_pow_eq_one fun g ↦ OneMemClass.coe_eq_one.mp g.prop

Premises used: Monoid.exponent_dvd_of_forall_pow_eq_one, OneMemClass.coe_eq_one, Subtype.prop, Iff.mp
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ Monoid.exponent.{u_1} ↥(rootsOfUnity n M) ∣ n

Tactic:
exact Monoid.exponent_dvd_of_forall_pow_eq_one fun g ↦ OneMemClass.coe_eq_one.mp g.prop

Premises used: Monoid.exponent_dvd_of_forall_pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
refine_2 : orderOf ζ ∣ Monoid.exponent.{u_1} ↥(rootsOfUnity n M)
⊢ n ∣ Monoid.exponent.{u_1} ↥(rootsOfUnity n M)

Tactic:
nth_rewrite 1 [h.eq_orderOf]

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
refine_2 : orderOf ⋯.unit ∣ Monoid.exponent.{u_1} ↥(rootsOfUnity n M)
⊢ orderOf ζ ∣ Monoid.exponent.{u_1} ↥(rootsOfUnity n M)

Tactic:
rw [← (h.isUnit NeZero.out).unit_spec, orderOf_units]

Premises used: orderOf_units, IsPrimitiveRoot.isUnit, NeZero.out, IsUnit.unit_spec
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
refine_2 : orderOf ⋯.unit ∣ Monoid.exponent.{u_1} ↥(rootsOfUnity n M)
refine_2₁ : Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) ⋯.unit
⊢ orderOf ⋯.unit ∣ Monoid.exponent.{u_1} ↥(rootsOfUnity n M)

Tactic:
let ζ' : rootsOfUnity n M := ⟨(h.isUnit NeZero.out).unit, ?_⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) :=
  Subtype.mk (p := fun (x : Mˣ) ↦ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) x) ⋯.unit ⋯
refine_2 :
  orderOf (Subtype.mk (p := fun (x : Mˣ) ↦ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) x) ⋯.unit ⋯) ∣
    Monoid.exponent.{u_1} ↥(rootsOfUnity n M)
refine_2₁ : Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) ⋯.unit
rw : Subgroup Mˣ
⊢ orderOf ⋯.unit ∣ Monoid.exponent.{u_1} ↥(rootsOfUnity n M)

Tactic:
rw [← Subgroup.orderOf_mk]

Premises used: Subgroup.orderOf_mk
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) :=
  Subtype.mk (p := fun (x : Mˣ) ↦ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) x) ⋯.unit ⋯
⊢ orderOf (Subtype.mk (p := fun (x : Mˣ) ↦ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) x) ⋯.unit ⋯) ∣
    Monoid.exponent.{u_1} ↥(rootsOfUnity n M)

Tactic:
Monoid.order_dvd_exponent ζ'

Premises used: Monoid.order_dvd_exponent
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
refine_2 : (↑(⋯.unit ^ n) : M) = (↑1 : M)
refine_2₁ : (↑⋯.unit : M) ^ n = (↑1 : M)
refine_2₂ : ζ ^ n = (↑1 : M)
refine_2₃ : Eq.{u_1 + 1} (α := M) 1 (↑1 : M)
refine_2₄ refine_2₅ : Eq.{u_1 + 1} (α := M) 1 1
⊢ ⋯.unit ^ n = 1

Tactic:
rw [← Units.val_inj, Units.val_pow_eq_pow_val, IsUnit.unit_spec, h.pow_eq_one, Units.val_one]

Premises used: Units.val_inj, Units.val_one, Units.val_pow_eq_pow_val, IsUnit.unit_spec, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
n : ℕ
inst : NeZero n
M : Type u_1
N : Type u_2
inst_1 : CommMonoid M
inst_2 : CommMonoid N
hm : HasEnoughRootsOfUnity M n
e : MulEquiv.{u_1, u_2} ↥(rootsOfUnity n M) ↥(rootsOfUnity n N)
obtain : ∀ (m : M) (hm : IsPrimitiveRoot m n), ∃ (m : N), IsPrimitiveRoot m n
⊢ ∃ (m : N), IsPrimitiveRoot m n

Tactic:
obtain ⟨m, hm⟩ := hm.prim

Premises used: HasEnoughRootsOfUnity.prim
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
n : ℕ
inst : NeZero n
M : Type u_1
N : Type u_2
inst_1 : CommMonoid M
inst_2 : CommMonoid N
hm_1 : HasEnoughRootsOfUnity M n
e : MulEquiv.{u_1, u_2} ↥(rootsOfUnity n M) ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
h :
  IsPrimitiveRoot.{u_2} (M := N)
    (↑(↑((e : (a : ↥(rootsOfUnity n M)) → ↥(rootsOfUnity n N)) hm.toRootsOfUnity) : Nˣ) : N) n
⊢ ∃ (m : N), IsPrimitiveRoot m n

Tactic:
use (e hm.toRootsOfUnity).val.val

Premises used: Units.val, IsPrimitiveRoot.toRootsOfUnity, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
n : ℕ
inst : NeZero n
M : Type u_1
N : Type u_2
inst_1 : CommMonoid M
inst_2 : CommMonoid N
hm_1 : HasEnoughRootsOfUnity M n
e : MulEquiv.{u_1, u_2} ↥(rootsOfUnity n M) ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
h :
  IsPrimitiveRoot.{u_2} (M := ↥(rootsOfUnity n N))
    ((e : (a : ↥(rootsOfUnity n M)) → ↥(rootsOfUnity n N)) hm.toRootsOfUnity : ↥(rootsOfUnity n N)) n
⊢ IsPrimitiveRoot.{u_2} (M := N)
    (↑(↑((e : (a : ↥(rootsOfUnity n M)) → ↥(rootsOfUnity n N)) hm.toRootsOfUnity) : Nˣ) : N) n

Tactic:
rw [IsPrimitiveRoot.coe_units_iff, IsPrimitiveRoot.coe_submonoidClass_iff]

Premises used: IsPrimitiveRoot.coe_units_iff, IsPrimitiveRoot.coe_submonoidClass_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
n : ℕ
inst : NeZero n
M : Type u_1
N : Type u_2
inst_1 : CommMonoid M
inst_2 : CommMonoid N
hm_1 : HasEnoughRootsOfUnity M n
e : MulEquiv.{u_1, u_2} ↥(rootsOfUnity n M) ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
⊢ IsPrimitiveRoot.{u_2} (M := ↥(rootsOfUnity n N))
    ((e : (a : ↥(rootsOfUnity n M)) → ↥(rootsOfUnity n N)) hm.toRootsOfUnity : ↥(rootsOfUnity n N)) n

Tactic:
.map_of_injective ?_ e.injective

Premises used: IsPrimitiveRoot.map_of_injective, MulEquiv.injective
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
n : ℕ
inst : NeZero n
M : Type u_1
N : Type u_2
inst_1 : CommMonoid M
inst_2 : CommMonoid N
hm_1 : HasEnoughRootsOfUnity M n
e : MulEquiv.{u_1, u_2} ↥(rootsOfUnity n M) ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
h : IsPrimitiveRoot hm.toRootsOfUnity n
⊢ IsPrimitiveRoot.{u_2} (M := ↥(rootsOfUnity n N))
    ((e : (a : ↥(rootsOfUnity n M)) → ↥(rootsOfUnity n N)) hm.toRootsOfUnity : ↥(rootsOfUnity n N)) n

Tactic:
refine .map_of_injective ?_ e.injective
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
n : ℕ
inst : NeZero n
M : Type u_1
N : Type u_2
inst_1 : CommMonoid M
inst_2 : CommMonoid N
hm_1 : HasEnoughRootsOfUnity M n
e : MulEquiv.{u_1, u_2} ↥(rootsOfUnity n M) ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
h : IsPrimitiveRoot (↑hm.toRootsOfUnity : Mˣ) n
h₁ h₂ h₃ h₄ : IsPrimitiveRoot (↑(↑hm.toRootsOfUnity : Mˣ) : M) n
⊢ IsPrimitiveRoot hm.toRootsOfUnity n

Tactic:
rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, ← IsPrimitiveRoot.coe_units_iff]

Premises used: IsPrimitiveRoot.coe_units_iff, IsPrimitiveRoot.coe_submonoidClass_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : IsCyclic G
inst_3 : CommMonoid M
inst_4 : HasEnoughRootsOfUnity M (Nat.card G)
⊢ NeZero (Nat.card G)

Tactic:
have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : IsCyclic G
inst_3 : CommMonoid M
inst_4 : HasEnoughRootsOfUnity M (Nat.card G)
this : NeZero (Nat.card G)
⊢ Nat.card.{u_2} ↥(rootsOfUnity (Nat.card G) M) = Nat.card G

Tactic:
have hord := HasEnoughRootsOfUnity.natCard_rootsOfUnity M (Nat.card G)
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : IsCyclic G
inst_3 : CommMonoid M
inst_4 : HasEnoughRootsOfUnity M (Nat.card G)
this : NeZero (Nat.card G)
hord : Nat.card.{u_2} ↥(rootsOfUnity (Nat.card G) M) = Nat.card G
e : MonoidHom.{u_1, u_2} G Mˣ ≃* ↥(rootsOfUnity (Nat.card G) Mˣ) := Nonempty.some ⋯
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)

Tactic:
⟨e.trans (rootsOfUnityUnitsMulEquiv M (Nat.card G)) |>.trans (mulEquivOfCyclicCardEq hord)⟩

Premises used: mulEquivOfCyclicCardEq, MulEquiv.trans, rootsOfUnityUnitsMulEquiv, Nat.card, Nonempty.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : IsCyclic G
inst_3 : CommMonoid M
inst_4 : HasEnoughRootsOfUnity M (Nat.card G)
this : NeZero (Nat.card G)
hord : Nat.card.{u_2} ↥(rootsOfUnity (Nat.card G) M) = Nat.card G
e : MonoidHom.{u_1, u_2} G Mˣ ≃* ↥(rootsOfUnity (Nat.card G) Mˣ) := Nonempty.some ⋯
⊢ Nonempty (MonoidHom.{u_1, u_2} G Mˣ ≃* G)

Tactic:
exact ⟨e.trans (rootsOfUnityUnitsMulEquiv M (Nat.card G)) |>.trans (mulEquivOfCyclicCardEq hord)⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Goal:
M : Type u_1
inst : CommMonoid M
⊢ IsPrimitiveRoot.{u_1} (M := M) 1 1

Tactic:
simp