awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ b = k
have rw : ∀ (hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k) (ha : i = i.gcd k * a) (b : ℕ) (hb : k = i.gcd k * b), b = k
Tactic: rw [ha] at hi
Cleared hypotheses: hi, ha, b, hb
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ b = k
have apply : (ζ ^ (i.gcd k * a)) ^ b = 1
Tactic: apply Nat.dvd_antisymm ⟨i.gcd k, hb⟩ (hi.dvd_of_pow_eq_one b _)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ (ζ ^ (i.gcd k * a)) ^ b = 1
have rw : ζ ^ (b * (i.gcd k * a)) = 1
Tactic: rw [← pow_mul', ← mul_assoc, ← hb, pow_mul, h.pow_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ (ζ ^ (i.gcd k * a)) ^ b = 1
have rw₁ : ζ ^ (b * i.gcd k * a) = 1
Tactic: rw [← pow_mul', ← mul_assoc, ← hb, pow_mul, h.pow_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ (ζ ^ (i.gcd k * a)) ^ b = 1
have rw₂ : ζ ^ (k * a) = 1
Tactic: rw [← pow_mul', ← mul_assoc, ← hb, pow_mul, h.pow_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ (ζ ^ (i.gcd k * a)) ^ b = 1
have rw₃ : (ζ ^ k) ^ a = 1
Tactic: rw [← pow_mul', ← mul_assoc, ← hb, pow_mul, h.pow_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ (ζ ^ (i.gcd k * a)) ^ b = 1
have rw₄ : HPow.hPow (α := M) 1 a = 1
Tactic: rw [← pow_mul', ← mul_assoc, ← hb, pow_mul, h.pow_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ (ζ ^ (i.gcd k * a)) ^ b = 1
have rw₅ : Eq.{u_1 + 1} (α := M) 1 1
Tactic: rw [← pow_mul', ← mul_assoc, ← hb, pow_mul, h.pow_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
⊢ IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
have refine : ∀ (h : IsPrimitiveRoot ζ k) (l : ℕ) (hl' : 0 < l) (hl : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < k
⊢ ζ ^ l ≠ 1
have hl₁ : l < orderOf ζ
Tactic: rw [h.eq_orderOf] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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')) (k.lcm k')
have h : k.lcm k' = orderOf (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k'))
Tactic: convert! IsPrimitiveRoot.orderOf _
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ k.lcm k' = orderOf (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k'))
have h : k = orderOf ζ
Tactic: convert!
    ((Commute.all ζ ζ').orderOf_mul_pow_eq_lcm (by simpa [← hζ.eq_orderOf])
        (by simpa [← hζ'.eq_orderOf])).symm using 2
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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 ζ
⊢ k.lcm k' = orderOf (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k'))
have h₁ : k' = orderOf ζ'
Tactic: convert!
    ((Commute.all ζ ζ').orderOf_mul_pow_eq_lcm (by simpa [← hζ.eq_orderOf])
        (by simpa [← hζ'.eq_orderOf])).symm using 2
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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 ζ'
⊢ k.lcm k' = orderOf (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k'))
have h₂ : ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k') =
  ζ ^ (orderOf ζ / (orderOf ζ).factorizationLCMLeft (orderOf ζ')) *
    ζ' ^ (orderOf ζ' / (orderOf ζ).factorizationLCMRight (orderOf ζ'))
Tactic: convert!
    ((Commute.all ζ ζ').orderOf_mul_pow_eq_lcm (by simpa [← hζ.eq_orderOf])
        (by simpa [← hζ'.eq_orderOf])).symm using 2
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ k
⊢ IsPrimitiveRoot (ζ ^ p) (k / p)
have rw : ∀ (hdiv : p ∣ orderOf ζ), IsPrimitiveRoot (ζ ^ p) (orderOf ζ / p)
Tactic: rw [h.eq_orderOf] at hdiv ⊢
Cleared hypotheses: hdiv
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
M : Type u_1
inst : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf ζ / p)
have rw : IsPrimitiveRoot (ζ ^ p) (orderOf (ζ ^ p))
Tactic: rw [← orderOf_pow_of_dvd hp hdiv]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
n a b : ℕ
hn : 0 < n
h : IsPrimitiveRoot ζ n
hprod : n = a * b
⊢ IsPrimitiveRoot (ζ ^ a) b
have hn₁ : 0 < a * b
Tactic: subst n
Cleared hypotheses: n, hn, h, hprod
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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
have h₁ : IsPrimitiveRoot ζ (a * b)
Tactic: subst n
Cleared hypotheses: n, hn, h, hprod
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
a b : ℕ
hn : 0 < a * b
h : IsPrimitiveRoot ζ (a * b)
⊢ IsPrimitiveRoot (ζ ^ a) b
have simp : ∀ (l : ℕ), ζ ^ (a * l) = 1 → b ∣ l
Tactic: simp only [iff_def, ← pow_mul, h.pow_eq_one, true_and]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
⊢ i = j
have rw : ∀ (hi : i < n) ⦃j : ℕ⦄ (hj : j < n) (e : Eq.{u_1 + 1} (α := M) ((fun (x : ℕ) ↦ ζ ^ x) i) ((fun (x : ℕ) ↦ ζ ^ x) j)),
  i = j
Tactic: rw [Finset.coe_range, Set.mem_Iio] at hi hj
Cleared hypotheses: hi, j, hj, e
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
M : Type u_1
inst : CommMonoid M
ζ : M
k : ℕ
hζ : ζ ^ k = 1
hk : k ≠ 0
⊢ orderOf ζ > 0
have rw : ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1
Tactic: rw [gt_iff_lt, orderOf_pos_iff, isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
⊢ HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) k = 1
have rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ k) : N) (1 : N)
Tactic: rw [← map_pow, h.pow_eq_one, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
⊢ HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) k = 1
have rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) 1 : N) (1 : N)
Tactic: rw [← map_pow, h.pow_eq_one, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
⊢ HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) k = 1
have rw₂ : Eq.{u_2 + 1} (α := N) 1 1
Tactic: rw [← map_pow, h.pow_eq_one, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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 : ℕ), HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) l = 1 → k ∣ l
have rw : ∀ (l : ℕ), HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) l = 1 → orderOf ζ ∣ l
Tactic: rw [h.eq_orderOf]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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
⊢ orderOf ζ ∣ l
have hl₁ : 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
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
⊢ ζ ^ k = 1
have apply_fun : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ k) : N) ((f : (a : M) → N) 1 : N)
Tactic: apply_fun f
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ k) : N) ((f : (a : M) → N) 1 : N)
have rw : HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) k = (f : (a : M) → N) 1
Tactic: rw [map_pow, map_one, h.pow_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ k) : N) ((f : (a : M) → N) 1 : N)
have rw₁ : HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) k = 1
Tactic: rw [map_pow, map_one, h.pow_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ k) : N) ((f : (a : M) → N) 1 : N)
have rw₂ : Eq.{u_2 + 1} (α := N) 1 1
Tactic: rw [map_pow, map_one, h.pow_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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 : ℕ), ζ ^ l = 1 → k ∣ l
have rw : ∀ (l : ℕ), ζ ^ l = 1 → orderOf.{u_2} (G := N) ((f : (a : M) → N) ζ : N) ∣ l
Tactic: rw [h.eq_orderOf]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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
⊢ orderOf.{u_2} (G := N) ((f : (a : M) → N) ζ : N) ∣ l
have hl₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (ζ ^ l) : N) ((f : (a : M) → N) 1 : N)
Tactic: apply_fun f at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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)
⊢ orderOf.{u_2} (G := N) ((f : (a : M) → N) ζ : N) ∣ l
have hl₁ : HPow.hPow (α := N) ((f : (a : M) → N) ζ : N) l = 1
Tactic: rw [map_pow, map_one] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
⊢ ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
have pos : ∀ (h0 : 0 ≤ l), ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
Tactic: by_cases h0 : 0 ≤ l
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
pos : ∀ (h0 : 0 ≤ l), ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
⊢ ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
have neg : ∀ (h0 : ¬0 ≤ l), ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
Tactic: by_cases h0 : 0 ≤ l
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : 0 ≤ l
⊢ ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
have pos : ∀ (l : ℕ), HPow.hPow (β := ℤ) ζ (↑l : ℤ) = 1 ↔ Dvd.dvd (α := ℤ) (↑k : ℤ) (↑l : ℤ)
Tactic: lift l to ℕ using h0
Cleared hypotheses: l, h0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
have this : 0 ≤ -l
Tactic: have : 0 ≤ -l := (Int.neg_pos_of_neg <| Int.lt_of_not_ge h0).le
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
this : 0 ≤ -l
⊢ ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
have neg : ∀ (l' : ℕ) (hl' : (↑l' : ℤ) = -l), ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
Tactic: lift -l to ℕ using this with l' hl'
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : (↑l' : ℤ) = -l
⊢ ζ ^ l = 1 ↔ (↑k : ℤ) ∣ l
have neg : ζ ^ l = 1 ↔ Dvd.dvd (α := ℤ) (↑k : ℤ) (↑l' : ℤ)
Tactic: rw [← dvd_neg, ← hl']
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : (↑l' : ℤ) = -l
⊢ ζ ^ l = 1 ↔ Dvd.dvd (α := ℤ) (↑k : ℤ) (↑l' : ℤ)
have neg : ζ ^ l = 1 ↔ k ∣ l'
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : (↑l' : ℤ) = -l
⊢ ζ ^ l = 1 ↔ k ∣ l'
have neg : ζ ^ l = 1 ↔ ζ ^ l' = 1
Tactic: rw [← h.pow_eq_one_iff_dvd, ← inv_inj, ← zpow_neg, ← hl', zpow_natCast, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ ζ ^ l = 1 ↔ k ∣ l'
have neg₁ : (ζ ^ l)⁻¹ = 1⁻¹ ↔ ζ ^ l' = 1
Tactic: rw [← h.pow_eq_one_iff_dvd, ← inv_inj, ← zpow_neg, ← hl', zpow_natCast, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ ζ ^ l = 1 ↔ k ∣ l'
have neg₂ : ζ ^ (-l) = 1⁻¹ ↔ ζ ^ l' = 1
Tactic: rw [← h.pow_eq_one_iff_dvd, ← inv_inj, ← zpow_neg, ← hl', zpow_natCast, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ ζ ^ l = 1 ↔ k ∣ l'
have neg₃ : HPow.hPow (β := ℤ) ζ (↑l' : ℤ) = 1⁻¹ ↔ ζ ^ l' = 1
Tactic: rw [← h.pow_eq_one_iff_dvd, ← inv_inj, ← zpow_neg, ← hl', zpow_natCast, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ ζ ^ l = 1 ↔ k ∣ l'
have neg₄ : ζ ^ l' = 1⁻¹ ↔ ζ ^ l' = 1
Tactic: rw [← h.pow_eq_one_iff_dvd, ← inv_inj, ← zpow_neg, ← hl', zpow_natCast, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ ζ ^ l = 1 ↔ k ∣ l'
have neg₅ : ζ ^ l' = 1 ↔ ζ ^ l' = 1
Tactic: rw [← h.pow_eq_one_iff_dvd, ← inv_inj, ← zpow_neg, ← hl', zpow_natCast, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ k ∣ l
have apply : ζ ^ l = 1
Tactic: apply h.dvd_of_pow_eq_one l
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ ζ ^ l = 1
have rw : (ζ ^ l)⁻¹ = 1⁻¹
Tactic: rw [← inv_inj, ← inv_pow, hl, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
rw : (ζ ^ l)⁻¹ = 1⁻¹
⊢ ζ ^ l = 1
have rw₁ : ζ⁻¹ ^ l = 1⁻¹
Tactic: rw [← inv_inj, ← inv_pow, hl, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
rw : (ζ ^ l)⁻¹ = 1⁻¹
rw₁ : ζ⁻¹ ^ l = 1⁻¹
⊢ ζ ^ l = 1
have rw₂ : Eq.{u_3 + 1} (α := G) 1 1⁻¹
Tactic: rw [← inv_inj, ← inv_pow, hl, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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⁻¹
⊢ ζ ^ l = 1
have rw₃ : Eq.{u_3 + 1} (α := G) 1 1
Tactic: rw [← inv_inj, ← inv_pow, hl, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
⊢ IsPrimitiveRoot (ζ ^ i) k
have pos : ∀ (h0 : 0 ≤ i), IsPrimitiveRoot (ζ ^ i) k
Tactic: by_cases h0 : 0 ≤ i
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ IsPrimitiveRoot (ζ ^ i) k
have neg : ∀ (h0 : ¬0 ≤ i), IsPrimitiveRoot (ζ ^ i) k
Tactic: by_cases h0 : 0 ≤ i
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
h0 : 0 ≤ i
⊢ IsPrimitiveRoot (ζ ^ i) k
have pos : ∀ (i : ℕ) (hi : Int.gcd (↑i : ℤ) (↑k : ℤ) = 1), IsPrimitiveRoot (HPow.hPow (β := ℤ) ζ (↑i : ℤ)) k
Tactic: lift i to ℕ using h0
Cleared hypotheses: i, hi, h0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
G : Type u_3
inst : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd (↑k : ℤ) = 1
h0 : ¬0 ≤ i
⊢ IsPrimitiveRoot (ζ ^ i) k
have this : 0 ≤ -i
Tactic: have : 0 ≤ -i := (Int.neg_pos_of_neg <| Int.lt_of_not_ge h0).le
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ IsPrimitiveRoot (ζ ^ i) k
have neg : ∀ (i' : ℕ) (hi' : (↑i' : ℤ) = -i), IsPrimitiveRoot (ζ ^ i) k
Tactic: lift -i to ℕ using this with i' hi'
Cleared hypotheses: this