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 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
hxy :
  ((↑(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)
⊢ (x : (a : S) → S)
      ((↑(↑μ' : Sˣ) : S) ^
        hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) =
    (↑(↑μ' : Sˣ) : S) ^
      hxy'.choose (p := fun (m : ℕ) ↦ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)

Tactic:
replace hxy : x (((μ' : Sˣ) : S) ^ hy'.choose) = ((μ' : Sˣ) : S) ^ hxy'.choose :=
          hy'.choose_spec ▸ hxy
-- 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
hxy :
  (x : (a : S) → S)
      ((↑(↑μ' : Sˣ) : S) ^
        hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) =
    (↑(↑μ' : Sˣ) : S) ^
      hxy'.choose (p := fun (m : ℕ) ↦ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
⊢ HPow.hPow (α := S) ((x : (a : S) → S) (↑(↑μ' : Sˣ) : S) : S)
      (hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) =
    (↑(↑μ' : Sˣ) : S) ^
      hxy'.choose (p := fun (m : ℕ) ↦ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)

Tactic:
rw [map_pow] at hxy

Premises used: map_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
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
hxy :
  HPow.hPow (α := S) ((x : (a : S) → S) (↑(↑μ' : Sˣ) : S) : S)
      (hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) =
    (↑(↑μ' : Sˣ) : S) ^
      hxy'.choose (p := fun (m : ℕ) ↦ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
⊢ ((↑(↑μ' : Sˣ) : S) ^
        hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) ^
      hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) =
    (↑(↑μ' : Sˣ) : S) ^
      hxy'.choose (p := fun (m : ℕ) ↦ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)

Tactic:
replace hxy : (((μ' : Sˣ) : S) ^ hx'.choose) ^ hy'.choose = ((μ' : Sˣ) : S) ^ hxy'.choose :=
          hx'.choose_spec ▸ hxy
-- 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
hxy :
  ((↑(↑μ' : Sˣ) : S) ^
        hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) ^
      hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) =
    (↑(↑μ' : Sˣ) : S) ^
      hxy'.choose (p := fun (m : ℕ) ↦ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
⊢ (↑(↑μ' : Sˣ) : S) ^
      (hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) *
        hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) =
    (↑(↑μ' : Sˣ) : S) ^
      hxy'.choose (p := fun (m : ℕ) ↦ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)

Tactic:
rw [← pow_mul] at hxy

Premises used: pow_mul
-- 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
hxy :
  (↑(↑μ' : Sˣ) : S) ^
      (hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) *
        hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) =
    (↑(↑μ' : Sˣ) : S) ^
      hxy'.choose (p := fun (m : ℕ) ↦ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
⊢ Eq.{u_5 + 1} (α := S)
    ((fun (x : ↥(rootsOfUnity n S)) ↦ (↑(↑x : Sˣ) : S))
      (μ' ^
        (hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) *
          hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m))))
    ((fun (x : ↥(rootsOfUnity n S)) ↦ (↑(↑x : Sˣ) : S))
      (μ' ^
        hxy'.choose (p := fun (m : ℕ) ↦
          ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)))

Tactic:
simpa only [rootsOfUnity.coe_pow] using hxy

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
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
hxy :
  (↑(↑μ' : Sˣ) : S) ^
      (hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) *
        hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) =
    (↑(↑μ' : Sˣ) : S) ^
      hxy'.choose (p := fun (m : ℕ) ↦ ((↑(x * y) : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)
⊢ μ' ^
      (hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) *
        hy'.choose (p := fun (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)

Tactic:
replace hxy : μ' ^ (hx'.choose * hy'.choose) = μ' ^ hxy'.choose :=
          rootsOfUnity.coe_injective (by simpa only [rootsOfUnity.coe_pow] using hxy)
-- 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
hxy :
  μ' ^
      (hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) *
        hy'.choose (p := fun (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)
h :
  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) =
    (↑(hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) *
          hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) :
      ZMod n)
⊢ (↑(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)

Tactic:
convert! ho ▸ (ZMod.natCast_eq_natCast_iff ..).mpr (pow_eq_pow_iff_modEq.mp hxy).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
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
hxy :
  μ' ^
      (hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) *
        hy'.choose (p := fun (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)
⊢ 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) =
    (↑(hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) *
          hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) :
      ZMod n)

Tactic:
(Nat.cast_mul ..).symm

Premises used: Nat.cast_mul, Eq.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
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
hxy :
  μ' ^
      (hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) *
        hy'.choose (p := fun (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)
⊢ 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) =
    (↑(hx'.choose (p := fun (m : ℕ) ↦ ((↑x : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m) *
          hy'.choose (p := fun (m : ℕ) ↦ ((↑y : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) :
      ZMod n)

Tactic:
exact (Nat.cast_mul ..).symm

Premises used: Nat.cast_mul, Eq.symm
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
⊢ Eq (α := ZMod n) (↑(((autToPow R hμ : (S ≃ₐ[R] S) →* (ZMod n)ˣ) : (a : S ≃ₐ[R] S) → (ZMod n)ˣ) f) : ZMod n)
    (↑(Exists.choose (p := fun (m : ℕ) ↦
          (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) ⋯) :
      ZMod n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
rw :
  μ ^
      ZMod.val (n := n)
        (↑(Exists.choose (p := fun (m : ℕ) ↦
              (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) ⋯) :
          ZMod n) =
    (f : (a : S) → S) μ
⊢ μ ^ ZMod.val (n := n) (↑(((autToPow R hμ : (S ≃ₐ[R] S) →* (ZMod n)ˣ) : (a : S ≃ₐ[R] S) → (ZMod n)ˣ) f) : ZMod n) =
    (f : (a : S) → S) μ

Tactic:
rw [IsPrimitiveRoot.coe_autToPow_apply]

Premises used: IsPrimitiveRoot.coe_autToPow_apply
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
generalize_proofs :
  ∀ (h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m),
    μ ^
        ZMod.val (n := n)
          (↑(h.choose (p := fun (m : ℕ) ↦
                (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)) :
            ZMod n) =
      (f : (a : S) → S) μ
⊢ μ ^
      ZMod.val (n := n)
        (↑(Exists.choose (p := fun (m : ℕ) ↦
              (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) ⋯) :
          ZMod n) =
    (f : (a : S) → S) μ

Tactic:
generalize_proofs h
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m
⊢ μ ^
      ZMod.val (n := n)
        (↑(h.choose (p := fun (m : ℕ) ↦
              (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)) :
          ZMod n) =
    (f : (a : S) → S) μ

Tactic:
(?_ : ((hμ.toRootsOfUnity : Sˣ) : S) ^ _ = _).trans h.choose_spec.symm

Premises used: Exists.choose_spec, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m
refine :
  (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^
      ZMod.val (n := n)
        (↑(h.choose (p := fun (m : ℕ) ↦
              (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)) :
          ZMod n) =
    (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^
      h.choose (p := fun (m : ℕ) ↦
        (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)
⊢ μ ^
      ZMod.val (n := n)
        (↑(h.choose (p := fun (m : ℕ) ↦
              (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)) :
          ZMod n) =
    (f : (a : S) → S) μ

Tactic:
refine (?_ : ((hμ.toRootsOfUnity : Sˣ) : S) ^ _ = _).trans h.choose_spec.symm

Premises used: Exists.choose_spec, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m
rw :
  (↑(↑(hμ.toRootsOfUnity ^
              ZMod.val (n := n)
                (↑(h.choose (p := fun (m : ℕ) ↦
                      (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)) :
                  ZMod n)) :
          Sˣ) :
      S) =
    (↑(↑(hμ.toRootsOfUnity ^
              h.choose (p := fun (m : ℕ) ↦
                (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)) :
          Sˣ) :
      S)
⊢ (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^
      ZMod.val (n := n)
        (↑(h.choose (p := fun (m : ℕ) ↦
              (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)) :
          ZMod n) =
    (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^
      h.choose (p := fun (m : ℕ) ↦
        (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)

Tactic:
rw [← rootsOfUnity.coe_pow, ← rootsOfUnity.coe_pow]

Premises used: rootsOfUnity.coe_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m
e_self :
  hμ.toRootsOfUnity ^
      ZMod.val (n := n)
        (↑(h.choose (p := fun (m : ℕ) ↦
              (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)) :
          ZMod n) =
    hμ.toRootsOfUnity ^
      h.choose (p := fun (m : ℕ) ↦
        (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)
⊢ (↑(↑(hμ.toRootsOfUnity ^
              ZMod.val (n := n)
                (↑(h.choose (p := fun (m : ℕ) ↦
                      (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)) :
                  ZMod n)) :
          Sˣ) :
      S) =
    (↑(↑(hμ.toRootsOfUnity ^
              h.choose (p := fun (m : ℕ) ↦
                (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)) :
          Sˣ) :
      S)

Tactic:
congr 2
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m
e_self :
  h.choose (p := fun (m : ℕ) ↦
        (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) %
      n ≡
    h.choose (p := fun (m : ℕ) ↦
      (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) [MOD
    orderOf hμ.toRootsOfUnity]
⊢ hμ.toRootsOfUnity ^
      ZMod.val (n := n)
        (↑(h.choose (p := fun (m : ℕ) ↦
              (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)) :
          ZMod n) =
    hμ.toRootsOfUnity ^
      h.choose (p := fun (m : ℕ) ↦
        (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m)

Tactic:
rw [pow_eq_pow_iff_modEq, ZMod.val_natCast]

Premises used: pow_eq_pow_iff_modEq, ZMod.val_natCast
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m
enter : n
| h.choose (p := fun (m : ℕ) ↦
        (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) %
      n ≡
    h.choose (p := fun (m : ℕ) ↦
      (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) [MOD
    orderOf hμ.toRootsOfUnity]

Tactic:
enter [2, 2]
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
S : Type u_5
inst : CommRing S
inst_1 : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst_2 : CommRing R
inst_3 : Algebra R S
inst_4 : NeZero n
f : S ≃ₐ[R] S
h : ∃ (m : ℕ), (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m
rw : orderOf μ
| n

Tactic:
rw [hμ.eq_orderOf]

Premises used: IsPrimitiveRoot.eq_orderOf