awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact orderOf_dvd_of_pow_eq_one (hf hl)

Premises used: orderOf_dvd_of_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.{u_2} (M := N) ((f : (a : M) → N) ζ : N) k
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
apply_fun : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ k) : N) ((f : (a : M) → N) 1 : N)
⊢ ζ ^ k = 1

Tactic:
apply_fun f
-- 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.{u_2} (M := N) ((f : (a : M) → N) ζ : N) k
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw : HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) k = (f : (a : M) → N) 1
rw₁ : HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) k = 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := N) 1 1
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ k) : N) ((f : (a : M) → N) 1 : N)

Tactic:
rw [map_pow, map_one, h.pow_eq_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.{u_2} (M := N) ((f : (a : M) → N) ζ : N) k
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw : ∀ (l : ℕ), ζ ^ l = 1 → orderOf.{u_2} (G := N) ((f : (a : M) → N) ζ : N) ∣ l
⊢ ∀ (l : ℕ), ζ ^ 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.{u_2} (M := N) ((f : (a : M) → N) ζ : N) k
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : ℕ
hl : ζ ^ l = 1
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ l) : N) ((f : (a : M) → N) 1 : N)

Tactic:
apply_fun f at hl
-- 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.{u_2} (M := N) ((f : (a : M) → N) ζ : N) 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)
⊢ HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) l = 1

Tactic:
rw [map_pow, map_one] 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.{u_2} (M := N) ((f : (a : M) → N) ζ : N) 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
⊢ orderOf.{u_2} (G := N) ((f : (a : M) → N) ζ : N) ∣ l

Tactic:
orderOf_dvd_of_pow_eq_one hl

Premises used: orderOf_dvd_of_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.{u_2} (M := N) ((f : (a : M) → N) ζ : N) 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
⊢ orderOf.{u_2} (G := N) ((f : (a : M) → N) ζ : N) ∣ l

Tactic:
exact orderOf_dvd_of_pow_eq_one hl

Premises used: orderOf_dvd_of_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
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsPrimitiveRoot.{u_2} (M := N) ((f : (a : M) → N) ζ : N) k ↔ IsPrimitiveRoot ζ k

Tactic:
⟨fun h => h.of_map_of_injective hf, fun h => h.map_of_injective hf⟩

Premises used: IsPrimitiveRoot.of_map_of_injective, Iff.intro, IsPrimitiveRoot.map_of_injective
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M₀ : Type u_7
inst : CommMonoidWithZero M₀
inst_1 : Nontrivial M₀
l : ℕ
hl : HPow.hPow (α := M₀) 0 l = 1
⊢ 0 ∣ l

Tactic:
simpa [zero_pow_eq] using hl

Premises used: zero_pow_eq
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
k : ℕ
M₀ : Type u_7
inst : CommMonoidWithZero M₀
inst_1 : Nontrivial M₀
ζ : M₀
h : IsPrimitiveRoot ζ k
⊢ k ≠ 0 → ζ ≠ 0

Tactic:
mt fun hn ↦ h.unique (hn.symm ▸ IsPrimitiveRoot.zero)

Premises used: mt, Eq.rec, IsPrimitiveRoot.zero, IsPrimitiveRoot.unique, Eq.symm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M₀ : Type u_7
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
n : ℕ
ζ : M₀
hζ : IsPrimitiveRoot ζ n
α : M₀
hα : α ≠ 0
i : ℕ
hi : i ∈ (↑(range n) : Set ℕ)
j : ℕ
hj : j ∈ (↑(range n) : Set ℕ)
e : Eq.{u_7 + 1} (α := M₀) ((fun (x : ℕ) ↦ ζ ^ x * α) i) ((fun (x : ℕ) ↦ ζ ^ x * α) j)
⊢ Eq.{u_7 + 1} (α := M₀) ((fun (x : ℕ) ↦ ζ ^ x) i) ((fun (x : ℕ) ↦ ζ ^ x) j)

Tactic:
simpa [mul_eq_mul_right_iff, or_iff_left hα] using e

Premises used: mul_eq_mul_right_iff, or_iff_left
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ HPow.hPow (β := ℤ) ζ (↑k : ℤ) = 1

Tactic:
exact_mod_cast h.pow_eq_one

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
pos : ∀ (h0 : 0 ≤ l), ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
neg : ∀ (h0 : ¬0 ≤ l), ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
⊢ ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l

Tactic:
by_cases h0 : 0 ≤ l
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : 0 ≤ l
⊢ 0 ≤ l

Tactic:
h0
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : 0 ≤ l
pos : ∀ (l : ℕ), HPow.hPow (β := ℤ) ζ (↑l : ℤ) = 1 ↔ Dvd.dvd (α := ℤ) (↑k : ℤ) (↑l : ℤ)
⊢ ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l

Tactic:
lift l to ℕ using h0
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ HPow.hPow (β := ℤ) ζ (↑l : ℤ) = 1 ↔ Dvd.dvd (α := ℤ) (↑k : ℤ) (↑l : ℤ)

Tactic:
exact_mod_cast h.pow_eq_one_iff_dvd l

Premises used: IsPrimitiveRoot.pow_eq_one_iff_dvd
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ 0 ≤ -l

Tactic:
have : 0 ≤ -l := (Int.neg_pos_of_neg <| Int.lt_of_not_ge h0).le
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
this : 0 ≤ -l
⊢ 0 ≤ -l

Tactic:
this
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
this : 0 ≤ -l
neg : ∀ (l' : ℕ) (hl' : (↑l' : ℤ) = -l), ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
⊢ ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l

Tactic:
lift -l to ℕ using this with l' hl'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : (↑l' : ℤ) = -l
neg : ζ ^ l = 1 ↔ Dvd.dvd (α := ℤ) (↑k : ℤ) (↑l' : ℤ)
⊢ ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l

Tactic:
rw [← dvd_neg, ← hl']

Premises used: dvd_neg
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : (↑l' : ℤ) = -l
neg : ζ ^ l = 1 ↔ k ∣ l'
⊢ ζ ^ l = 1 ↔ Dvd.dvd (α := ℤ) (↑k : ℤ) (↑l' : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : (↑l' : ℤ) = -l
neg : ζ ^ l = 1 ↔ ζ ^ l' = 1
neg₁ : (ζ ^ l)⁻¹ = 1⁻¹ ↔ ζ ^ l' = 1
neg₂ : ζ ^ (-l) = 1⁻¹ ↔ ζ ^ l' = 1
neg₃ : HPow.hPow (β := ℤ) ζ (↑l' : ℤ) = 1⁻¹ ↔ ζ ^ l' = 1
neg₄ : ζ ^ l' = 1⁻¹ ↔ ζ ^ l' = 1
neg₅ neg₆ : ζ ^ l' = 1 ↔ ζ ^ l' = 1
⊢ ζ ^ l = 1 ↔ k ∣ l'

Tactic:
rw [← h.pow_eq_one_iff_dvd, ← inv_inj, ← zpow_neg, ← hl', zpow_natCast, inv_one]

Premises used: zpow_natCast, inv_one, inv_inj, zpow_neg, IsPrimitiveRoot.pow_eq_one_iff_dvd
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ζ⁻¹ ^ k = 1

Tactic:
simp only [h.pow_eq_one, inv_one, inv_pow]

Premises used: inv_one, inv_pow, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
apply : ζ ^ l = 1
⊢ k ∣ l

Tactic:
apply h.dvd_of_pow_eq_one l

Premises used: IsPrimitiveRoot.dvd_of_pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
rw : (ζ ^ l)⁻¹ = 1⁻¹
rw₁ : ζ⁻¹ ^ l = 1⁻¹
rw₂ : Eq.{u_3 + 1} (α := G) 1 1⁻¹
rw₃ rw₄ : Eq.{u_3 + 1} (α := G) 1 1
⊢ ζ ^ l = 1

Tactic:
rw [← inv_inj, ← inv_pow, hl, inv_one]

Premises used: inv_one, inv_pow, inv_inj
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
⊢ IsPrimitiveRoot ζ⁻¹ k ↔ IsPrimitiveRoot ζ k

Tactic:
⟨fun h ↦ inv_inv ζ ▸ inv h, fun h ↦ inv h⟩

Premises used: Eq.rec, IsPrimitiveRoot.inv, inv_inv, Iff.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
pos : ∀ (h0 : 0 ≤ i), IsPrimitiveRoot (ζ ^ i) k
neg : ∀ (h0 : ¬0 ≤ i), IsPrimitiveRoot (ζ ^ i) k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
by_cases h0 : 0 ≤ i
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
h0 : 0 ≤ i
⊢ 0 ≤ i

Tactic:
h0
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
h0 : 0 ≤ i
pos : ∀ (i : ℕ) (hi : Int.gcd (↑i : ℤ) (↑k : ℤ) = 1), IsPrimitiveRoot (HPow.hPow (β := ℤ) ζ (↑i : ℤ)) k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
lift i to ℕ using h0
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℕ
hi : Int.gcd (↑i : ℤ) (↑k : ℤ) = 1
⊢ IsPrimitiveRoot (HPow.hPow (β := ℤ) ζ (↑i : ℤ)) k

Tactic:
exact_mod_cast h.pow_of_coprime i hi

Premises used: IsPrimitiveRoot.pow_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
h0 : ¬0 ≤ i
⊢ 0 ≤ -i

Tactic:
have : 0 ≤ -i := (Int.neg_pos_of_neg <| Int.lt_of_not_ge h0).le
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
h0 : ¬0 ≤ i
this : 0 ≤ -i
⊢ 0 ≤ -i

Tactic:
this
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
h0 : ¬0 ≤ i
this : 0 ≤ -i
neg : ∀ (i' : ℕ) (hi' : (↑i' : ℤ) = -i), IsPrimitiveRoot (ζ ^ i) k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
lift -i to ℕ using this with i' hi'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : (↑i' : ℤ) = -i
neg : IsPrimitiveRoot (ζ ^ i') k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
rw [← inv_iff, ← zpow_neg, ← hi', zpow_natCast]

Premises used: zpow_natCast, IsPrimitiveRoot.inv_iff, zpow_neg
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : (↑i' : ℤ) = -i
neg : i'.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i') k

Tactic:
apply h.pow_of_coprime

Premises used: IsPrimitiveRoot.pow_of_coprime
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : (↑i' : ℤ) = -i
neg : ∀ (hi : i.natAbs.gcd (Int.natAbs (↑k : ℤ)) = 1) (h0 : ¬0 ≤ i) (i' : ℕ) (hi' : (↑i' : ℤ) = -i), i'.Coprime k
neg₁ : ∀ (hi : (-i).natAbs.gcd (Int.natAbs (↑k : ℤ)) = 1) (h0 : ¬0 ≤ i) (i' : ℕ) (hi' : (↑i' : ℤ) = -i), i'.Coprime k
neg₂ neg₃ neg₄ neg₅ :
  ∀ (h0 : ¬0 ≤ i) (i' : ℕ) (hi : (Int.natAbs (↑i' : ℤ)).gcd (Int.natAbs (↑k : ℤ)) = 1) (hi' : (↑i' : ℤ) = -i),
    i'.Coprime k
⊢ i'.Coprime k

Tactic:
rwa [Int.gcd, ← Int.natAbs_neg, ← hi'] at hi

Premises used: Int.gcd, Int.natAbs_neg
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
n : ℕ
ζ : R
hn : 1 < n
hζ : IsPrimitiveRoot ζ n
⊢ ζ - 1 ≠ 0

Tactic:
sub_ne_zero.mpr <| hζ.ne_one hn

Premises used: Iff.mpr, sub_ne_zero, IsPrimitiveRoot.ne_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ (HPow.hPow (α := R[X]) X n - 1).IsRoot ζ

Tactic:
simp [hζ.pow_eq_one]

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
k : ℕ
⊢ (HPow.hPow (α := R[X]) X (n * k) - 1).IsRoot ζ

Tactic:
simp [pow_mul, hζ.pow_eq_one]

Premises used: pow_mul, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
⊢ primitiveRoots 1 R = {1}

Tactic:
Finset.eq_singleton_iff_unique_mem.2 ⟨?_, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Finset.eq_singleton_iff_unique_mem, And.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
refine_1 : 1 ∈ primitiveRoots 1 R
refine_2 : ∀ (x : R) (hx : x ∈ primitiveRoots 1 R), x = 1
⊢ primitiveRoots 1 R = {1}

Tactic:
refine Finset.eq_singleton_iff_unique_mem.2 ⟨?_, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Finset.eq_singleton_iff_unique_mem, And.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
⊢ 1 ∈ primitiveRoots 1 R

Tactic:
simp only [IsPrimitiveRoot.one_right_iff, mem_primitiveRoots zero_lt_one]

Premises used: zero_lt_one, IsPrimitiveRoot.one_right_iff, mem_primitiveRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
x : R
hx : x ∈ primitiveRoots 1 R
refine_2 : ∀ (hx : IsPrimitiveRoot x 1), x = 1
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : ∀ (hx : x = 1), x = 1
⊢ x = 1

Tactic:
rwa [mem_primitiveRoots zero_lt_one, IsPrimitiveRoot.one_right_iff] at hx

Premises used: zero_lt_one, IsPrimitiveRoot.one_right_iff, mem_primitiveRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
ζ : R
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
inst_2 : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
⊢ NeZero.{u_4} (R := R) (↑n : R)

Tactic:
.of_not_dvd R (p := p) fun hpn ↦ ?_

Premises used: NeZero.of_not_dvd
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
ζ : R
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
inst_2 : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
refine : ∀ (hpn : p ∣ n), False
⊢ NeZero.{u_4} (R := R) (↑n : R)

Tactic:
refine .of_not_dvd R (p := p) fun hpn ↦ ?_
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
ζ : R
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
inst_2 : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hpn : p ∣ n
obtain : ∀ (n : ℕ) [NeZero (p * n)] (hζ : IsPrimitiveRoot ζ (p * n)), False
⊢ False

Tactic:
obtain ⟨n, rfl⟩ := hpn

Premises used: rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
ζ : R
inst : CommRing R
inst_1 : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst_2 : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
⊢ p ≠ 0 ∧ n ≠ 0

Tactic:
aesop
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
ζ : R
inst : CommRing R
inst_1 : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst_2 : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
⊢ p ≠ 0 ∧ n ≠ 0

Tactic:
have h : p ≠ 0 ∧ n ≠ 0 := by aesop
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
ζ : R
inst : CommRing R
inst_1 : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst_2 : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
h : p ≠ 0 ∧ n ≠ 0
⊢ NeZero p

Tactic:
have : NeZero p := .mk h.1
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
ζ : R
inst : CommRing R
inst_1 : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst_2 : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
h : p ≠ 0 ∧ n ≠ 0
this : NeZero p
⊢ Fact (Nat.Prime p)

Tactic:
have hp : Fact p.Prime := CharP.char_is_prime_of_pos R p
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
ζ : R
inst : CommRing R
inst_1 : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst_2 : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
h : p ≠ 0 ∧ n ≠ 0
this : NeZero p
hp : Fact (Nat.Prime p)
⊢ 0 < n

Tactic:
grind
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
ζ : R
inst : CommRing R
inst_1 : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst_2 : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
h : p ≠ 0 ∧ n ≠ 0
this : NeZero p
hp : Fact (Nat.Prime p)
refine : Eq (α := R) ((frobenius R p : (a : R) → R) (ζ ^ n) : R) ((frobenius R p : (a : R) → R) 1 : R)
⊢ False

Tactic:
refine (hζ.pow_ne_one_of_pos_of_lt h.2 (lt_mul_of_one_lt_left (by grind) hp.1.one_lt) <|
    frobenius_inj R p ?_).elim

Premises used: IsPrimitiveRoot.pow_ne_one_of_pos_of_lt, Nat.Prime.one_lt, False.elim, And.right, Fact.out, frobenius_inj, lt_mul_of_one_lt_left
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
ζ : R
inst : CommRing R
inst_1 : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst_2 : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
h : p ≠ 0 ∧ n ≠ 0
this : NeZero p
hp : Fact (Nat.Prime p)
rw : (ζ ^ n) ^ p = (frobenius R p : (a : R) → R) 1
rw₁ : ζ ^ (p * n) = (frobenius R p : (a : R) → R) 1
rw₂ : Eq (α := R) (1 : R) ((frobenius R p : (a : R) → R) 1 : R)
rw₃ rw₄ : Eq.{u_4 + 1} (α := R) 1 1
⊢ Eq (α := R) ((frobenius R p : (a : R) → R) (ζ ^ n) : R) ((frobenius R p : (a : R) → R) 1 : R)

Tactic:
rw [frobenius_def, ← pow_mul', hζ.1, map_one]

Premises used: frobenius_def, map_one, pow_mul', IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
ζ : R
inst : CommRing R
inst_1 : IsDomain R
hζ : IsPrimitiveRoot ζ k
hk : 0 < k
⊢ Membership.mem (γ := Finset R) (nthRootsFinset k 1) ζ

Tactic:
(mem_nthRootsFinset hk (1 : R)).2 hζ.pow_eq_one

Premises used: Iff.mpr, OfNat.ofNat, IsPrimitiveRoot.pow_eq_one, Polynomial.mem_nthRootsFinset
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : NoZeroDivisors R
ζ : R
h : IsPrimitiveRoot ζ 2
⊢ ζ = -1

Tactic:
(sq_eq_one_iff.mp h.pow_eq_one).resolve_left <| ne_one h one_lt_two

Premises used: sq_eq_one_iff, Or.resolve_left, Iff.mp, one_lt_two, IsPrimitiveRoot.ne_one, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
p : ℕ
inst_1 : Nontrivial R
h : CharP R p
hp : p ≠ 2
⊢ IsPrimitiveRoot.{u_4} (M := R) (-1) (orderOf.{u_4} (G := R) (-1))

Tactic:
IsPrimitiveRoot.orderOf (-1 : R)

Premises used: IsPrimitiveRoot.orderOf, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
p : ℕ
inst_1 : Nontrivial R
h : CharP R p
hp : p ≠ 2
h₁ : 2 = orderOf.{u_4} (G := R) (-1)
⊢ IsPrimitiveRoot.{u_4} (M := R) (-1) 2

Tactic:
convert! IsPrimitiveRoot.orderOf (-1 : R)

Premises used: IsPrimitiveRoot.orderOf, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
p : ℕ
inst_1 : Nontrivial R
h : CharP R p
hp : p ≠ 2
rwa rwa₁ rwa₂ rwa₃ : ¬p = 2
⊢ ¬ringChar R = 2

Tactic:
rwa [ringChar.eq_iff.mpr h]

Premises used: Iff.mpr, ringChar.eq_iff
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
p : ℕ
inst_1 : Nontrivial R
h : CharP R p
hp : p ≠ 2
h₁ : Eq (α := ℕ) 2 (if ringChar R = 2 then 1 else 2)
h₂ h₃ : Eq (α := ℕ) 2 2
⊢ 2 = orderOf.{u_4} (G := R) (-1)

Tactic:
rw [orderOf_neg_one, if_neg <| by rwa [ringChar.eq_iff.mpr h]]

Premises used: orderOf_neg_one, if_neg
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
inst_1 : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
⊢ Eq.{u_4 + 1} (α := R) (∑ i ∈ range k, ζ ^ i) 0

Tactic:
eq_zero_of_ne_zero_of_mul_left_eq_zero (sub_ne_zero_of_ne (hζ.ne_one hk).symm) ?_

Premises used: Ne.symm, eq_zero_of_ne_zero_of_mul_left_eq_zero, sub_ne_zero_of_ne, IsPrimitiveRoot.ne_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
inst_1 : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
refine : (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 0
⊢ Eq.{u_4 + 1} (α := R) (∑ i ∈ range k, ζ ^ i) 0

Tactic:
refine eq_zero_of_ne_zero_of_mul_left_eq_zero (sub_ne_zero_of_ne (hζ.ne_one hk).symm) ?_

Premises used: Ne.symm, eq_zero_of_ne_zero_of_mul_left_eq_zero, sub_ne_zero_of_ne, IsPrimitiveRoot.ne_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
inst_1 : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
rw : 1 - ζ ^ k = 0
rw₁ : HSub.hSub (α := R) 1 1 = 0
rw₂ rw₃ : Eq.{u_4 + 1} (α := R) 0 0
⊢ (1 - ζ) * ∑ i ∈ range k, ζ ^ i = 0

Tactic:
rw [mul_neg_geom_sum, hζ.pow_eq_one, sub_self]

Premises used: sub_self, mul_neg_geom_sum, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
inst_1 : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
⊢ IsRoot (∑ i ∈ range k, HPow.hPow (α := R[X]) X i) ζ

Tactic:
simp [geom_sum_eq_zero hζ hk]

Premises used: IsPrimitiveRoot.geom_sum_eq_zero
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
inst_1 : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
rw : ζ ^ k.pred + ∑ i ∈ range k.pred, ζ ^ i = 0
rw₁ : ∑ i ∈ range k.pred, ζ ^ i + ζ ^ k.pred = 0
rw₂ : Eq.{u_4 + 1} (α := R) (∑ x ∈ range (k.pred + 1), ζ ^ x) 0
rw₃ : Eq.{u_4 + 1} (α := R) (∑ x ∈ range k.pred.succ, ζ ^ x) 0
rw₄ : Eq.{u_4 + 1} (α := R) (∑ x ∈ range k, ζ ^ x) 0
rw₅ rw₆ : Eq.{u_4 + 1} (α := R) 0 0
⊢ ζ ^ k.pred = -∑ i ∈ range k.pred, ζ ^ i

Tactic:
rw [eq_neg_iff_add_eq_zero, add_comm, ← sum_range_succ, ← Nat.succ_eq_add_one,
    Nat.succ_pred_eq_of_pos (pos_of_gt hk), hζ.geom_sum_eq_zero hk]

Premises used: Nat.succ_eq_add_one, Nat.succ_pred_eq_of_pos, pos_of_gt, add_comm, IsPrimitiveRoot.geom_sum_eq_zero, eq_neg_iff_add_eq_zero, Finset.sum_range_succ