awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
k : ℕ
M : Type u_7
B : Type u_8
inst : CommMonoid M
inst_1 : SetLike B M
inst_2 : SubmonoidClass B M
N : B
ζ : ↥N
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l) ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l
⊢ ((↑ζ : M) ^ k = 1 ∧ ∀ (l : ℕ), (↑ζ : M) ^ l = 1 → k ∣ l) ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ IsPrimitiveRoot (↑ζ : M) k ↔ IsPrimitiveRoot ζ k

Tactic:
simp only [iff_def, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one]

Premises used: Units.ext_iff, IsPrimitiveRoot.iff_def, Units.val_one, Units.val_pow_eq_pow_val
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
n : ℕ
hn : n ≠ 0
hζ : IsPrimitiveRoot ζ n
⊢ IsPrimitiveRoot ⋯.unit n

Tactic:
coe_units_iff.mp hζ

Premises used: IsPrimitiveRoot.coe_units_iff, Iff.mp
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
ζ : G
n : ℕ
hn : n ≠ 0
hζ : IsPrimitiveRoot ζ n
⊢ IsPrimitiveRoot ⋯.unit' n

Tactic:
coe_units_iff.mp hζ

Premises used: IsPrimitiveRoot.coe_units_iff, Iff.mp
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
pos : ∀ (h0 : k = 0), IsPrimitiveRoot (ζ ^ i) k
neg : ∀ (h0 : ¬k = 0), IsPrimitiveRoot (ζ ^ i) k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
by_cases h0 : k = 0
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
h0 : k = 0
pos : ∀ (h : IsPrimitiveRoot ζ 0) (hi : i.Coprime 0), IsPrimitiveRoot (ζ ^ i) 0
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
subst k
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
i : ℕ
h : IsPrimitiveRoot ζ 0
hi : i.Coprime 0
⊢ IsPrimitiveRoot (ζ ^ i) 0

Tactic:
simp_all only [pow_one, Nat.coprime_zero_right]

Premises used: Nat.coprime_zero_right, pow_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
neg : ∀ (ζ : Mˣ) (h : IsPrimitiveRoot (↑ζ : M) k), IsPrimitiveRoot ((↑ζ : M) ^ i) k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
rcases h.isUnit h0 with ⟨ζ, rfl⟩

Premises used: IsPrimitiveRoot.isUnit, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ : M) k
neg : IsPrimitiveRoot (↑(ζ ^ i) : M) k
⊢ IsPrimitiveRoot ((↑ζ : M) ^ i) k

Tactic:
rw [← Units.val_pow_eq_pow_val]

Premises used: Units.val_pow_eq_pow_val
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ : M) k
neg : ∀ (h : IsPrimitiveRoot ζ k), IsPrimitiveRoot (ζ ^ i) k
⊢ IsPrimitiveRoot (↑(ζ ^ i) : M) k

Tactic:
rw [coe_units_iff] at h ⊢

Premises used: IsPrimitiveRoot.coe_units_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
rw : ζ ^ (k * i) = 1
rw₁ : (ζ ^ k) ^ i = 1
rw₂ : HPow.hPow (α := Mˣ) 1 i = 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := Mˣ) 1 1
⊢ (ζ ^ i) ^ k = 1

Tactic:
rw [← pow_mul', pow_mul, h.pow_eq_one, one_pow]

Premises used: one_pow, pow_mul, pow_mul', IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
neg : ∀ (l : ℕ) (hl : (ζ ^ i) ^ l = 1), ζ ^ l = 1
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
refine
    { pow_eq_one := by rw [← pow_mul', pow_mul, h.pow_eq_one, one_pow]
      dvd_of_pow_eq_one := fun l hl ↦ h.dvd_of_pow_eq_one l ?_ }
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
neg : ζ ^ (HMul.hMul (α := ℤ) (↑i : ℤ) (↑l : ℤ) * i.gcdA k) * (ζ ^ ((↑k : ℤ) * i.gcdB k)) ^ l = 1
⊢ ζ ^ l = 1

Tactic:
rw [← pow_one ζ, ← zpow_natCast ζ, ← hi.gcd_eq_one, Nat.gcd_eq_gcd_ab, zpow_add, mul_pow,
    ← zpow_natCast, ← zpow_mul, mul_right_comm]

Premises used: zpow_natCast, zpow_add, zpow_mul, Nat.Coprime.gcd_eq_one, mul_right_comm, pow_one, mul_pow, Nat.gcd_eq_gcd_ab
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ (HMul.hMul (α := ℤ) (↑i : ℤ) (↑l : ℤ) * i.gcdA k) * (ζ ^ ((↑k : ℤ) * i.gcdB k)) ^ l = 1

Tactic:
simp only [zpow_mul, hl, h.pow_eq_one, one_zpow, one_pow, one_mul, zpow_natCast]

Premises used: zpow_natCast, one_pow, zpow_mul, one_zpow, IsPrimitiveRoot.pow_eq_one, one_mul
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hprime : Nat.Prime p
hdiv : ¬p ∣ k
⊢ IsPrimitiveRoot (ζ ^ p) k

Tactic:
h.pow_of_coprime p (hprime.coprime_iff_not_dvd.2 hdiv)

Premises used: Iff.mpr, IsPrimitiveRoot.pow_of_coprime, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
⊢ IsPrimitiveRoot (ζ ^ i) k ↔ i.Coprime k

Tactic:
⟨fun hi ↦ ?_, h.pow_of_coprime i⟩

Premises used: IsPrimitiveRoot.pow_of_coprime, Iff.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
refine : ∀ (hi : IsPrimitiveRoot (ζ ^ i) k), i.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i) k ↔ i.Coprime k

Tactic:
refine ⟨fun hi ↦ ?_, h.pow_of_coprime i⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
obtain : ∀ (a : ℕ) (ha : i = i.gcd k * a), i.Coprime k
⊢ i.Coprime k

Tactic:
obtain ⟨a, ha⟩ := i.gcd_dvd_left k

Premises used: Nat.gcd_dvd_left
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = i.gcd k * a
obtain : ∀ (b : ℕ) (hb : k = i.gcd k * b), i.Coprime k
⊢ i.Coprime k

Tactic:
obtain ⟨b, hb⟩ := i.gcd_dvd_right k

Premises used: Nat.gcd_dvd_right
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = i.gcd k * a
b : ℕ
hb : k = i.gcd k * b
this : b = k
rwa : ∀ (hb : k = i.gcd k * k) (this : b = k), i.Coprime k
rwa₁ : ∀ (hb : i.gcd k * k = k) (this : b = k), i.Coprime k
rwa₂ : ∀ (hb : i.gcd k = 1) (this : b = k), i.Coprime k
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hb : i.Coprime k) (this : b = k), i.Coprime k
⊢ i.Coprime k

Tactic:
rwa [this, eq_comm, Nat.mul_eq_right h0.ne', ← Nat.coprime_iff_gcd_eq_one] at hb

Premises used: Nat.mul_eq_right, eq_comm, LT.lt.ne', Nat.coprime_iff_gcd_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = i.gcd k * a
b : ℕ
hb : k = i.gcd k * b
suffices : b = k
⊢ i.Coprime k

Tactic:
suffices b = k by
    rwa [this, eq_comm, Nat.mul_eq_right h0.ne', ← Nat.coprime_iff_gcd_eq_one] at hb
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = i.gcd k * a
b : ℕ
hb : k = i.gcd k * b
rw : ∀ (hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k) (ha : i = i.gcd k * a) (b : ℕ) (hb : k = i.gcd k * b), b = k
⊢ b = k

Tactic:
rw [ha] at hi
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = b * i.gcd k
apply : (ζ ^ (i.gcd k * a)) ^ b = 1
⊢ b = k

Tactic:
apply Nat.dvd_antisymm ⟨i.gcd k, hb⟩ (hi.dvd_of_pow_eq_one b _)

Premises used: Nat.gcd, Exists.intro, IsPrimitiveRoot.dvd_of_pow_eq_one, Nat.dvd_antisymm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = b * i.gcd k
rw : ζ ^ (b * (i.gcd k * a)) = 1
rw₁ : ζ ^ (b * i.gcd k * a) = 1
rw₂ : ζ ^ (k * a) = 1
rw₃ : (ζ ^ k) ^ a = 1
rw₄ : HPow.hPow (α := M) 1 a = 1
rw₅ rw₆ : Eq.{u_1 + 1} (α := M) 1 1
⊢ (ζ ^ (i.gcd k * a)) ^ b = 1

Tactic:
rw [← pow_mul', ← mul_assoc, ← hb, pow_mul, h.pow_eq_one, one_pow]

Premises used: one_pow, mul_assoc, pow_mul, pow_mul', IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
⊢ IsPrimitiveRoot ζ (orderOf ζ)

Tactic:
⟨pow_orderOf_eq_one ζ, fun _ ↦ orderOf_dvd_of_pow_eq_one⟩

Premises used: IsPrimitiveRoot.mk, orderOf_dvd_of_pow_eq_one, pow_orderOf_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k l : ℕ
ζ : M
hk : IsPrimitiveRoot ζ k
hl : IsPrimitiveRoot ζ l
⊢ k = l

Tactic:
Nat.dvd_antisymm (hk.2 _ hl.1) (hl.2 _ hk.1)

Premises used: IsPrimitiveRoot.dvd_of_pow_eq_one, IsPrimitiveRoot.pow_eq_one, Nat.dvd_antisymm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
⊢ k = orderOf ζ

Tactic:
h.unique (IsPrimitiveRoot.orderOf ζ)

Premises used: IsPrimitiveRoot.orderOf, IsPrimitiveRoot.unique
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
⊢ IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1

Tactic:
⟨fun h ↦ ⟨h.pow_eq_one, fun l hl' hl ↦ ?_⟩,
    fun ⟨hζ, hl⟩ ↦ IsPrimitiveRoot.mk_of_lt ζ hk hζ hl⟩

Premises used: _private.0.IsPrimitiveRoot.iff.match_1, IsPrimitiveRoot.mk_of_lt, And.intro, Iff.intro, IsPrimitiveRoot, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
refine : ∀ (h : IsPrimitiveRoot ζ k) (l : ℕ) (hl' : 0 < l) (hl : l < k), ζ ^ l ≠ 1
⊢ IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1

Tactic:
refine ⟨fun h ↦ ⟨h.pow_eq_one, fun l hl' hl ↦ ?_⟩,
    fun ⟨hζ, hl⟩ ↦ IsPrimitiveRoot.mk_of_lt ζ hk hζ hl⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < k
⊢ l < orderOf ζ

Tactic:
rw [h.eq_orderOf] at hl

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < orderOf ζ
⊢ ζ ^ l ≠ 1

Tactic:
pow_ne_one_of_lt_orderOf hl'.ne' hl

Premises used: LT.lt.ne', pow_ne_one_of_lt_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < orderOf ζ
⊢ ζ ^ l ≠ 1

Tactic:
exact pow_ne_one_of_lt_orderOf hl'.ne' hl

Premises used: LT.lt.ne', pow_ne_one_of_lt_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
⊢ ¬IsPrimitiveRoot ζ k ↔ orderOf ζ ≠ k

Tactic:
⟨fun h hk ↦ h <| hk ▸ IsPrimitiveRoot.orderOf ζ,
    fun h hk ↦ h.symm <| hk.unique <| IsPrimitiveRoot.orderOf ζ⟩

Premises used: IsPrimitiveRoot.orderOf, Eq.rec, Ne.symm, Iff.intro, IsPrimitiveRoot.unique
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
⊢ IsPrimitiveRoot ζ k ↔ orderOf ζ = k

Tactic:
not_iff_not.mp IsPrimitiveRoot.not_iff

Premises used: not_iff_not, IsPrimitiveRoot.not_iff, Iff.mp
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ IsPrimitiveRoot (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k'))
    (orderOf (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k')))

Tactic:
IsPrimitiveRoot.orderOf _

Premises used: IsPrimitiveRoot.orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
h : k.lcm k' = orderOf (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k'))
⊢ IsPrimitiveRoot (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k')) (k.lcm k')

Tactic:
convert! IsPrimitiveRoot.orderOf _

Premises used: IsPrimitiveRoot.orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ orderOf ζ ≠ 0

Tactic:
simpa [← hζ.eq_orderOf]

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ orderOf ζ' ≠ 0

Tactic:
simpa [← hζ'.eq_orderOf]

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
h : k = orderOf ζ
h₁ : k' = orderOf ζ'
h₂ :
  ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k') =
    ζ ^ (orderOf ζ / (orderOf ζ).factorizationLCMLeft (orderOf ζ')) *
      ζ' ^ (orderOf ζ' / (orderOf ζ).factorizationLCMRight (orderOf ζ'))
⊢ k.lcm k' = orderOf (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k'))

Tactic:
convert!
    ((Commute.all ζ ζ').orderOf_mul_pow_eq_lcm (by simpa [← hζ.eq_orderOf])
        (by simpa [← hζ'.eq_orderOf])).symm using 2

Premises used: Eq.symm, Commute.all, Commute.orderOf_mul_pow_eq_lcm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ k = orderOf ζ

Tactic:
simp [hζ.eq_orderOf, hζ'.eq_orderOf]

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ k' = orderOf ζ'

Tactic:
simp [hζ.eq_orderOf, hζ'.eq_orderOf]

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k') =
    ζ ^ (orderOf ζ / (orderOf ζ).factorizationLCMLeft (orderOf ζ')) *
      ζ' ^ (orderOf ζ' / (orderOf ζ).factorizationLCMRight (orderOf ζ'))

Tactic:
simp [hζ.eq_orderOf, hζ'.eq_orderOf]

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ k
rw : ∀ (hdiv : p ∣ orderOf ζ), IsPrimitiveRoot (ζ ^ p) (orderOf ζ / p)
⊢ IsPrimitiveRoot (ζ ^ p) (k / p)

Tactic:
rw [h.eq_orderOf] at hdiv ⊢

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
rw : IsPrimitiveRoot (ζ ^ p) (orderOf (ζ ^ p))
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf ζ / p)

Tactic:
rw [← orderOf_pow_of_dvd hp hdiv]

Premises used: orderOf_pow_of_dvd
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf (ζ ^ p))

Tactic:
IsPrimitiveRoot.orderOf _

Premises used: IsPrimitiveRoot.orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf (ζ ^ p))

Tactic:
exact IsPrimitiveRoot.orderOf _

Premises used: IsPrimitiveRoot.orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : Mˣ
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) ζ

Tactic:
h.pow_eq_one

Premises used: Set.Mem, setOf, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
n a b : ℕ
hn : 0 < n
h : IsPrimitiveRoot ζ n
hprod : n = a * b
⊢ 0 < a * b

Tactic:
subst n
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
n a b : ℕ
hn : 0 < n
h : IsPrimitiveRoot ζ n
hprod : n = a * b
hn₁ : 0 < a * b
⊢ IsPrimitiveRoot ζ (a * b)

Tactic:
subst n
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
simp : ∀ (l : ℕ), ζ ^ (a * l) = 1 → b ∣ l
⊢ IsPrimitiveRoot (ζ ^ a) b

Tactic:
simp only [iff_def, ← pow_mul, h.pow_eq_one, true_and]

Premises used: IsPrimitiveRoot.iff_def, pow_mul, IsPrimitiveRoot.pow_eq_one, true_and
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
hl : ζ ^ (a * l) = 1
⊢ b ∣ l

Tactic:
Nat.dvd_of_mul_dvd_mul_left (Nat.pos_of_mul_pos_right hn) <| h.dvd_of_pow_eq_one _ hl

Premises used: Nat.pos_of_mul_pos_right, IsPrimitiveRoot.dvd_of_pow_eq_one, Nat.dvd_of_mul_dvd_mul_left
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
l : ℕ
hl : ζ ^ (a * l) = 1
⊢ b ∣ l

Tactic:
exact Nat.dvd_of_mul_dvd_mul_left (Nat.pos_of_mul_pos_right hn) <| h.dvd_of_pow_eq_one _ hl

Premises used: Nat.pos_of_mul_pos_right, IsPrimitiveRoot.dvd_of_pow_eq_one, Nat.dvd_of_mul_dvd_mul_left
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i ∈ (↑(range n) : Set ℕ)
j : ℕ
hj : j ∈ (↑(range n) : Set ℕ)
e : Eq.{u_1 + 1} (α := M) ((fun (x : ℕ) ↦ ζ ^ x) i) ((fun (x : ℕ) ↦ ζ ^ x) j)
rw :
  ∀ (hi : i < n) ⦃j : ℕ⦄ (hj : j < n) (e : Eq.{u_1 + 1} (α := M) ((fun (x : ℕ) ↦ ζ ^ x) i) ((fun (x : ℕ) ↦ ζ ^ x) j)),
    i = j
⊢ i = j

Tactic:
rw [Finset.coe_range, Set.mem_Iio] at hi hj

Premises used: Set.mem_Iio, Finset.coe_range
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
e : Eq.{u_1 + 1} (α := M) ((fun (x : ℕ) ↦ ζ ^ x) i) ((fun (x : ℕ) ↦ ζ ^ x) j)
⊢ i = j

Tactic:
hζ.pow_inj hi hj e

Premises used: IsPrimitiveRoot.pow_inj
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
e : Eq.{u_1 + 1} (α := M) ((fun (x : ℕ) ↦ ζ ^ x) i) ((fun (x : ℕ) ↦ ζ ^ x) j)
⊢ i = j

Tactic:
exact hζ.pow_inj hi hj e

Premises used: IsPrimitiveRoot.pow_inj
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
k : ℕ
hζ : ζ ^ k = 1
hk : k ≠ 0
rw : ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1
⊢ orderOf ζ > 0

Tactic:
rw [gt_iff_lt, orderOf_pos_iff, isOfFinOrder_iff_pow_eq_one]

Premises used: gt_iff_lt, orderOf_pos_iff, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
k : ℕ
hζ : ζ ^ k = 1
hk : k ≠ 0
⊢ ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1

Tactic:
⟨k, Nat.pos_iff_ne_zero.mpr hk, hζ⟩

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
k : ℕ
hζ : ζ ^ k = 1
hk : k ≠ 0
⊢ ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1

Tactic:
exact ⟨k, Nat.pos_iff_ne_zero.mpr hk, hζ⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
⊢ ∃! k : ℕ, IsPrimitiveRoot ζ k

Tactic:
⟨_, .orderOf _, fun _ hl ↦ unique hl (.orderOf _)⟩

Premises used: IsPrimitiveRoot.orderOf, ExistsUnique, And.intro, Exists.intro, IsPrimitiveRoot.unique
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
inst : CommMonoid M
u : Mˣ
n : ℕ
inst_1 : NeZero n
hu : Membership.mem (γ := Subgroup Mˣ) (rootsOfUnity n M) u
⊢ ∃ (d : ℕ), d ≠ 0 ∧ d ∣ n ∧ IsPrimitiveRoot u d

Tactic:
⟨orderOf u, (IsOfFinOrder.orderOf_pos ⟨n, NeZero.pos n,
    (isPeriodicPt_mul_iff_pow_eq_one u).mpr hu⟩).ne', orderOf_dvd_of_pow_eq_one hu,
    IsPrimitiveRoot.orderOf u⟩

Premises used: Iff.mpr, IsPrimitiveRoot.orderOf, IsOfFinOrder.orderOf_pos, orderOf_dvd_of_pow_eq_one, LT.lt.ne', orderOf, isPeriodicPt_mul_iff_pow_eq_one, And.intro, Exists.intro, NeZero.pos
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
k : ℕ
ζ : M
f : F
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ k) : N) (1 : N)
rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 1 : N) (1 : N)
rw₂ rw₃ : Eq.{u_2 + 1} (α := N) 1 1
⊢ HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) k = 1

Tactic:
rw [← map_pow, h.pow_eq_one, map_one]

Premises used: map_pow, map_one, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
k : ℕ
ζ : M
f : F
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw : ∀ (l : ℕ), HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) l = 1 → orderOf ζ ∣ l
⊢ ∀ (l : ℕ), HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) l = 1 → k ∣ l

Tactic:
rw [h.eq_orderOf]

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
k : ℕ
ζ : M
f : F
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : ℕ
hl : HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) l = 1
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ l) : N) ((f : (a : M) → N) 1 : N)

Tactic:
rw [← map_pow, ← map_one f] at hl

Premises used: map_pow, map_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
k : ℕ
ζ : M
f : F
inst_2 : FunLike F M N
inst_3 : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : ℕ
hl : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ l) : N) ((f : (a : M) → N) 1 : N)
⊢ orderOf ζ ∣ l

Tactic:
orderOf_dvd_of_pow_eq_one (hf hl)

Premises used: orderOf_dvd_of_pow_eq_one