-- Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
theorem cyclotomic_mul_prime_eq_pow_of_not_dvd (R : Type*) {p n : ℕ} [hp : Fact (Nat.Prime p)]
    [Ring R] [CharP R p] (hn : ¬p ∣ n) : cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)

Proof state:
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (fun x => cyclotomic n (ZMod p) * x) (cyclotomic (n * p) (ZMod p)) =
    (fun x => cyclotomic n (ZMod p) * x) (cyclotomic n (ZMod p) ^ (p - 1))

Tactic:
dsimp

Result:
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic n (ZMod p) * cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) * cyclotomic n (ZMod p) ^ (p - 1)

Proof state:
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic n (ZMod p) * cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) * cyclotomic n (ZMod p) ^ (p - 1)

Tactic:
rw [← pow_succ', tsub_add_cancel_of_le hp.out.one_lt.le, mul_comm, ← ZMod.expand_card]

Result:
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) = (expand (ZMod p) p) (cyclotomic n (ZMod p))

Proof state:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this✝ : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1)
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)

Tactic:
rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
  this, Polynomial.map_pow]

Result:
no goals

Proof state:
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) = (expand (ZMod p) p) (cyclotomic n (ZMod p))

Tactic:
conv_rhs => rw [← map_cyclotomic_int]

Result:
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) =
    (expand (ZMod p) p) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))

Proof state:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1)

Tactic:
apply mul_right_injective₀ (cyclotomic_ne_zero n <| ZMod p)

Result:
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (fun x => cyclotomic n (ZMod p) * x) (cyclotomic (n * p) (ZMod p)) =
    (fun x => cyclotomic n (ZMod p) * x) (cyclotomic n (ZMod p) ^ (p - 1))

Proof state:
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) =
    (expand (ZMod p) p) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))

Tactic:
rw [← map_expand, cyclotomic_expand_eq_cyclotomic_mul hp.out hn, Polynomial.map_mul,
  map_cyclotomic, map_cyclotomic]

Result:
no goals

Proof state:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)

Tactic:
letI : Algebra (ZMod p) R := ZMod.algebra _ _

Result:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)

Proof state:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)

Tactic:
suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1) by
  rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
    this, Polynomial.map_pow]

Result:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1)