-- Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
theorem cyclotomic_expand_eq_cyclotomic_mul {p n : ℕ} (hp : Nat.Prime p) (hdiv : ¬p ∣ n)
    (R : Type*) [CommRing R] :
    expand R p (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R

Proof state:
case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℤ * cyclotomic n ℤ ∣ (expand ℤ p) (cyclotomic n ℤ)

Tactic:
refine (IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast _ _
  (IsPrimitive.mul (cyclotomic.isPrimitive (n * p) ℤ) (cyclotomic.isPrimitive n ℤ))
  ((cyclotomic.monic n ℤ).expand hp.pos).isPrimitive).2 ?_

Result:
case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ map (Int.castRingHom ℚ) (cyclotomic (n * p) ℤ * cyclotomic n ℤ) ∣
    map (Int.castRingHom ℚ) ((expand ℤ p) (cyclotomic n ℤ))

Proof state:
case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

Tactic:
refine IsCoprime.mul_dvd (cyclotomic.isCoprime_rat fun h => ?_) ?_ ?_

Result:
case inr.refine_1.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
h : n * p = n
⊢ False

case inr.refine_1.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

case inr.refine_1.refine_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic n ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

Proof state:
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ (expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R

Tactic:
suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ by
  rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int,
    map_cyclotomic]

Result:
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ (expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ

Proof state:
case inr.refine_1.refine_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic n ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

Tactic:
have hprim := Complex.isPrimitiveRoot_exp _ hnpos.ne.symm

Result:
case inr.refine_1.refine_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ cyclotomic n ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

Proof state:
case inr.refine_1.refine_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n) ^ p) n

Tactic:
exact IsPrimitiveRoot.pow_of_prime hprim hp hdiv

Result:
no goals

Proof state:
case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ ((expand ℤ p) (cyclotomic n ℤ)).natDegree ≤ (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree

Tactic:
rw [natDegree_expand, natDegree_cyclotomic,
  natDegree_mul (cyclotomic_ne_zero _ ℤ) (cyclotomic_ne_zero _ ℤ), natDegree_cyclotomic,
  natDegree_cyclotomic, mul_comm n,
  Nat.totient_mul ((Nat.Prime.coprime_iff_not_dvd hp).2 hdiv), Nat.totient_prime hp,
  mul_comm (p - 1), ← Nat.mul_succ, Nat.sub_one, Nat.succ_pred_eq_of_pos hp.pos]

Result:
no goals

Proof state:
case inr.refine_1.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
h : n * p = n * 1
⊢ False

Tactic:
exact Nat.Prime.ne_one hp (mul_left_cancel₀ hnpos.ne' h)

Result:
no goals

Proof state:
case inr.refine_1.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
⊢ cyclotomic (n * p) ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

Tactic:
have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne'

Result:
case inr.refine_1.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ cyclotomic (n * p) ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

Proof state:
case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ map (Int.castRingHom ℚ) (cyclotomic (n * p) ℤ * cyclotomic n ℤ) ∣
    map (Int.castRingHom ℚ) ((expand ℤ p) (cyclotomic n ℤ))

Tactic:
rw [Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic_int, map_expand, map_cyclotomic_int]

Result:
case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

Proof state:
case inr.refine_1.refine_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ cyclotomic n ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

Tactic:
rw [cyclotomic_eq_minpoly_rat hprim hnpos]

Result:
case inr.refine_1.refine_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) ∣
    (expand ℚ p) (minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))

Proof state:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this✝ : NeZero n
this : (expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
⊢ (expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R

Tactic:
rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int,
  map_cyclotomic]

Result:
no goals