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
simp :
  Eq (α := Additive ↥(Subgroup.zpowers ζ))
    ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) 1 ⋯) :
      Additive ↥(Subgroup.zpowers ζ))
    (0 : Additive ↥(Subgroup.zpowers ζ))
⊢ Eq (α := Additive ↥(Subgroup.zpowers ζ))
    ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x)
          ((fun (x : ℤ) ↦ ζ ^ x) 0) ⋯) :
      Additive ↥(Subgroup.zpowers ζ))
    (0 : Additive ↥(Subgroup.zpowers ζ))

Tactic:
simp only [zpow_zero]

Premises used: zpow_zero
-- 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
⊢ Eq (α := Additive ↥(Subgroup.zpowers ζ))
    ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) 1 ⋯) :
      Additive ↥(Subgroup.zpowers ζ))
    (0 : Additive ↥(Subgroup.zpowers ζ))

Tactic:
rfl
-- 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 j : ℤ
simp :
  (Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
      (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i * ζ ^ j) ⋯) =
    HAdd.hAdd (α := Additive ↥(Subgroup.zpowers ζ)) (β := 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 ζ))
      ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ j) ⋯) :
        Additive ↥(Subgroup.zpowers ζ))
⊢ (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 + j)) ⋯) =
    HAdd.hAdd (α := Additive ↥(Subgroup.zpowers ζ))
      ((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) ⋯))
      ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
        (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x)
          ((fun (x : ℤ) ↦ ζ ^ x) j) ⋯))

Tactic:
simp only [zpow_add]

Premises used: zpow_add
-- 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 j : ℤ
⊢ (Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
      (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i * ζ ^ j) ⋯) =
    HAdd.hAdd (α := Additive ↥(Subgroup.zpowers ζ)) (β := 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 ζ))
      ((Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
          (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ j) ⋯) :
        Additive ↥(Subgroup.zpowers ζ))

Tactic:
rfl
-- 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 : ℤ
hi : i ∈ AddMonoidHom.ker (M := ZMod k) (Int.castAddHom (ZMod k))
⊢ (↑k : ℤ) ∣ i

Tactic:
simp only [AddMonoidHom.mem_ker, CharP.intCast_eq_zero_iff (ZMod k) k, AddMonoidHom.coe_mk,
          Int.coe_castAddHom] at hi ⊢

Premises used: AddMonoidHom.coe_mk, Int.coe_castAddHom, ZMod, AddMonoidHom.mem_ker, CharP.intCast_eq_zero_iff
-- 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 : ℤ
hi : (↑k : ℤ) ∣ i
obtain :
  ∀ (i : ℤ),
    Eq.{u_4 + 1} (α := Additive ↥(Subgroup.zpowers ζ))
      (({
              toFun := fun (i : ℤ) ↦
                (Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
                  (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯),
              map_zero' := ⋯ } :
            (a : ℤ) → Additive ↥(Subgroup.zpowers ζ))
          ((↑k : ℤ) * i) :
        Additive ↥(Subgroup.zpowers ζ))
      (0 : Additive ↥(Subgroup.zpowers ζ))
⊢ Eq.{u_4 + 1} (α := Additive ↥(Subgroup.zpowers ζ))
    (({
            toFun := fun (i : ℤ) ↦
              (Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
                (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯),
            map_zero' := ⋯ } :
          (a : ℤ) → Additive ↥(Subgroup.zpowers ζ))
        i :
      Additive ↥(Subgroup.zpowers ζ))
    (0 : Additive ↥(Subgroup.zpowers ζ))

Tactic:
obtain ⟨i, rfl⟩ := hi

Premises used: rfl
-- 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 : ℤ
⊢ Eq.{u_4 + 1} (α := Additive ↥(Subgroup.zpowers ζ))
    (({
            toFun := fun (i : ℤ) ↦
              (Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
                (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) (ζ ^ i) ⋯),
            map_zero' := ⋯ } :
          (a : ℤ) → Additive ↥(Subgroup.zpowers ζ))
        ((↑k : ℤ) * i) :
      Additive ↥(Subgroup.zpowers ζ))
    (0 : Additive ↥(Subgroup.zpowers ζ))

Tactic:
simp [zpow_mul, h.pow_eq_one, one_zpow, zpow_natCast]

Premises used: zpow_natCast, zpow_mul, one_zpow, IsPrimitiveRoot.pow_eq_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 R
ζ : Rˣ
h_1 h : IsPrimitiveRoot ζ k
left :
  ∀ (a : ZMod k),
    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 ζ))
            a :
          Additive ↥(Subgroup.zpowers ζ))
        (0 : Additive ↥(Subgroup.zpowers ζ)) →
      a = 0
⊢ Function.Injective.{1, u_4 + 1} (α := ZMod k) (β := 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 ζ))

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- 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 : ZMod k
hi :
  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 :
      Additive ↥(Subgroup.zpowers ζ))
    (0 : Additive ↥(Subgroup.zpowers ζ))
⊢ Eq.{u_4 + 1} (α := Rˣ)
    (↑((((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) :
      Rˣ)
    (↑0 : Rˣ)

Tactic:
rw [Subtype.ext_iff] at hi

Premises used: Subtype.ext_iff
-- 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 : ZMod k
hi :
  Eq.{u_4 + 1} (α := Rˣ)
    (↑((((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) :
      Rˣ)
    (↑0 : Rˣ)
⊢ Dvd.dvd (α := ℤ) (↑k : ℤ) i.cast

Tactic:
have := (h.zpow_eq_one_iff_dvd _).mp hi
-- 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 : ZMod k
hi :
  Eq.{u_4 + 1} (α := Rˣ)
    (↑((((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) :
      Rˣ)
    (↑0 : Rˣ)
this : Dvd.dvd (α := ℤ) (↑k : ℤ) i.cast
left : (↑i.cast : ZMod k) = i
⊢ i = 0

Tactic:
rw [← (CharP.intCast_eq_zero_iff (ZMod k) k _).mpr this, eq_comm]

Premises used: Iff.mpr, eq_comm, ZMod, CharP.intCast_eq_zero_iff
-- 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 : ZMod k
hi :
  Eq.{u_4 + 1} (α := Rˣ)
    (↑((((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) :
      Rˣ)
    (↑0 : Rˣ)
this : Dvd.dvd (α := ℤ) (↑k : ℤ) i.cast
⊢ (↑i.cast : ZMod k) = i

Tactic:
ZMod.intCast_rightInverse i

Premises used: ZMod.intCast_rightInverse
-- 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 : ZMod k
hi :
  Eq.{u_4 + 1} (α := Rˣ)
    (↑((((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) :
      Rˣ)
    (↑0 : Rˣ)
this : Dvd.dvd (α := ℤ) (↑k : ℤ) i.cast
⊢ (↑i.cast : ZMod k) = i

Tactic:
exact ZMod.intCast_rightInverse i

Premises used: ZMod.intCast_rightInverse
-- 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 : ℤ
⊢ ∃ (a : ZMod k),
    (((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 ζ))
        a =
      Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x)
        ((fun (x : ℤ) ↦ ζ ^ x) i) ⋯

Tactic:
⟨Int.castAddHom (ZMod k) i, ?_⟩

Premises used: ZMod, Int.castAddHom, Exists.intro, DFunLike.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 R
ζ : Rˣ
h_1 h : IsPrimitiveRoot ζ k
i : ℤ
right :
  (((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 ζ))
      ((Int.castAddHom (ZMod k) : (a : ℤ) → ZMod k) i : ZMod k) =
    Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) ((fun (x : ℤ) ↦ ζ ^ x) i)
      ⋯
⊢ ∃ (a : ZMod k),
    (((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 ζ))
        a =
      Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x)
        ((fun (x : ℤ) ↦ ζ ^ x) i) ⋯

Tactic:
refine ⟨Int.castAddHom (ZMod k) i, ?_⟩
-- 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 : ℤ
right :
  ((↑(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)
      ⋯
⊢ (((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 ζ))
      ((Int.castAddHom (ZMod k) : (a : ℤ) → ZMod k) i : ZMod k) =
    Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x) ((fun (x : ℤ) ↦ ζ ^ x) i)
      ⋯

Tactic:
rw [AddMonoidHom.liftOfRightInverse_comp_apply]

Premises used: AddMonoidHom.liftOfRightInverse_comp_apply