-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem pow_of_coprime (h : IsPrimitiveRoot ζ k) (i : ℕ) (hi : i.Coprime k) :
    IsPrimitiveRoot (ζ ^ i) k

Proof state:
case pos
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
h0 : k = 0
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
subst k

Result:
case pos
M : Type u_1
inst✝ : CommMonoid M
ζ : M
i : ℕ
h : IsPrimitiveRoot ζ 0
hi : i.Coprime 0
⊢ IsPrimitiveRoot (ζ ^ i) 0

Proof state:
case neg.intro
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ IsPrimitiveRoot (↑ζ ^ i) k

Tactic:
rw [← Units.val_pow_eq_pow_val]

Result:
case neg.intro
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ IsPrimitiveRoot (↑(ζ ^ i)) k

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ (ζ ^ i) ^ k = 1

Tactic:
rw [← pow_mul', pow_mul, h.pow_eq_one, one_pow]

Result:
no goals

Proof state:
case neg
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
rcases h.isUnit (Nat.pos_of_ne_zero h0) with ⟨ζ, rfl⟩

Result:
case neg.intro
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ IsPrimitiveRoot (↑ζ ^ i) k

Proof state:
case neg.intro
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ l = 1

Tactic:
rw [← pow_one ζ, ← zpow_natCast ζ, ← hi.gcd_eq_one, Nat.gcd_eq_gcd_ab, zpow_add, mul_pow,
  ← zpow_natCast, ← zpow_mul, mul_right_comm]

Result:
case neg.intro
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ (↑i * ↑l * i.gcdA k) * (ζ ^ (↑k * i.gcdB k)) ^ l = 1

Proof state:
case neg.intro
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
refine
  { pow_eq_one := by rw [← pow_mul', pow_mul, h.pow_eq_one, one_pow]
    dvd_of_pow_eq_one := fun l hl ↦ h.dvd_of_pow_eq_one l ?_ }

Result:
case neg.intro
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ l = 1

Proof state:
case neg.intro
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ (↑i * ↑l * i.gcdA k) * (ζ ^ (↑k * i.gcdB k)) ^ l = 1

Tactic:
simp only [zpow_mul, hl, h.pow_eq_one, one_zpow, one_pow, one_mul, zpow_natCast]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
by_cases h0 : k = 0

Result:
case pos
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
h0 : k = 0
⊢ IsPrimitiveRoot (ζ ^ i) k

case neg
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
⊢ IsPrimitiveRoot (ζ ^ i) k

Proof state:
case pos
M : Type u_1
inst✝ : CommMonoid M
ζ : M
i : ℕ
h : IsPrimitiveRoot ζ 0
hi : i.Coprime 0
⊢ IsPrimitiveRoot (ζ ^ i) 0

Tactic:
simp_all only [pow_one, Nat.coprime_zero_right]

Result:
no goals

Proof state:
case neg.intro
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ IsPrimitiveRoot (↑(ζ ^ i)) k

Tactic:
rw [coe_units_iff] at h ⊢

Result:
case neg.intro
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ IsPrimitiveRoot (ζ ^ i) k