awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr₉ : n.totient * p ≤ n.totient * (p - 1).succ
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr₁₀ : n.totient * p ≤ n.totient * p.pred.succ
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr₁₁ : n.totient * p ≤ n.totient * p
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
inst : Ring R
this : cyclotomic 6 ℤ = HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1
⊢ cyclotomic 6 R = HPow.hPow (α := R[X]) (β := ℕ) X 2 - X + 1
have rw : map (Int.castRingHom R) (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) = HPow.hPow (α := R[X]) (β := ℕ) X 2 - X + 1
Tactic: rw [← map_cyclotomic_int, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
inst : Ring R
⊢ cyclotomic 6 R = HPow.hPow (α := R[X]) (β := ℕ) X 2 - X + 1
have suffices : cyclotomic 6 ℤ = HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1
Tactic: suffices cyclotomic 6 ℤ = X ^ 2 - X + 1 by
    rw [← map_cyclotomic_int, this]
    simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
inst : Ring R
⊢ cyclotomic 6 ℤ = HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1
have apply : cyclotomic 6 ℤ * cyclotomic 2 ℤ = (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) * cyclotomic 2 ℤ
Tactic: apply mul_right_cancel₀ (cyclotomic_ne_zero 2 ℤ)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
inst : Ring R
⊢ cyclotomic 6 ℤ * cyclotomic 2 ℤ = (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) * cyclotomic 2 ℤ
have rw : (expand ℤ 3 : (a : ℤ[X]) → ℤ[X]) (cyclotomic 2 ℤ) = (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) * cyclotomic 2 ℤ
Tactic: rw [show 6 = 2 * 3 by rfl, ← cyclotomic_expand_eq_cyclotomic_mul Nat.prime_three (by norm_num1)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
R : Type u_1
inst : Ring R
⊢ (expand ℤ 3 : (a : ℤ[X]) → ℤ[X]) (cyclotomic 2 ℤ) = (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) * cyclotomic 2 ℤ
have simp : HPow.hPow (α := ℤ[X]) (β := ℕ) X 3 + 1 = (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) * HAdd.hAdd (α := ℤ[X]) X 1
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic n R) : R[X]) (cyclotomic (n * p) R : R[X])
have inl : ∀ (hdiv : p ∣ 0),
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic 0 R) : R[X]) (cyclotomic (0 * p) R : R[X])
Tactic: rcases n.eq_zero_or_pos with (rfl | hzero)
Cleared hypotheses: n, hdiv
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
inl :
  ∀ (hdiv : p ∣ 0),
    Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic 0 R) : R[X]) (cyclotomic (0 * p) R : R[X])
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic n R) : R[X]) (cyclotomic (n * p) R : R[X])
have inr : ∀ (hzero : n > 0),
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic n R) : R[X]) (cyclotomic (n * p) R : R[X])
Tactic: rcases n.eq_zero_or_pos with (rfl | hzero)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (hypothesis)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic n R) : R[X]) (cyclotomic (n * p) R : R[X])
have this : NeZero n
Tactic: haveI := NeZero.of_pos hzero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this_1 : NeZero n
this : Eq (α := ℤ[X]) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) : ℤ[X]) (cyclotomic (n * p) ℤ : ℤ[X])
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic n R) : R[X]) (cyclotomic (n * p) R : R[X])
have rw : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) : R[X])
  (cyclotomic (n * p) R : R[X])
Tactic: rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this_1 : NeZero n
this : Eq (α := ℤ[X]) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) : ℤ[X]) (cyclotomic (n * p) ℤ : ℤ[X])
rw :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) : R[X])
    (cyclotomic (n * p) R : R[X])
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic n R) : R[X]) (cyclotomic (n * p) R : R[X])
have rw₁ : Eq (α := R[X]) (map (R := ℤ) (Int.castRingHom R) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)))
  (cyclotomic (n * p) R)
Tactic: rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this_1 : NeZero n
this : Eq (α := ℤ[X]) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) : ℤ[X]) (cyclotomic (n * p) ℤ : ℤ[X])
rw :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) : R[X])
    (cyclotomic (n * p) R : R[X])
rw₁ :
  Eq (α := R[X]) (map (R := ℤ) (Int.castRingHom R) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)))
    (cyclotomic (n * p) R)
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic n R) : R[X]) (cyclotomic (n * p) R : R[X])
have rw₂ : Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic (n * p) ℤ)) (cyclotomic (n * p) R)
Tactic: rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this_1 : NeZero n
this : Eq (α := ℤ[X]) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) : ℤ[X]) (cyclotomic (n * p) ℤ : ℤ[X])
rw :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) : R[X])
    (cyclotomic (n * p) R : R[X])
rw₁ :
  Eq (α := R[X]) (map (R := ℤ) (Int.castRingHom R) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)))
    (cyclotomic (n * p) R)
rw₂ : Eq (α := R[X]) (map (Int.castRingHom R) (cyclotomic (n * p) ℤ)) (cyclotomic (n * p) R)
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic n R) : R[X]) (cyclotomic (n * p) R : R[X])
have rw₃ : Eq (α := R[X]) (cyclotomic (n * p) R) (cyclotomic (n * p) R)
Tactic: rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic n R) : R[X]) (cyclotomic (n * p) R : R[X])
have inr : Eq (α := ℤ[X]) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) : ℤ[X]) (cyclotomic (n * p) ℤ : ℤ[X])
Tactic: suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ by
    rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
⊢ Eq (α := ℤ[X]) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) : ℤ[X]) (cyclotomic (n * p) ℤ : ℤ[X])
have inr : Dvd.dvd (α := ℤ[X]) (cyclotomic (n * p) ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
Tactic: refine eq_of_monic_of_dvd_of_natDegree_le (cyclotomic.monic _ ℤ)
    ((cyclotomic.monic n ℤ).expand hp.pos) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
inr : Dvd.dvd (α := ℤ[X]) (cyclotomic (n * p) ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
⊢ Eq (α := ℤ[X]) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) : ℤ[X]) (cyclotomic (n * p) ℤ : ℤ[X])
have inr₁ : natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ)
Tactic: refine eq_of_monic_of_dvd_of_natDegree_le (cyclotomic.monic _ ℤ)
    ((cyclotomic.monic n ℤ).expand hp.pos) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (hypothesis)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic (n * p) ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
have hpos : 0 < n * p
Tactic: have hpos := Nat.mul_pos hzero hp.pos
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (hypothesis)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
hpos : 0 < n * p
⊢ Dvd.dvd (α := ℤ[X]) (cyclotomic (n * p) ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
have hprim : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ))) (n * p)
Tactic: have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne.symm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : 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]) (cyclotomic (n * p) ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
have inr : Dvd.dvd (α := ℤ[X]) (minpoly ℤ (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ))))
  ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
Tactic: rw [cyclotomic_eq_minpoly hprim hpos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : 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 ℤ))
have inr : Eq (α := ℂ)
  ((aeval (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ))) : (a : ℤ[X]) → ℂ)
      ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) : ℤ[X]) :
    ℂ)
  (0 : ℂ)
Tactic: refine minpoly.isIntegrallyClosed_dvd (hprim.isIntegral hpos) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ))) (n * p)
⊢ Eq (α := ℂ)
    ((aeval (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ))) : (a : ℤ[X]) → ℂ)
        ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) : ℤ[X]) :
      ℂ)
    (0 : ℂ)
have inr : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑(n * p) : ℂ)) ^ p) n
Tactic: rw [← eval_map_algebraMap, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def,
      @isRoot_cyclotomic_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : 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
have h : n = n * p / p
Tactic: convert! IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : 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
have h : n = n
Tactic: rw [Nat.mul_div_cancel _ hp.pos]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ)
have inr : natDegree (cyclotomic n ℤ) * p ≤ natDegree (cyclotomic (n * p) ℤ)
Tactic: rw [natDegree_expand, natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n,
      Nat.totient_mul_of_prime_of_dvd hp hdiv, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
inr : natDegree (cyclotomic n ℤ) * p ≤ natDegree (cyclotomic (n * p) ℤ)
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ)
have inr₁ : n.totient * p ≤ natDegree (cyclotomic (n * p) ℤ)
Tactic: rw [natDegree_expand, natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n,
      Nat.totient_mul_of_prime_of_dvd hp hdiv, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
inr : natDegree (cyclotomic n ℤ) * p ≤ natDegree (cyclotomic (n * p) ℤ)
inr₁ : n.totient * p ≤ natDegree (cyclotomic (n * p) ℤ)
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ)
have inr₂ : n.totient * p ≤ (n * p).totient
Tactic: rw [natDegree_expand, natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n,
      Nat.totient_mul_of_prime_of_dvd hp hdiv, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
inr : natDegree (cyclotomic n ℤ) * p ≤ natDegree (cyclotomic (n * p) ℤ)
inr₁ : n.totient * p ≤ natDegree (cyclotomic (n * p) ℤ)
inr₂ : n.totient * p ≤ (n * p).totient
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ)
have inr₃ : n.totient * p ≤ (p * n).totient
Tactic: rw [natDegree_expand, natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n,
      Nat.totient_mul_of_prime_of_dvd hp hdiv, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
inr : natDegree (cyclotomic n ℤ) * p ≤ natDegree (cyclotomic (n * p) ℤ)
inr₁ : n.totient * p ≤ natDegree (cyclotomic (n * p) ℤ)
inr₂ : n.totient * p ≤ (n * p).totient
inr₃ : n.totient * p ≤ (p * n).totient
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ)
have inr₄ : n.totient * p ≤ p * n.totient
Tactic: rw [natDegree_expand, natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n,
      Nat.totient_mul_of_prime_of_dvd hp hdiv, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
inr : natDegree (cyclotomic n ℤ) * p ≤ natDegree (cyclotomic (n * p) ℤ)
inr₁ : n.totient * p ≤ natDegree (cyclotomic (n * p) ℤ)
inr₂ : n.totient * p ≤ (n * p).totient
inr₃ : n.totient * p ≤ (p * n).totient
inr₄ : n.totient * p ≤ p * n.totient
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ)
have inr₅ : p * n.totient ≤ p * n.totient
Tactic: rw [natDegree_expand, natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n,
      Nat.totient_mul_of_prime_of_dvd hp hdiv, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (M := R[X]) (cyclotomic (p ^ n) R)
⊢ Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
have inl : ∀ (hmn : 0 ≤ n), Irreducible (M := R[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) R)
Tactic: rcases m.eq_zero_or_pos with (rfl | hm)
Cleared hypotheses: m, hmn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (M := R[X]) (cyclotomic (p ^ n) R)
inl : ∀ (hmn : 0 ≤ n), Irreducible (M := R[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) R)
⊢ Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
have inr : ∀ (hm : m > 0), Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
Tactic: rcases m.eq_zero_or_pos with (rfl | hm)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (M := R[X]) (cyclotomic (p ^ n) R)
hm : m > 0
⊢ Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
have inr : ∀ (k : ℕ) (hmn : m ≤ m + k) (h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + k)) R)),
  Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
Cleared hypotheses: n, hmn, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk :
  ∀ (hmn : m ≤ m + k) (h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + k)) R)),
    Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + (k + 1))) R)
⊢ Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
have this : m + k ≠ 0
Tactic: have : m + k ≠ 0 := (add_pos_of_pos_of_nonneg hm k.zero_le).ne'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk :
  ∀ (hmn : m ≤ m + k) (h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + k)) R)),
    Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + (k + 1))) R)
this : m + k ≠ 0
⊢ Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
have h₁ : Irreducible (M := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic (p ^ (m + k)) R) : R[X])
Tactic: rw [Nat.add_succ, pow_succ, ← cyclotomic_expand_eq_cyclotomic hp <| dvd_pow_self p this] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hmn : m ≤ m + k
h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + k)) R)
⊢ Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
have inr : ∀ (hmn : m ≤ m + 0) (h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + 0)) R)),
  Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
Tactic: induction k with
  | zero => simpa using h
  | succ k hk =>
    have : m + k ≠ 0 := (add_pos_of_pos_of_nonneg hm k.zero_le).ne'
    rw [Nat.add_succ, pow_succ, ← cyclotomic_expand_eq_cyclotomic hp <| dvd_pow_self p this] at h
    exact hk (by lia) (of_irreducible_expand hp.ne_zero h)
Cleared hypotheses: k, hmn, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hmn : m ≤ m + k
h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + k)) R)
inr :
  ∀ (hmn : m ≤ m + 0) (h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + 0)) R)),
    Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
⊢ Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
have inr₁ : ∀ (k : ℕ)
  (hk :
    ∀ (hmn : m ≤ m + k) (h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + k)) R)),
      Irreducible (M := R[X]) (cyclotomic (p ^ m) R))
  (hmn : m ≤ m + (k + 1)) (h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + (k + 1))) R)),
  Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
Tactic: induction k with
  | zero => simpa using h
  | succ k hk =>
    have : m + k ≠ 0 := (add_pos_of_pos_of_nonneg hm k.zero_le).ne'
    rw [Nat.add_succ, pow_succ, ← cyclotomic_expand_eq_cyclotomic hp <| dvd_pow_self p this] at h
    exact hk (by lia) (of_irreducible_expand hp.ne_zero h)
Cleared hypotheses: k, hmn, h