-- 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.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
⊢ (aeval (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))
      ((expand ℚ p) (minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))) =
    0

Tactic:
rw [aeval_def, ← eval_map, map_expand, expand_eval, ← IsRoot.def, ←
  cyclotomic_eq_minpoly_rat hprim hnpos, map_cyclotomic, @isRoot_cyclotomic_iff]

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
⊢ IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n) ^ p) 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
h : n * p = n
⊢ n * p = n * 1

Tactic:
simp [h]

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
⊢ False

Tactic:
replace h : n * p = n * 1 := by simp [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 * 1
⊢ False

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
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ (aeval (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)))) ((expand ℚ p) (cyclotomic n ℚ)) = 0

Tactic:
rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def,
  @isRoot_cyclotomic_iff]

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)
⊢ IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)) ^ p) n

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
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ cyclotomic (n * p) ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

Tactic:
rw [cyclotomic_eq_minpoly_rat hprim hpos]

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)
⊢ minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) ∣ (expand ℚ p) (cyclotomic n ℚ)

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
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)) ^ p) n

Tactic:
convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n)

Result:
case h.e'_4
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)
⊢ n = n * p / p

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 ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ

Tactic:
refine eq_of_monic_of_dvd_of_natDegree_le ((cyclotomic.monic _ ℤ).mul (cyclotomic.monic _ ℤ))
  ((cyclotomic.monic n ℤ).expand hp.pos) ?_ ?_

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 ℤ)

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

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
⊢ minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) ∣
    (expand ℚ p) (minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))

Tactic:
refine minpoly.dvd ℚ _ ?_

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
⊢ (aeval (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))
      ((expand ℚ p) (minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))) =
    0

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

Tactic:
haveI := NeZero.of_pos hnpos

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 R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R

Proof state:
case h.e'_4
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)
⊢ n = n * p / p

Tactic:
rw [Nat.mul_div_cancel _ (Nat.Prime.pos hp)]

Result:
no goals

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

Tactic:
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)

Result:
case inl
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝ : CommRing R
hdiv : ¬p ∣ 0
⊢ (expand R p) (cyclotomic 0 R) = cyclotomic (0 * p) R * cyclotomic 0 R

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

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
⊢ cyclotomic (n * p) ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

Tactic:
have hpos : 0 < n * p := mul_pos hnpos hp.pos

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
⊢ cyclotomic (n * p) ℚ ∣ (expand ℚ p) (cyclotomic n ℚ)

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
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) ∣ (expand ℚ p) (cyclotomic n ℚ)

Tactic:
refine minpoly.dvd ℚ _ ?_

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)
⊢ (aeval (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)))) ((expand ℚ p) (cyclotomic n ℚ)) = 0

Proof state:
case inl
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝ : CommRing R
hdiv : ¬p ∣ 0
⊢ (expand R p) (cyclotomic 0 R) = cyclotomic (0 * p) R * cyclotomic 0 R

Tactic:
simp

Result:
no goals