awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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)
⊢ Eq (α := ZMod n)
    (↑(h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) :
      ZMod n)
    1
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
    (↑(h1.choose (p := fun (m : ℕ) ↦ ((↑1 : S →ₐ[R] S) : (a : S) → S) (↑(↑μ' : Sˣ) : S) = (↑(↑μ' : Sˣ) : S) ^ m)) :
      ZMod n)
    1
have h₁ : Eq (α := ZMod n) 1 (↑1 : ZMod n)
Tactic: convert! ho ▸ (ZMod.natCast_eq_natCast_iff ..).mpr (pow_eq_pow_iff_modEq.mp h).symm
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ (↑(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)
have 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)
Tactic: generalize_proofs hxy' hx' hy'
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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'.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)
have 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)
Tactic: have hxy := hxy'.choose_spec
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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)
⊢ (↑(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)
have 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)
Tactic: replace hxy : x (((μ' : Sˣ) : S) ^ hy'.choose) = ((μ' : Sˣ) : S) ^ hxy'.choose :=
          hy'.choose_spec ▸ hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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)
⊢ (↑(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)
have 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)
Tactic: rw [map_pow] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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)
⊢ (↑(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)
have 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)
Tactic: replace hxy : (((μ' : Sˣ) : S) ^ hx'.choose) ^ hy'.choose = ((μ' : Sˣ) : S) ^ hxy'.choose :=
          hx'.choose_spec ▸ hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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)
⊢ (↑(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)
have 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)
Tactic: rw [← pow_mul] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (hypothesis)
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)
⊢ (↑(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)
have 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)
Tactic: replace hxy : μ' ^ (hx'.choose * hy'.choose) = μ' ^ hxy'.choose :=
          rootsOfUnity.coe_injective (by simpa only [rootsOfUnity.coe_pow] using hxy)
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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)
⊢ (↑(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)
have 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)
Tactic: convert! ho ▸ (ZMod.natCast_eq_natCast_iff ..).mpr (pow_eq_pow_iff_modEq.mp hxy).symm
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ μ ^ 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) μ
have rw : μ ^
    ZMod.val (n := n)
      (↑(Exists.choose (p := fun (m : ℕ) ↦
            (f : (a : S) → S) (↑(↑hμ.toRootsOfUnity : Sˣ) : S) = (↑(↑hμ.toRootsOfUnity : Sˣ) : S) ^ m) sorry) :
        ZMod n) =
  (f : (a : S) → S) μ
Tactic: rw [IsPrimitiveRoot.coe_autToPow_apply]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ μ ^
      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) μ
have 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) μ
Tactic: generalize_proofs h
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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) μ
have 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)
Tactic: refine (?_ : ((hμ.toRootsOfUnity : Sˣ) : S) ^ _ = _).trans h.choose_spec.symm
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ (↑(↑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)
have 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)
Tactic: rw [← rootsOfUnity.coe_pow, ← rootsOfUnity.coe_pow]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ (↑(↑(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)
have 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)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
⊢ 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)
have 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]
Tactic: rw [pow_eq_pow_iff_modEq, ZMod.val_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
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
| 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]
have enter : n
Tactic: enter [2, 2]