awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
inr : HSub.hSub (α := ℝ) (↑q : ℝ) 1 ^ φ n < (↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ)
⊢ (q - 1) ^ φ n < (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs

Tactic:
rw [← @Nat.cast_lt ℝ, Nat.cast_pow, Nat.cast_sub hq'.le, Nat.cast_one, Nat.cast_natAbs]

Premises used: Nat.cast_sub, Nat.cast_natAbs, LT.lt.le, Nat.cast_pow, Nat.cast_lt, Nat.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 ^ φ n < (↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ)

Tactic:
(sub_one_pow_totient_lt_cyclotomic_eval hn' (Nat.one_lt_cast.2 hq')).trans_le ?_

Premises used: Iff.mpr, LT.lt.trans_le, Nat.one_lt_cast, Polynomial.sub_one_pow_totient_lt_cyclotomic_eval
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
inr : eval (↑q : ℝ) (cyclotomic n ℝ) ≤ (↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ)
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 ^ φ n < (↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ)

Tactic:
refine (sub_one_pow_totient_lt_cyclotomic_eval hn' (Nat.one_lt_cast.2 hq')).trans_le ?_

Premises used: Iff.mpr, LT.lt.trans_le, Nat.one_lt_cast, Polynomial.sub_one_pow_totient_lt_cyclotomic_eval
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ LE.le (α := ℝ) (eval ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (↑q : ℤ)) (cyclotomic n ℝ) : ℝ)
    (|(algebraMap ℤ ℝ : (a : ℤ) → ℝ) (eval (↑q : ℤ) (cyclotomic n ℤ))| : ℝ)

Tactic:
(cyclotomic.eval_apply (q : ℤ) n (algebraMap ℤ ℝ)).trans_le (le_abs_self _)

Premises used: Real, le_abs_self, Algebra.algebraMap, Eq.trans_le, Int, Nat.cast, Polynomial.cyclotomic.eval_apply
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
h :
  Eq (α := ℝ) ((↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ) : ℝ)
    (|(algebraMap ℤ ℝ : (a : ℤ) → ℝ) (eval (↑q : ℤ) (cyclotomic n ℤ))| : ℝ)
⊢ eval (↑q : ℝ) (cyclotomic n ℝ) ≤ (↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ)

Tactic:
convert! (cyclotomic.eval_apply (q : ℤ) n (algebraMap ℤ ℝ)).trans_le (le_abs_self _)

Premises used: Real, le_abs_self, Algebra.algebraMap, Eq.trans_le, Int, Nat.cast, Polynomial.cyclotomic.eval_apply
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ Eq (α := ℝ) ((↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ) : ℝ)
    (|(algebraMap ℤ ℝ : (a : ℤ) → ℝ) (eval (↑q : ℤ) (cyclotomic n ℤ))| : ℝ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
⊢ q - 1 < (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs

Tactic:
calc
    q - 1 ≤ (q - 1) ^ totient n := Nat.le_self_pow (Nat.totient_pos.2 <| pos_of_gt hn').ne' _
    _ < ((cyclotomic n ℤ).eval ↑q).natAbs := sub_one_pow_totient_lt_natAbs_cyclotomic_eval hn' hq

Premises used: Iff.mpr, Trans.trans, Nat.le_self_pow, Polynomial.sub_one_pow_totient_lt_natAbs_cyclotomic_eval, pos_of_gt, LT.lt.ne', Nat.totient_pos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
inl :
  ∀ (hdiv : ¬p ∣ 0),
    (expand R p : (a : R[X]) → R[X]) (cyclotomic 0 R) = HMul.hMul (α := R[X]) (cyclotomic (0 * p) R) (cyclotomic 0 R)
inr :
  ∀ (hnpos : n > 0),
    (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)

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

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst : CommRing R
hdiv : ¬p ∣ 0
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic 0 R) = HMul.hMul (α := R[X]) (cyclotomic (0 * p) R) (cyclotomic 0 R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
⊢ NeZero n

Tactic:
haveI := NeZero.of_pos hnpos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this_1 : NeZero n
this : (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
rw :
  (expand R p : (a : R[X]) → R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
rw₁ :
  map (R := ℤ) (Int.castRingHom R) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
rw₂ :
  map (Int.castRingHom R) (cyclotomic (n * p) ℤ * cyclotomic n ℤ) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
rw₃ :
  HMul.hMul (α := R[X]) (map (Int.castRingHom R) (cyclotomic (n * p) ℤ)) (map (Int.castRingHom R) (cyclotomic n ℤ)) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
rw₄ :
  HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ)) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
rw₅ rw₆ :
  HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)

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

Premises used: Polynomial.map_mul, Polynomial.map_expand, Polynomial.map_cyclotomic_int, Polynomial.map_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this : NeZero n
inr : (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (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]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this : NeZero n
⊢ (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ

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

Premises used: Nat.Prime.pos, Int, Polynomial.eq_of_monic_of_dvd_of_natDegree_le, Polynomial.cyclotomic.monic, Polynomial.Monic.expand, Polynomial.Monic.mul
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this : NeZero n
inr : cyclotomic (n * p) ℤ * cyclotomic n ℤ ∣ (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)
inr₁ :
  natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
⊢ (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (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) ?_ ?_

Premises used: Nat.Prime.pos, Int, Polynomial.eq_of_monic_of_dvd_of_natDegree_le, Polynomial.cyclotomic.monic, Polynomial.Monic.expand, Polynomial.Monic.mul
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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 : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)

Tactic:
(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 ?_

Premises used: Iff.mpr, HMul.hMul, Polynomial.IsPrimitive.mul, Nat.Prime.pos, Int, Polynomial.cyclotomic.isPrimitive, Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast, Polynomial.cyclotomic.monic, Polynomial.Monic.expand, Polynomial.Monic.isPrimitive
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this : NeZero n
inr :
  map (Int.castRingHom ℚ) (cyclotomic (n * p) ℤ * cyclotomic n ℤ) ∣
    map (Int.castRingHom ℚ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
⊢ cyclotomic (n * p) ℤ * cyclotomic n ℤ ∣ (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (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 ?_

Premises used: Iff.mpr, HMul.hMul, Polynomial.IsPrimitive.mul, Nat.Prime.pos, Int, Polynomial.cyclotomic.isPrimitive, Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast, Polynomial.cyclotomic.monic, Polynomial.Monic.expand, Polynomial.Monic.isPrimitive
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this : NeZero n
inr : cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ (expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ)
⊢ map (Int.castRingHom ℚ) (cyclotomic (n * p) ℤ * cyclotomic n ℤ) ∣
    map (Int.castRingHom ℚ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))

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

Premises used: Polynomial.map_mul, Polynomial.map_expand, Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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 : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ)

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

Premises used: IsCoprime.mul_dvd, Polynomial.cyclotomic.isCoprime_rat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this : NeZero n
inr : ∀ (h : n * p = n), False
inr₁ : Dvd.dvd (α := ℚ[X]) (cyclotomic (n * p) ℚ) ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))
inr₂ : Dvd.dvd (α := ℚ[X]) (cyclotomic n ℚ) ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))
⊢ cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ (expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ)

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

Premises used: IsCoprime.mul_dvd, Polynomial.cyclotomic.isCoprime_rat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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:
replace h : n * p = n * 1 := by simp [h]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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:
Nat.Prime.ne_one hp (mul_left_cancel₀ hnpos.ne' h)

Premises used: mul_left_cancel₀, LT.lt.ne', Nat.Prime.ne_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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)

Premises used: mul_left_cancel₀, LT.lt.ne', Nat.Prime.ne_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this : NeZero n
⊢ 0 < n * p

Tactic:
have hpos : 0 < n * p := mul_pos hnpos hp.pos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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
⊢ IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ))) (n * p)

Tactic:
have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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)
inr :
  Dvd.dvd (α := ℚ[X]) (minpoly ℚ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ))))
    ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))
⊢ Dvd.dvd (α := ℚ[X]) (cyclotomic (n * p) ℚ) ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))

Tactic:
rw [cyclotomic_eq_minpoly_rat hprim hpos]

Premises used: Polynomial.cyclotomic_eq_minpoly_rat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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)
⊢ Dvd.dvd (α := ℚ[X]) (minpoly ℚ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ))))
    ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))

Tactic:
minpoly.dvd ℚ _ ?_

Premises used: Rat, minpoly.dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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)
inr :
  Eq (α := ℂ)
    ((aeval (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ))) : (a : ℚ[X]) → ℂ)
        ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ) : ℚ[X]) :
      ℂ)
    (0 : ℂ)
⊢ Dvd.dvd (α := ℚ[X]) (minpoly ℚ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ))))
    ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))

Tactic:
refine minpoly.dvd ℚ _ ?_

Premises used: Rat, minpoly.dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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)
inr : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ)) ^ p) n
⊢ Eq (α := ℂ)
    ((aeval (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ))) : (a : ℚ[X]) → ℂ)
        ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ) : ℚ[X]) :
      ℂ)
    (0 : ℂ)

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

Premises used: Polynomial.map_expand, Polynomial.IsRoot.def, Polynomial.eval_map_algebraMap, Polynomial.map_cyclotomic, Polynomial.expand_eval, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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 * p / p)

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

Premises used: IsPrimitiveRoot.pow_of_dvd, dvd_mul_left, Nat.Prime.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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)
h : n = n * p / 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)

Premises used: IsPrimitiveRoot.pow_of_dvd, dvd_mul_left, Nat.Prime.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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)
h h₁ : n = n
⊢ n = n * p / p

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

Premises used: Nat.mul_div_cancel, Nat.Prime.pos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this : NeZero n
⊢ IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) n

Tactic:
have hprim := Complex.isPrimitiveRoot_exp _ hnpos.ne.symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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
inr :
  Dvd.dvd (α := ℚ[X]) (minpoly ℚ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))))
    ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (minpoly ℚ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))))
⊢ Dvd.dvd (α := ℚ[X]) (cyclotomic n ℚ) ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))

Tactic:
rw [cyclotomic_eq_minpoly_rat hprim hnpos]

Premises used: Polynomial.cyclotomic_eq_minpoly_rat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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
⊢ Dvd.dvd (α := ℚ[X]) (minpoly ℚ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))))
    ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (minpoly ℚ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))))

Tactic:
minpoly.dvd ℚ _ ?_

Premises used: Rat, minpoly.dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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
inr :
  Eq (α := ℂ)
    ((aeval (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) : (a : ℚ[X]) → ℂ)
        ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (minpoly ℚ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))) :
          ℚ[X]) :
      ℂ)
    (0 : ℂ)
⊢ Dvd.dvd (α := ℚ[X]) (minpoly ℚ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))))
    ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (minpoly ℚ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))))

Tactic:
refine minpoly.dvd ℚ _ ?_

Premises used: Rat, minpoly.dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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
inr : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)) ^ p) n
⊢ Eq (α := ℂ)
    ((aeval (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) : (a : ℚ[X]) → ℂ)
        ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (minpoly ℚ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)))) :
          ℚ[X]) :
      ℂ)
    (0 : ℂ)

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

Premises used: Polynomial.map_expand, Polynomial.IsRoot.def, Polynomial.cyclotomic_eq_minpoly_rat, Polynomial.eval_map_algebraMap, Polynomial.map_cyclotomic, Polynomial.expand_eval, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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:
IsPrimitiveRoot.pow_of_prime hprim hp hdiv

Premises used: IsPrimitiveRoot.pow_of_prime
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
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

Premises used: IsPrimitiveRoot.pow_of_prime
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this : NeZero n
inr : natDegree (cyclotomic n ℤ) * p ≤ (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
inr₁ : n.totient * p ≤ (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
inr₂ : n.totient * p ≤ natDegree (cyclotomic (n * p) ℤ) + natDegree (cyclotomic n ℤ)
inr₃ : n.totient * p ≤ (n * p).totient + natDegree (cyclotomic n ℤ)
inr₄ : n.totient * p ≤ (n * p).totient + n.totient
inr₅ : n.totient * p ≤ (p * n).totient + n.totient
inr₆ : n.totient * p ≤ p.totient * n.totient + n.totient
inr₇ : n.totient * p ≤ (p - 1) * n.totient + n.totient
inr₈ : n.totient * p ≤ n.totient * (p - 1) + n.totient
inr₉ : n.totient * p ≤ n.totient * (p - 1).succ
inr₁₀ : n.totient * p ≤ n.totient * p.pred.succ
inr₁₁ inr₁₂ : n.totient * p ≤ n.totient * p
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (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]

Premises used: Iff.mpr, Nat.mul_succ, Polynomial.cyclotomic_ne_zero, Nat.succ_pred_eq_of_pos, Polynomial.natDegree_mul, Polynomial.natDegree_cyclotomic, HSub.hSub, Nat.totient_prime, Nat.Prime.pos, Int, Nat.totient_mul, mul_comm, Nat.sub_one, Polynomial.natDegree_expand, OfNat.ofNat, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
inst : Ring R
this : cyclotomic 6 ℤ = HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1
rw : map (Int.castRingHom R) (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) = HPow.hPow (α := R[X]) (β := ℕ) X 2 - X + 1
⊢ cyclotomic 6 R = HPow.hPow (α := R[X]) (β := ℕ) X 2 - X + 1

Tactic:
rw [← map_cyclotomic_int, this]

Premises used: Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
inst : Ring R
this : cyclotomic 6 ℤ = HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1
⊢ map (Int.castRingHom R) (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) = HPow.hPow (α := R[X]) (β := ℕ) X 2 - X + 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
inst : Ring R
suffices : cyclotomic 6 ℤ = HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1
⊢ cyclotomic 6 R = HPow.hPow (α := R[X]) (β := ℕ) X 2 - X + 1

Tactic:
suffices cyclotomic 6 ℤ = X ^ 2 - X + 1 by
    rw [← map_cyclotomic_int, this]
    simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
inst : Ring R
apply : cyclotomic 6 ℤ * cyclotomic 2 ℤ = (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) * cyclotomic 2 ℤ
⊢ cyclotomic 6 ℤ = HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1

Tactic:
apply mul_right_cancel₀ (cyclotomic_ne_zero 2 ℤ)

Premises used: Polynomial.cyclotomic_ne_zero, Int, OfNat.ofNat, mul_right_cancel₀
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
inst : Ring R
⊢ 6 = HMul.hMul (α := ℕ) 2 3

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
inst : Ring R
⊢ ¬Dvd.dvd (α := ℕ) 3 2

Tactic:
norm_num1