awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing R
ζ : Rˣ
h_1 : IsPrimitiveRoot ζ k
inst_4 : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
hr : 0 < n
⊢ a.Coprime n

Tactic:
simpa [(a.gcd_dvd_left n).trans] using h.dvd_iff (Nat.gcd_dvd_right a n)

Premises used: Nat.gcd_dvd_left, Nat.ModEq.dvd_iff, Nat.gcd_dvd_right, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing R
ζ : Rˣ
h_1 : IsPrimitiveRoot ζ k
inst_4 : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
hr : 0 < n
⊢ b.Coprime n

Tactic:
simpa [(b.gcd_dvd_left n).trans] using h.dvd_iff (Nat.gcd_dvd_right b n)

Premises used: Nat.gcd_dvd_left, Nat.ModEq.dvd_iff, Nat.gcd_dvd_right, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing R
ζ : Rˣ
h_1 : IsPrimitiveRoot ζ k
inst_4 : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
a₁ :
  (↑((fun (x : ↥(primitiveRoots n R)) ↦
            (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ b) ⋯ : ↥(primitiveRoots n R)))
          ((fun (x : ↥(primitiveRoots n R)) ↦
              (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ a) ⋯ : ↥(primitiveRoots n R)))
            x)) :
      R) =
    (↑x : R)
⊢ (fun (x : ↥(primitiveRoots n R)) ↦
        (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ b) ⋯ : ↥(primitiveRoots n R)))
      ((fun (x : ↥(primitiveRoots n R)) ↦
          (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ a) ⋯ : ↥(primitiveRoots n R)))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing R
ζ : Rˣ
h_1 : IsPrimitiveRoot ζ k
inst_4 : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
⊢ (↑((fun (x : ↥(primitiveRoots n R)) ↦
            (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ b) ⋯ : ↥(primitiveRoots n R)))
          ((fun (x : ↥(primitiveRoots n R)) ↦
              (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ a) ⋯ : ↥(primitiveRoots n R)))
            x)) :
      R) =
    (↑x : R)

Tactic:
simp [← pow_mul,
    pow_eq_pow_of_modEq h (isPrimitiveRoot_of_mem_primitiveRoots x.2).pow_eq_one]

Premises used: pow_mul, isPrimitiveRoot_of_mem_primitiveRoots, IsPrimitiveRoot.pow_eq_one, pow_eq_pow_of_modEq, Subtype.property
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing R
ζ : Rˣ
h_1 : IsPrimitiveRoot ζ k
inst_4 : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
a₁ :
  (↑((fun (x : ↥(primitiveRoots n R)) ↦
            (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ a) ⋯ : ↥(primitiveRoots n R)))
          ((fun (x : ↥(primitiveRoots n R)) ↦
              (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ b) ⋯ : ↥(primitiveRoots n R)))
            x)) :
      R) =
    (↑x : R)
⊢ (fun (x : ↥(primitiveRoots n R)) ↦
        (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ a) ⋯ : ↥(primitiveRoots n R)))
      ((fun (x : ↥(primitiveRoots n R)) ↦
          (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ b) ⋯ : ↥(primitiveRoots n R)))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing R
ζ : Rˣ
h_1 : IsPrimitiveRoot ζ k
inst_4 : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
⊢ (↑((fun (x : ↥(primitiveRoots n R)) ↦
            (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ a) ⋯ : ↥(primitiveRoots n R)))
          ((fun (x : ↥(primitiveRoots n R)) ↦
              (Subtype.mk (p := fun (x : R) ↦ x ∈ primitiveRoots n R) ((↑x : R) ^ b) ⋯ : ↥(primitiveRoots n R)))
            x)) :
      R) =
    (↑x : R)

Tactic:
simp [← pow_mul, mul_comm b,
    pow_eq_pow_of_modEq h (isPrimitiveRoot_of_mem_primitiveRoots x.2).pow_eq_one]

Premises used: pow_mul, mul_comm, isPrimitiveRoot_of_mem_primitiveRoots, IsPrimitiveRoot.pow_eq_one, pow_eq_pow_of_modEq, Subtype.property
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing R
ζ : Rˣ
h_1 : IsPrimitiveRoot ζ k
inst_4 : IsDomain R
a n : ℕ
h : a.Coprime n
inst_5 : NeZero n
h2 : ∃ m < n, a * m % n = 1 % n
⊢ a * h2.choose (p := fun (m : ℕ) ↦ m < n ∧ a * m % n = 1 % n) ≡ 1 [MOD n]

Tactic:
grind [Nat.ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k l : ℕ
h : k ≠ l
⊢ Disjoint (primitiveRoots k R) (primitiveRoots l R)

Tactic:
Finset.disjoint_left.2 fun _ hk hl ↦
    h <|
      (isPrimitiveRoot_of_mem_primitiveRoots hk).unique <| isPrimitiveRoot_of_mem_primitiveRoots hl

Premises used: Iff.mpr, IsPrimitiveRoot.unique, isPrimitiveRoot_of_mem_primitiveRoots, Finset.disjoint_left
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
inst_3 : NeZero n
h :
  ∀ (x : R),
    Membership.mem (γ := Finset R) (nthRootsFinset n 1) x ↔
      Membership.mem (γ := Finset R) (n.divisors.biUnion fun (i : ℕ) ↦ primitiveRoots i R) x
⊢ Eq.{u_4 + 1} (α := Finset R) (nthRootsFinset n 1) (n.divisors.biUnion fun (i : ℕ) ↦ primitiveRoots i R)

Tactic:
ext x
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
inst_3 : NeZero n
x : R
this : x ^ n = 1 ↔ ∃ (a : ℕ), a ∣ n ∧ x ∈ primitiveRoots a R
⊢ Membership.mem (γ := Finset R) (nthRootsFinset n 1) x ↔
    Membership.mem (γ := Finset R) (n.divisors.biUnion fun (i : ℕ) ↦ primitiveRoots i R) x

Tactic:
simpa [Polynomial.mem_nthRootsFinset (NeZero.pos n), (NeZero.ne n)]

Premises used: NeZero.pos, NeZero.ne, Polynomial.mem_nthRootsFinset
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
inst_3 : NeZero n
x : R
h : x ^ n = 1 ↔ ∃ (a : ℕ), a ∣ n ∧ x ∈ primitiveRoots a R
⊢ Membership.mem (γ := Finset R) (nthRootsFinset n 1) x ↔
    Membership.mem (γ := Finset R) (n.divisors.biUnion fun (i : ℕ) ↦ primitiveRoots i R) x

Tactic:
suffices x ^ n = 1 ↔ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R by
    simpa [Polynomial.mem_nthRootsFinset (NeZero.pos n), (NeZero.ne n)]
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
inst_3 : NeZero n
x : R
h : x ^ n = 1 → ∃ (a : ℕ), a ∣ n ∧ x ∈ primitiveRoots a R
h₁ : (∃ (a : ℕ), a ∣ n ∧ x ∈ primitiveRoots a R) → x ^ n = 1
⊢ x ^ n = 1 ↔ ∃ (a : ℕ), a ∣ n ∧ x ∈ primitiveRoots a R

Tactic:
constructor
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
inst_3 : NeZero n
x : R
H : x ^ n = 1
h : ∀ (k : ℕ) (hk : k > 0) (hx : IsPrimitiveRoot x k), ∃ (a : ℕ), a ∣ n ∧ x ∈ primitiveRoots a R
⊢ ∃ (a : ℕ), a ∣ n ∧ x ∈ primitiveRoots a R

Tactic:
obtain ⟨k, hk, hx⟩ := exists_pos H (NeZero.ne n)

Premises used: IsPrimitiveRoot.exists_pos, NeZero.ne
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
inst_3 : NeZero n
x : R
H : x ^ n = 1
k : ℕ
hk : k > 0
hx : IsPrimitiveRoot x k
⊢ ∃ (a : ℕ), a ∣ n ∧ x ∈ primitiveRoots a R

Tactic:
⟨k, hx.2 _ H, (mem_primitiveRoots hk).mpr hx⟩

Premises used: Iff.mpr, And.intro, mem_primitiveRoots, Exists.intro, IsPrimitiveRoot.dvd_of_pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
inst_3 : NeZero n
x : R
H : x ^ n = 1
k : ℕ
hk : k > 0
hx : IsPrimitiveRoot x k
⊢ ∃ (a : ℕ), a ∣ n ∧ x ∈ primitiveRoots a R

Tactic:
exact ⟨k, hx.2 _ H, (mem_primitiveRoots hk).mpr hx⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
inst_3 : NeZero n
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : n = a * d
ha₀ : a = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
inst_3 : NeZero n
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : n = a * d
⊢ 0 < a

Tactic:
have hazero : 0 < a := Nat.pos_of_ne_zero fun ha₀ ↦ by simp_all
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
inst_3 : NeZero n
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : n = a * d
hazero : 0 < a
h : ∀ (ha : IsPrimitiveRoot x a) (d : ℕ) (hd : n = a * d) (hazero : 0 < a), x ^ n = 1
⊢ x ^ n = 1

Tactic:
rw [mem_primitiveRoots hazero] at ha

Premises used: mem_primitiveRoots
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
inst_3 : NeZero n
x : R
a : ℕ
ha : IsPrimitiveRoot x a
d : ℕ
hd : n = a * d
hazero : 0 < a
h : x ^ (a * d) = 1
h₁ : (x ^ a) ^ d = 1
h₂ : HPow.hPow (α := R) 1 d = 1
h₃ h₄ : Eq.{u_4 + 1} (α := R) 1 1
⊢ x ^ n = 1

Tactic:
rw [hd, pow_mul, ha.pow_eq_one, one_pow]

Premises used: one_pow, pow_mul, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
pos :
  ∀ (hn : n = 0),
    Eq.{u_4 + 1} (α := Finset R) (nthRootsFinset n 1) (n.divisors.biUnion fun (i : ℕ) ↦ primitiveRoots i R)
neg :
  ∀ (hn : ¬n = 0),
    Eq.{u_4 + 1} (α := Finset R) (nthRootsFinset n 1) (n.divisors.biUnion fun (i : ℕ) ↦ primitiveRoots i R)
⊢ Eq.{u_4 + 1} (α := Finset R) (nthRootsFinset n 1) (n.divisors.biUnion fun (i : ℕ) ↦ primitiveRoots i R)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
hn : n = 0
⊢ Eq.{u_4 + 1} (α := Finset R) (nthRootsFinset n 1) (n.divisors.biUnion fun (i : ℕ) ↦ primitiveRoots i R)

Tactic:
simp only [hn, nthRootsFinset_zero, Nat.divisors_zero, biUnion_empty]

Premises used: Finset.biUnion_empty, Polynomial.nthRootsFinset_zero, Nat.divisors_zero
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
hn : ¬n = 0
⊢ NeZero n

Tactic:
have : NeZero n := ⟨hn⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
hn : ¬n = 0
this : NeZero n
⊢ Eq.{u_4 + 1} (α := Finset R) (nthRootsFinset n 1) (n.divisors.biUnion fun (i : ℕ) ↦ primitiveRoots i R)

Tactic:
nthRoots_one_eq_biUnion_primitiveRoots'

Premises used: _private.0.IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
hn : ¬n = 0
this : NeZero n
⊢ Eq.{u_4 + 1} (α := Finset R) (nthRootsFinset n 1) (n.divisors.biUnion fun (i : ℕ) ↦ primitiveRoots i R)

Tactic:
exact nthRoots_one_eq_biUnion_primitiveRoots'

Premises used: _private.0.IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
⊢ orderOf μ' = n

Tactic:
Eq.trans ?_ hμ.eq_orderOf.symm

Premises used: IsPrimitiveRoot.eq_orderOf, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
refine : orderOf μ' = orderOf μ
⊢ orderOf μ' = n

Tactic:
refine Eq.trans ?_ hμ.eq_orderOf.symm

Premises used: IsPrimitiveRoot.eq_orderOf, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
rw : orderOf μ' = orderOf (↑(↑hμ.toRootsOfUnity : Sˣ) : S)
rw₁ : orderOf μ' = orderOf (↑hμ.toRootsOfUnity : Sˣ)
rw₂ rw₃ : orderOf μ' = orderOf hμ.toRootsOfUnity
⊢ orderOf μ' = orderOf μ

Tactic:
rw [← hμ.val_toRootsOfUnity_coe, orderOf_units, Subgroup.orderOf_coe]

Premises used: IsPrimitiveRoot.val_toRootsOfUnity_coe, orderOf_units, Subgroup.orderOf_coe
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
⊢ ∃ (m : ℕ), ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m

Tactic:
generalize_proofs h1
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
h1 : ∃ (m : ℕ), ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m
⊢ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) =
    (↑(↑μ' : Sˣ) : S) ^
      h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)

Tactic:
have h := h1.choose_spec
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
h1 : ∃ (m : ℕ), ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m
h :
  ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) =
    (↑(↑μ' : Sˣ) : S) ^
      h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
⊢ Eq.{u_5 + 1} (α := S) ((fun (x : ↥(rootsOfUnity n S)) ↦ (↑(↑x : Sˣ) : S)) μ')
    ((fun (x : ↥(rootsOfUnity n S)) ↦ (↑(↑x : Sˣ) : S))
      (μ' ^ h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)))

Tactic:
simpa only [rootsOfUnity.coe_pow] using h

Premises used: rootsOfUnity.coe_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
h1 : ∃ (m : ℕ), ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m
h :
  ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) =
    (↑(↑μ' : Sˣ) : S) ^
      h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
⊢ μ' = μ' ^ h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)

Tactic:
replace h : μ' = μ' ^ h1.choose :=
          rootsOfUnity.coe_injective (by simpa only [rootsOfUnity.coe_pow] using h)
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
h1 : ∃ (m : ℕ), ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m
h : μ' = μ' ^ h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
⊢ HPow.hPow (β := ℕ) μ' 1 =
    μ' ^ h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)

Tactic:
nth_rw 1 [← pow_one μ'] at h

Premises used: pow_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
h1 : ∃ (m : ℕ), ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m
h :
  HPow.hPow (β := ℕ) μ' 1 =
    μ' ^ h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
h₁ : Eq (α := ZMod n) 1 (↑1 : ZMod n)
⊢ Eq (α := ZMod n)
    (↑(h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) :
      ZMod n)
    1

Tactic:
convert! ho ▸ (ZMod.natCast_eq_natCast_iff ..).mpr (pow_eq_pow_iff_modEq.mp h).symm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
h1 : ∃ (m : ℕ), ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m
h :
  HPow.hPow (β := ℕ) μ' 1 =
    μ' ^ h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
⊢ Eq (α := ZMod n) 1 (↑1 : ZMod n)

Tactic:
Nat.cast_one.symm

Premises used: Eq.symm, Nat.cast_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
h1 : ∃ (m : ℕ), ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m
h :
  HPow.hPow (β := ℕ) μ' 1 =
    μ' ^ h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
⊢ Eq (α := ZMod n) 1 (↑1 : ZMod n)

Tactic:
exact Nat.cast_one.symm

Premises used: Eq.symm, Nat.cast_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
x y : S ≃ₐ[R] S
generalize_proofs :
  ∀ (hxy' : ∃ (m : ℕ), ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
    (hx' : ∃ (m : ℕ), ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
    (hy' : ∃ (m : ℕ), ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m),
    (↑(hxy'.choose (p := fun (m : ℕ) ↦
            ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) :
        ZMod n) =
      HMul.hMul (α := ZMod n)
        (↑(hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) :
          ZMod n)
        (↑(hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) :
          ZMod n)
⊢ (↑(Exists.choose (p := fun (m : ℕ) ↦ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
          ⋯) :
      ZMod n) =
    HMul.hMul (α := ZMod n)
      (↑(Exists.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
            ⋯) :
        ZMod n)
      (↑(Exists.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
            ⋯) :
        ZMod n)

Tactic:
generalize_proofs hxy' hx' hy'
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing S
inst_4 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_5 : CommRing R
inst_6 : Algebra R S
inst_7 : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
ho : orderOf μ' = n
x y : S ≃ₐ[R] S
hxy' : ∃ (m : ℕ), ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m
hx' : ∃ (m : ℕ), ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m
hy' : ∃ (m : ℕ), ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m
⊢ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) =
    (↑(↑μ' : Sˣ) : S) ^
      hxy'.choose (p := fun (m : ℕ) ↦ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)

Tactic:
have hxy := hxy'.choose_spec