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 h : IsPrimitiveRoot ζ k
i : ℤ
⊢ ((↑(Subtype.mk (p := fun (g : ℤ →+ Additive ↥(Subgroup.zpowers ζ)) ↦
              AddMonoidHom.ker (M := ZMod k) (Int.castAddHom (ZMod k)) ≤ g.ker)
              {
                toFun := fun (i : ℤ) ↦
                  (Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
                    (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x)
                      ((fun (x : ℤ) ↦ ζ ^ x) i) ⋯),
                map_zero' := ⋯, map_add' := ⋯ }
              ⋯) :
          ℤ →+ Additive ↥(Subgroup.zpowers ζ)) :
        (a : ℤ) → Additive ↥(Subgroup.zpowers ζ))
      i =
    Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) ((fun (x : ℤ) ↦ ζ ^ x) i)
      ⋯

Tactic:
rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℤ
⊢ Eq.{u_4 + 1} (α := Additive ↥(Subgroup.zpowers ζ))
    ((((AddMonoidHom.liftOfRightInverse (Int.castAddHom (ZMod k)) ZMod.cast ⋯ :
                (a : { g : ℤ →+ Additive ↥(Subgroup.zpowers ζ) // (Int.castAddHom (ZMod k)).ker ≤ g.ker }) →
                  ZMod k →+ Additive ↥(Subgroup.zpowers ζ))
              (Subtype.mk (p := fun (g : ℤ →+ Additive ↥(Subgroup.zpowers ζ)) ↦
                AddMonoidHom.ker (M := ZMod k) (Int.castAddHom (ZMod k)) ≤ g.ker)
                {
                  toFun := fun (i : ℤ) ↦
                    (Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
                      (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x)
                        ((fun (x : ℤ) ↦ ζ ^ x) i) ⋯),
                  map_zero' := ⋯, map_add' := ⋯ }
                ⋯) :
            ZMod k →+ Additive ↥(Subgroup.zpowers ζ)) :
          (a : ZMod k) → Additive ↥(Subgroup.zpowers ζ))
        (↑i : ZMod k) :
      Additive ↥(Subgroup.zpowers ζ))
    ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯) :
      Additive ↥(Subgroup.zpowers ζ))

Tactic:
AddMonoidHom.liftOfRightInverse_comp_apply _ _ ZMod.intCast_rightInverse _ _

Premises used: AddMonoidHom.liftOfRightInverse_comp_apply
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℤ
⊢ Eq.{u_4 + 1} (α := Additive ↥(Subgroup.zpowers ζ))
    ((((AddMonoidHom.liftOfRightInverse (Int.castAddHom (ZMod k)) ZMod.cast ⋯ :
                (a : { g : ℤ →+ Additive ↥(Subgroup.zpowers ζ) // (Int.castAddHom (ZMod k)).ker ≤ g.ker }) →
                  ZMod k →+ Additive ↥(Subgroup.zpowers ζ))
              (Subtype.mk (p := fun (g : ℤ →+ Additive ↥(Subgroup.zpowers ζ)) ↦
                AddMonoidHom.ker (M := ZMod k) (Int.castAddHom (ZMod k)) ≤ g.ker)
                {
                  toFun := fun (i : ℤ) ↦
                    (Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
                      (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x)
                        ((fun (x : ℤ) ↦ ζ ^ x) i) ⋯),
                  map_zero' := ⋯, map_add' := ⋯ }
                ⋯) :
            ZMod k →+ Additive ↥(Subgroup.zpowers ζ)) :
          (a : ZMod k) → Additive ↥(Subgroup.zpowers ζ))
        (↑i : ZMod k) :
      Additive ↥(Subgroup.zpowers ζ))
    ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯) :
      Additive ↥(Subgroup.zpowers ζ))

Tactic:
exact AddMonoidHom.liftOfRightInverse_comp_apply _ _ ZMod.intCast_rightInverse _ _

Premises used: AddMonoidHom.liftOfRightInverse_comp_apply
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ZMod k) (↑i : ZMod k) (↑i : ZMod k)
⊢ Eq (α := ZMod k) (↑i : ZMod k) (↑(↑i : ℤ) : ZMod k)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ Eq (α := ZMod k) (↑i : ZMod k) (↑(↑i : ℤ) : ZMod k)

Tactic:
have : (i : ZMod k) = (i : ℤ) := by norm_cast
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
this : Eq (α := ZMod k) (↑i : ZMod k) (↑(↑i : ℤ) : ZMod k)
⊢ Eq (α := Additive ↥(Subgroup.zpowers ζ))
    ((h.zmodEquivZPowers : (a : ZMod k) → Additive ↥(Subgroup.zpowers ζ)) (↑i : ZMod k) :
      Additive ↥(Subgroup.zpowers ζ))
    ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯) :
      Additive ↥(Subgroup.zpowers ζ))

Tactic:
simp only [this, zmodEquivZPowers_apply_coe_int, zpow_natCast]

Premises used: zpow_natCast, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℤ
rw :
  Eq (α := ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯)) :
      ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        ((h.zmodEquivZPowers : (a : ZMod k) → Additive ↥(Subgroup.zpowers ζ)) (↑i : ZMod k)) :
      ZMod k)
rw₁ rw₂ :
  Eq (α := ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯)) :
      ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯)) :
      ZMod k)
⊢ Eq (α := ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯)) :
      ZMod k)
    ((↑i : ZMod k) : ZMod k)

Tactic:
rw [← h.zmodEquivZPowers.symm_apply_apply i, zmodEquivZPowers_apply_coe_int]

Premises used: Int.cast, AddEquiv.symm_apply_apply, IsPrimitiveRoot.zmodEquivZPowers, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℤ
⊢ Eq (α := ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯) :
      ZMod k)
    ((↑i : ZMod k) : ZMod k)

Tactic:
h.zmodEquivZPowers_symm_apply_zpow i

Premises used: IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
rw :
  Eq (α := ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯)) :
      ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        ((h.zmodEquivZPowers : (a : ZMod k) → Additive ↥(Subgroup.zpowers ζ)) (↑i : ZMod k)) :
      ZMod k)
rw₁ rw₂ :
  Eq (α := ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯)) :
      ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯)) :
      ZMod k)
⊢ Eq (α := ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯)) :
      ZMod k)
    ((↑i : ZMod k) : ZMod k)

Tactic:
rw [← h.zmodEquivZPowers.symm_apply_apply i, zmodEquivZPowers_apply_coe_nat]

Premises used: AddEquiv.symm_apply_apply, IsPrimitiveRoot.zmodEquivZPowers, Nat.cast, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
k : ℕ
inst : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ Eq (α := ZMod k)
    ((h.zmodEquivZPowers.symm : (a : Additive ↥(Subgroup.zpowers ζ)) → ZMod k)
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯) :
      ZMod k)
    ((↑i : ZMod k) : ZMod k)

Tactic:
h.zmodEquivZPowers_symm_apply_pow i

Premises used: IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
a : (↑(Subgroup.zpowers ζ) : Set Rˣ) = (↑(rootsOfUnity k R : Subgroup Rˣ) : Set Rˣ)
⊢ Eq (α := Subgroup Rˣ) (Subgroup.zpowers ζ) (rootsOfUnity k R)

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
a :
  ∀ (F : Fintype ↥(Subgroup.zpowers ζ)), (↑(Subgroup.zpowers ζ) : Set Rˣ) = (↑(rootsOfUnity k R : Subgroup Rˣ) : Set Rˣ)
⊢ (↑(Subgroup.zpowers ζ) : Set Rˣ) = (↑(rootsOfUnity k R : Subgroup Rˣ) : Set Rˣ)

Tactic:
have F : Fintype (Subgroup.zpowers ζ) := Fintype.ofEquiv _ h.zmodEquivZPowers.toEquiv
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
F : Fintype ↥(Subgroup.zpowers ζ)
⊢ (↑(Subgroup.zpowers ζ) : Set Rˣ) = (↑(rootsOfUnity k R : Subgroup Rˣ) : Set Rˣ)

Tactic:
@Set.eq_of_subset_of_card_le Rˣ _ _ F (rootsOfUnity.fintype R k)
      (Subgroup.zpowers_le_of_mem <| show ζ ∈ rootsOfUnity k R from h.pow_eq_one) ?_

Premises used: Set.eq_of_subset_of_card_le, Subgroup.zpowers_le_of_mem, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
F : Fintype ↥(Subgroup.zpowers ζ)
a :
  Fintype.card.{u_4} (↑(↑(rootsOfUnity k R : Subgroup Rˣ) : Set Rˣ) : Type u_4) ≤
    Fintype.card.{u_4} (↑(↑(Subgroup.zpowers ζ) : Set Rˣ) : Type u_4)
⊢ (↑(Subgroup.zpowers ζ) : Set Rˣ) = (↑(rootsOfUnity k R : Subgroup Rˣ) : Set Rˣ)

Tactic:
refine
    @Set.eq_of_subset_of_card_le Rˣ _ _ F (rootsOfUnity.fintype R k)
      (Subgroup.zpowers_le_of_mem <| show ζ ∈ rootsOfUnity k R from h.pow_eq_one) ?_

Premises used: Set.eq_of_subset_of_card_le, Subgroup.zpowers_le_of_mem, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
F : Fintype ↥(Subgroup.zpowers ζ)
⊢ Fintype.card.{u_4} ↥(rootsOfUnity k R) ≤ k

Tactic:
card_rootsOfUnity R k

Premises used: card_rootsOfUnity
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
F : Fintype ↥(Subgroup.zpowers ζ)
⊢ k = Fintype.card (ZMod k)

Tactic:
(ZMod.card k).symm

Premises used: Eq.symm, ZMod.card
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
F : Fintype ↥(Subgroup.zpowers ζ)
⊢ Fintype.card (ZMod k) = Fintype.card.{u_4} ↥(Subgroup.zpowers ζ)

Tactic:
Fintype.card_congr h.zmodEquivZPowers.toEquiv

Premises used: Fintype.card_congr, IsPrimitiveRoot.zmodEquivZPowers, AddEquiv.toEquiv
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDomain R
k : ℕ
inst_2 : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
F : Fintype ↥(Subgroup.zpowers ζ)
⊢ Fintype.card.{u_4} (↑(↑(rootsOfUnity k R : Subgroup Rˣ) : Set Rˣ) : Type u_4) ≤
    Fintype.card.{u_4} (↑(↑(Subgroup.zpowers ζ) : Set Rˣ) : Type u_4)

Tactic:
calc
    Fintype.card (rootsOfUnity k R) ≤ k := card_rootsOfUnity R k
    _ = Fintype.card (ZMod k) := (ZMod.card k).symm
    _ = Fintype.card (Subgroup.zpowers ζ) := Fintype.card_congr h.zmodEquivZPowers.toEquiv

Premises used: Fintype.card_congr, Membership.mem, Fintype.card, Subtype, IsPrimitiveRoot.zmodEquivZPowers, rootsOfUnity, ZMod, Subgroup.zpowers, AddEquiv.toEquiv, card_rootsOfUnity, Eq.symm, ZMod.card
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
ζ : R
n : ℕ
inst_6 : NeZero n
hζ : IsPrimitiveRoot ζ n
f : F
hf : Function.Injective.{u_4 + 1, u_7 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this : CommMonoid Sˣ := inferInstance
⊢ IsPrimitiveRoot ⋯.unit n

Tactic:
replace hζ := hζ.isUnit_unit NeZero.out
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
ζ : R
n : ℕ
inst_6 : NeZero n
hζ_1 : IsPrimitiveRoot ζ n
f : F
hf : Function.Injective.{u_4 + 1, u_7 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this : CommMonoid Sˣ := inferInstance
hζ : IsPrimitiveRoot ⋯.unit n
rw : Eq (α := Subgroup Sˣ) (Subgroup.map (Units.map (↑f : R →* S)) (Subgroup.zpowers ⋯.unit)) (rootsOfUnity n S)
rw₁ :
  Eq (α := Subgroup Sˣ) (Subgroup.map (Units.map (↑f : R →* S)) (Subgroup.zpowers ⋯.unit))
    (Subgroup.zpowers (((Units.map (↑f : R →* S) : MonoidHom.{u_4, u_7} Rˣ Sˣ) : (a : Rˣ) → Sˣ) ⋯.unit))
rw₂ rw₃ :
  Eq.{u_7 + 1} (α := Subgroup Sˣ)
    (Subgroup.zpowers (((Units.map (↑f : R →* S) : MonoidHom.{u_4, u_7} Rˣ Sˣ) : (a : Rˣ) → Sˣ) ⋯.unit) : Subgroup Sˣ)
    (Subgroup.zpowers (((Units.map (↑f : R →* S) : MonoidHom.{u_4, u_7} Rˣ Sˣ) : (a : Rˣ) → Sˣ) ⋯.unit) : Subgroup Sˣ)
⊢ Eq (α := Subgroup Sˣ) (Subgroup.map (G := Rˣ) (Units.map (↑f : R →* S)) (rootsOfUnity n R)) (rootsOfUnity n S)

Tactic:
rw [← hζ.zpowers_eq,
    ← (hζ.map_of_injective (Units.map_injective (f := (f : R →* S)) hf)).zpowers_eq,
    MonoidHom.map_zpowers]

Premises used: Units.map_injective, IsPrimitiveRoot.zpowers_eq, IsPrimitiveRoot.map_of_injective, MonoidHom.map_zpowers
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 S)
obtain :
  ∀ (ε : ↥(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)
⊢ (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))
                η) :
            Rˣ) :
        R) =
    (↑(↑η : Sˣ) : S)

Tactic:
obtain ⟨ε, rfl⟩ := (rootsOfUnityEquivOfPrimitiveRoots hf hζ).surjective η

Premises used: MulEquiv.surjective, rootsOfUnityEquivOfPrimitiveRoots, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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)
rw₁ rw₂ : Eq.{u_7 + 1} (α := S) ((f : (a : R) → S) (↑(↑ε : Rˣ) : R) : S) ((f : (a : R) → S) (↑(↑ε : Rˣ) : R) : 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)

Tactic:
rw [MulEquiv.symm_apply_apply, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe]

Premises used: val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe, MulEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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) ξ
rwa rwa₁ rwa₂ rwa₃ : ∀ (hξ : Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) ξ), ∃ (n : ℤ), ζ ^ n = ξ
⊢ ∃ (n : ℤ), ζ ^ n = ξ

Tactic:
rwa [← h.zpowers_eq] at hξ

Premises used: IsPrimitiveRoot.zpowers_eq
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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) ξ
obtain : ∀ (n : ℤ) (hξ : Membership.mem (γ := Subgroup Rˣ) (rootsOfUnity k R) (ζ ^ n)), ∃ i < k, ζ ^ i = ζ ^ n
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
obtain ⟨n, rfl⟩ : ∃ n : ℤ, ζ ^ n = ξ := by rwa [← h.zpowers_eq] at hξ

Premises used: rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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)
⊢ LT.lt (α := ℤ) 0 (↑k : ℤ)

Tactic:
have hk0 : (0 : ℤ) < k := mod_cast NeZero.pos k
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 : ℤ)
⊢ 0 ≤ i

Tactic:
have hi0 : 0 ≤ i := Int.emod_nonneg _ (ne_of_gt hk0)
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
⊢ 0 ≤ i

Tactic:
hi0
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
lift : ∀ (i₀ : ℕ) (hi₀ : (↑i₀ : ℤ) = i), ∃ i < k, ζ ^ i = ζ ^ n
⊢ ∃ i < k, ζ ^ i = ζ ^ n

Tactic:
lift i to ℕ using hi0 with i₀ hi₀
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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

Tactic:
⟨i₀, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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
refine_2 : ζ ^ i₀ = ζ ^ n
⊢ ∃ i < k, ζ ^ i = ζ ^ n

Tactic:
refine ⟨i₀, ?_, ?_⟩
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 : LT.lt (α := ℤ) (↑i₀ : ℤ) (↑k : ℤ)
⊢ i₀ < k

Tactic:
zify
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 : ℤ)
⊢ LT.lt (α := ℤ) (↑i₀ : ℤ) (↑k : ℤ)

Tactic:
rw [hi₀]
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 : ℤ)

Tactic:
Int.emod_lt_of_pos _ hk0

Premises used: Int.emod_lt_of_pos
-- Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
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 : ℤ)

Tactic:
exact Int.emod_lt_of_pos _ hk0

Premises used: Int.emod_lt_of_pos