awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
F : Type u_8
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : MonoidHomClass F R S
n : ℕ
inst_6 : NeZero n
f : F
hf : Function.Injective.{u_4 + 1, u_7 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hζ : (primitiveRoots n R).Nonempty
ε : ↥(rootsOfUnity n R)
⊢ Eq.{u_7 + 1} (α := S)
    ((f : (a : R) → S)
        (↑(↑(((MulEquiv.symm (rootsOfUnityEquivOfPrimitiveRoots hf hζ) :
                      MulEquiv.{u_7, u_4} ↥(rootsOfUnity n S) ↥(rootsOfUnity n R)) :
                    (a : ↥(rootsOfUnity n S)) → ↥(rootsOfUnity n R))
                  (((rootsOfUnityEquivOfPrimitiveRoots hf hζ :
                        MulEquiv.{u_4, u_7} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                      (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
                    ε)) :
              Rˣ) :
          R) :
      S)
    ((↑(↑(((rootsOfUnityEquivOfPrimitiveRoots hf hζ : MulEquiv.{u_4, u_7} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                  (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
                ε) :
            Sˣ) :
        S) :
      S)
have rw : Eq.{u_7 + 1} (α := S) ((f : (a : R) → S) (↑(↑ε : Rˣ) : R) : S)
  ((↑(↑(((rootsOfUnityEquivOfPrimitiveRoots hf hζ : MulEquiv.{u_4, u_7} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
              ε) :
          Sˣ) :
      S) :
    S)
Tactic: rw [MulEquiv.symm_apply_apply, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
S : Type u_7
F : Type u_8
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : FunLike F R S
inst_5 : MonoidHomClass F R S
n : ℕ
inst_6 : NeZero n
f : F
hf : Function.Injective.{u_4 + 1, u_7 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hζ : (primitiveRoots n R).Nonempty
ε : ↥(rootsOfUnity n R)
rw :
  Eq.{u_7 + 1} (α := S) ((f : (a : R) → S) (↑(↑ε : Rˣ) : R) : S)
    ((↑(↑(((rootsOfUnityEquivOfPrimitiveRoots hf hζ : MulEquiv.{u_4, u_7} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                  (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
                ε) :
            Sˣ) :
        S) :
      S)
⊢ Eq.{u_7 + 1} (α := S)
    ((f : (a : R) → S)
        (↑(↑(((MulEquiv.symm (rootsOfUnityEquivOfPrimitiveRoots hf hζ) :
                      MulEquiv.{u_7, u_4} ↥(rootsOfUnity n S) ↥(rootsOfUnity n R)) :
                    (a : ↥(rootsOfUnity n S)) → ↥(rootsOfUnity n R))
                  (((rootsOfUnityEquivOfPrimitiveRoots hf hζ :
                        MulEquiv.{u_4, u_7} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                      (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
                    ε)) :
              Rˣ) :
          R) :
      S)
    ((↑(↑(((rootsOfUnityEquivOfPrimitiveRoots hf hζ : MulEquiv.{u_4, u_7} ↥(rootsOfUnity n R) ↥(rootsOfUnity n S)) :
                  (a : ↥(rootsOfUnity n R)) → ↥(rootsOfUnity n S))
                ε) :
            Sˣ) :
        S) :
      S)
have rw₁ : Eq.{u_7 + 1} (α := S) ((f : (a : R) → S) (↑(↑ε : Rˣ) : R) : S) ((f : (a : R) → S) (↑(↑ε : Rˣ) : R) : S)
Tactic: rw [MulEquiv.symm_apply_apply, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) ξ
⊢ ∃ (n : ℤ), ζ ^ n = ξ
have rwa : ∀ (hξ : Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) ξ), ∃ (n : ℤ), ζ ^ n = ξ
Tactic: rwa [← h.zpowers_eq] at hξ
Cleared hypotheses: hξ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) ξ
⊢ ∃ i < k, ζ ^ i = ξ
have obtain : ∀ (n : ℤ) (hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)), ∃ i < k, ζ ^ i = ζ ^ n
Tactic: obtain ⟨n, rfl⟩ : ∃ n : ℤ, ζ ^ n = ξ := by rwa [← h.zpowers_eq] at hξ
Cleared hypotheses: ξ, hξ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
⊢ ∃ i < k, ζ ^ i = ζ ^ n
have hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
Tactic: have hk0 : (0 : ℤ) < k := mod_cast NeZero.pos k
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
⊢ ∃ i < k, ζ ^ i = ζ ^ n
have hi0 : 0 ≤ i
Tactic: have hi0 : 0 ≤ i := Int.emod_nonneg _ (ne_of_gt hk0)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
hi0 : 0 ≤ i
⊢ ∃ i < k, ζ ^ i = ζ ^ n
have lift : ∀ (i₀ : ℕ) (hi₀ : (↑i₀ : ℤ) = i), ∃ i < k, ζ ^ i = ζ ^ n
Tactic: lift i to ℕ using hi0 with i₀ hi₀
Cleared hypotheses: hi0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
⊢ ∃ i < k, ζ ^ i = ζ ^ n
have refine_1 : i₀ < k
Tactic: refine ⟨i₀, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
refine_1 : i₀ < k
⊢ ∃ i < k, ζ ^ i = ζ ^ n
have refine_2 : ζ ^ i₀ = ζ ^ n
Tactic: refine ⟨i₀, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
⊢ i₀ < k
have refine_1 : LT.lt (α := ℤ) (↑i₀ : ℤ) (↑k : ℤ)
Tactic: zify
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
⊢ LT.lt (α := ℤ) (↑i₀ : ℤ) (↑k : ℤ)
have refine_1 : i < (↑k : ℤ)
Tactic: rw [hi₀]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
⊢ ζ ^ i₀ = ζ ^ n
have refine_2 : HPow.hPow (β := ℤ) ζ (↑i₀ : ℤ) = ζ ^ n
Tactic: rw [← zpow_natCast, hi₀, ← Int.emod_add_mul_ediv n k, zpow_add, zpow_mul, h.zpow_eq_one,
      one_zpow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
refine_2 : HPow.hPow (β := ℤ) ζ (↑i₀ : ℤ) = ζ ^ n
⊢ ζ ^ i₀ = ζ ^ n
have refine_2₁ : ζ ^ i = ζ ^ n
Tactic: rw [← zpow_natCast, hi₀, ← Int.emod_add_mul_ediv n k, zpow_add, zpow_mul, h.zpow_eq_one,
      one_zpow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
refine_2 : HPow.hPow (β := ℤ) ζ (↑i₀ : ℤ) = ζ ^ n
refine_2₁ : ζ ^ i = ζ ^ n
⊢ ζ ^ i₀ = ζ ^ n
have refine_2₂ : ζ ^ i = ζ ^ (n % (↑k : ℤ) + (↑k : ℤ) * (n / (↑k : ℤ)))
Tactic: rw [← zpow_natCast, hi₀, ← Int.emod_add_mul_ediv n k, zpow_add, zpow_mul, h.zpow_eq_one,
      one_zpow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
refine_2 : HPow.hPow (β := ℤ) ζ (↑i₀ : ℤ) = ζ ^ n
refine_2₁ : ζ ^ i = ζ ^ n
refine_2₂ : ζ ^ i = ζ ^ (n % (↑k : ℤ) + (↑k : ℤ) * (n / (↑k : ℤ)))
⊢ ζ ^ i₀ = ζ ^ n
have refine_2₃ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * ζ ^ ((↑k : ℤ) * (n / (↑k : ℤ)))
Tactic: rw [← zpow_natCast, hi₀, ← Int.emod_add_mul_ediv n k, zpow_add, zpow_mul, h.zpow_eq_one,
      one_zpow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
refine_2 : HPow.hPow (β := ℤ) ζ (↑i₀ : ℤ) = ζ ^ n
refine_2₁ : ζ ^ i = ζ ^ n
refine_2₂ : ζ ^ i = ζ ^ (n % (↑k : ℤ) + (↑k : ℤ) * (n / (↑k : ℤ)))
refine_2₃ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * ζ ^ ((↑k : ℤ) * (n / (↑k : ℤ)))
⊢ ζ ^ i₀ = ζ ^ n
have refine_2₄ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * HPow.hPow (β := ℤ) ζ (↑k : ℤ) ^ (n / (↑k : ℤ))
Tactic: rw [← zpow_natCast, hi₀, ← Int.emod_add_mul_ediv n k, zpow_add, zpow_mul, h.zpow_eq_one,
      one_zpow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
refine_2 : HPow.hPow (β := ℤ) ζ (↑i₀ : ℤ) = ζ ^ n
refine_2₁ : ζ ^ i = ζ ^ n
refine_2₂ : ζ ^ i = ζ ^ (n % (↑k : ℤ) + (↑k : ℤ) * (n / (↑k : ℤ)))
refine_2₃ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * ζ ^ ((↑k : ℤ) * (n / (↑k : ℤ)))
refine_2₄ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * HPow.hPow (β := ℤ) ζ (↑k : ℤ) ^ (n / (↑k : ℤ))
⊢ ζ ^ i₀ = ζ ^ n
have refine_2₅ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * HPow.hPow (α := Rˣ) 1 (n / (↑k : ℤ))
Tactic: rw [← zpow_natCast, hi₀, ← Int.emod_add_mul_ediv n k, zpow_add, zpow_mul, h.zpow_eq_one,
      one_zpow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
refine_2 : HPow.hPow (β := ℤ) ζ (↑i₀ : ℤ) = ζ ^ n
refine_2₁ : ζ ^ i = ζ ^ n
refine_2₂ : ζ ^ i = ζ ^ (n % (↑k : ℤ) + (↑k : ℤ) * (n / (↑k : ℤ)))
refine_2₃ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * ζ ^ ((↑k : ℤ) * (n / (↑k : ℤ)))
refine_2₄ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * HPow.hPow (β := ℤ) ζ (↑k : ℤ) ^ (n / (↑k : ℤ))
refine_2₅ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * HPow.hPow (α := Rˣ) 1 (n / (↑k : ℤ))
⊢ ζ ^ i₀ = ζ ^ n
have refine_2₆ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * 1
Tactic: rw [← zpow_natCast, hi₀, ← Int.emod_add_mul_ediv n k, zpow_add, zpow_mul, h.zpow_eq_one,
      one_zpow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)
hk0 : LT.lt (α := ℤ) 0 (↑k : ℤ)
i : ℤ := n % (↑k : ℤ)
i₀ : ℕ
hi₀ : (↑i₀ : ℤ) = i
refine_2 : HPow.hPow (β := ℤ) ζ (↑i₀ : ℤ) = ζ ^ n
refine_2₁ : ζ ^ i = ζ ^ n
refine_2₂ : ζ ^ i = ζ ^ (n % (↑k : ℤ) + (↑k : ℤ) * (n / (↑k : ℤ)))
refine_2₃ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * ζ ^ ((↑k : ℤ) * (n / (↑k : ℤ)))
refine_2₄ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * HPow.hPow (β := ℤ) ζ (↑k : ℤ) ^ (n / (↑k : ℤ))
refine_2₅ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * HPow.hPow (α := Rˣ) 1 (n / (↑k : ℤ))
refine_2₆ : ζ ^ i = ζ ^ (n % (↑k : ℤ)) * 1
⊢ ζ ^ i₀ = ζ ^ n
have refine_2₇ : ζ ^ i = ζ ^ (n % (↑k : ℤ))
Tactic: rw [← zpow_natCast, hi₀, ← Int.emod_add_mul_ediv n k, zpow_add, zpow_mul, h.zpow_eq_one,
      one_zpow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
hξ : ξ ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ
have lift : ∀ (ζ : Rˣ) (h : IsPrimitiveRoot (↑ζ : R) k), ∃ i < k, (↑ζ : R) ^ i = ξ
Tactic: lift ζ to Rˣ using h.isUnit NeZero.out
Cleared hypotheses: ζ, h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ξ : R
hξ : ξ ^ k = 1
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ : R) k
⊢ ∃ i < k, (↑ζ : R) ^ i = ξ
have lift : ∀ (ξ : Rˣ) (hξ : (↑ξ : R) ^ k = 1), ∃ i < k, (↑ζ : R) ^ i = (↑ξ : R)
Tactic: lift ξ to Rˣ using .of_pow_eq_one hξ <| NeZero.ne k
Cleared hypotheses: ξ, hξ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ : R) k
ξ : Rˣ
hξ : (↑ξ : R) ^ k = 1
⊢ ∃ i < k, (↑ζ : R) ^ i = (↑ξ : R)
have simp : ∃ i < k, ζ ^ i = ξ
Tactic: simp only [← Units.val_pow_eq_pow_val, ← Units.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ : R) k
ξ : Rˣ
hξ : (↑ξ : R) ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ
have rw : ∀ (h : IsPrimitiveRoot ζ k) (ξ : Rˣ) (hξ : (↑ξ : R) ^ k = 1), ∃ i < k, ζ ^ i = ξ
Tactic: rw [coe_units_iff] at h
Cleared hypotheses: h, ξ, hξ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
have mp : IsPrimitiveRoot ξ k → ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
mp : IsPrimitiveRoot ξ k → ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
⊢ IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
have mpr : (∃ i < k, i.Coprime k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ k
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : Rˣ
h : IsPrimitiveRoot ζ k
hξ : IsPrimitiveRoot ξ k
⊢ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
have mp : ∀ (i : ℕ) (hik : i < k) (hξ : IsPrimitiveRoot (ζ ^ i) k), ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i
Tactic: obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_mem_rootsOfUnity hξ.pow_eq_one
Cleared hypotheses: ξ, hξ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : IsPrimitiveRoot (ζ ^ i) k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i
have hξ₁ : i.Coprime k
Tactic: rw [h.pow_iff_coprime <| NeZero.pos k] at hξ
Cleared hypotheses: hξ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
have mp : IsPrimitiveRoot ξ k → ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
mp : IsPrimitiveRoot ξ k → ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
⊢ IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
have mpr : (∃ i < k, i.Coprime k ∧ ζ ^ i = ξ) → IsPrimitiveRoot ξ k
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
hξ : IsPrimitiveRoot ξ k
⊢ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
have mp : ∀ (i : ℕ) (hik : i < k) (hξ : IsPrimitiveRoot (ζ ^ i) k), ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i
Tactic: obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_pow_eq_one hξ.pow_eq_one
Cleared hypotheses: ξ, hξ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : R
h : IsPrimitiveRoot ζ k
i : ℕ
hik : i < k
hξ : IsPrimitiveRoot (ζ ^ i) k
⊢ ∃ i_1 < k, i_1.Coprime k ∧ ζ ^ i_1 = ζ ^ i
have hξ₁ : i.Coprime k
Tactic: rw [h.pow_iff_coprime <| NeZero.pos k] at hξ
Cleared hypotheses: hξ
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
have inl : ∀ (hζ : IsPrimitiveRoot ζ 0) (e : HPow.hPow (β := ℕ) α 0 = a),
  nthRoots 0 a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range 0)
Tactic: obtain (rfl | hn) := n.eq_zero_or_pos
Cleared hypotheses: n, hζ, e
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
inl :
  ∀ (hζ : IsPrimitiveRoot ζ 0) (e : HPow.hPow (β := ℕ) α 0 = a),
    nthRoots 0 a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range 0)
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
have inr : ∀ (hn : n > 0), nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
Tactic: obtain (rfl | hn) := n.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
have pos : ∀ (hα : α = 0), nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
Tactic: by_cases hα : α = 0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
pos : ∀ (hα : α = 0), nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
have neg : ∀ (hα : ¬α = 0), nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
Tactic: by_cases hα : α = 0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : α = 0
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
have e₁ : 0 = a
Tactic: rw [hα, zero_pow hn.ne'] at e
Cleared hypotheses: e, hn, hα
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ nthRoots n a = Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n)
have neg : Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) = nthRoots n a
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) = nthRoots n a
have neg : Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) ≤ nthRoots n a
Tactic: apply Multiset.eq_of_le_of_card_le
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
neg : Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) ≤ nthRoots n a
⊢ Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) = nthRoots n a
have neg₁ : (nthRoots n a).card ≤ Multiset.card.{u_4} (α := R) (Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n))
Tactic: apply Multiset.eq_of_le_of_card_le
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
⊢ Multiset.map (fun (x : ℕ) ↦ ζ ^ x * α) (Multiset.range n) ≤ nthRoots n a
have neg : val (image (fun (x : ℕ) ↦ ζ ^ x * α) (range n)) ⊆ nthRoots n a
Tactic: rw [← Finset.range_val,
      ← Finset.image_val_of_injOn (hζ.injOn_pow_mul hα), Finset.val_le_iff_val_subset]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
x : R
hx : Membership.mem (γ := Multiset R) (val (image (fun (x : ℕ) ↦ ζ ^ x * α) (range n))) x
⊢ x ∈ nthRoots n a
have hx₁ : ∃ a < n, ζ ^ a * α = x
Tactic: simp only [Finset.image_val, Finset.range_val, Multiset.mem_dedup, Multiset.mem_map,
      Multiset.mem_range] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
x : R
hx : ∃ a < n, ζ ^ a * α = x
⊢ x ∈ nthRoots n a
have neg : ∀ m < n, ζ ^ m * α ∈ nthRoots n a
Tactic: obtain ⟨m, _, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
m : ℕ
left : m < n
⊢ ζ ^ m * α ∈ nthRoots n a
have neg : (ζ ^ m * α) ^ n = a
Tactic: rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
m : ℕ
left : m < n
neg : (ζ ^ m * α) ^ n = a
⊢ ζ ^ m * α ∈ nthRoots n a
have neg₁ : (ζ ^ m) ^ n * α ^ n = a
Tactic: rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
m : ℕ
left : m < n
neg : (ζ ^ m * α) ^ n = a
neg₁ : (ζ ^ m) ^ n * α ^ n = a
⊢ ζ ^ m * α ∈ nthRoots n a
have neg₂ : (ζ ^ m) ^ n * a = a
Tactic: rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]