awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
inst : Ring R
rw : (expand ℤ 3 : (a : ℤ[X]) → ℤ[X]) (cyclotomic 2 ℤ) = (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) * cyclotomic 2 ℤ
⊢ cyclotomic 6 ℤ * 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)]

Premises used: Polynomial.cyclotomic_expand_eq_cyclotomic_mul, Nat.prime_three
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
inst : Ring R
simp : HPow.hPow (α := ℤ[X]) (β := ℕ) X 3 + 1 = (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) * HAdd.hAdd (α := ℤ[X]) X 1
⊢ (expand ℤ 3 : (a : ℤ[X]) → ℤ[X]) (cyclotomic 2 ℤ) = (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 - X + 1) * cyclotomic 2 ℤ

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

Tactic:
ring
-- 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),
    Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic 0 R) : R[X]) (cyclotomic (0 * p) R : R[X])
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])
⊢ 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)

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
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic 0 R) : R[X]) (cyclotomic (0 * p) R : R[X])

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
hzero : n > 0
⊢ NeZero n

Tactic:
haveI := NeZero.of_pos hzero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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)
rw₃ rw₄ : Eq (α := R[X]) (cyclotomic (n * p) R) (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])

Tactic:
rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int]

Premises used: 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
hzero : n > 0
this : NeZero n
inr : 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])

Tactic:
suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ by
    rw [← map_cyclotomic_int, ← map_expand, this, 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
hzero : n > 0
this : NeZero n
⊢ Eq (α := ℤ[X]) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) : ℤ[X]) (cyclotomic (n * p) ℤ : ℤ[X])

Tactic:
eq_of_monic_of_dvd_of_natDegree_le (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
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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 ℤ))
inr₁ : natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ)
⊢ Eq (α := ℤ[X]) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) : ℤ[X]) (cyclotomic (n * p) ℤ : ℤ[X])

Tactic:
refine eq_of_monic_of_dvd_of_natDegree_le (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
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst : CommRing R
hzero : n > 0
this : NeZero n
⊢ 0 < n * p

Tactic:
have hpos := Nat.mul_pos hzero 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
hzero : 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.symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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)
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 hprim hpos]

Premises used: Polynomial.cyclotomic_eq_minpoly
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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 ℤ))

Tactic:
minpoly.isIntegrallyClosed_dvd (hprim.isIntegral hpos) ?_

Premises used: IsPrimitiveRoot.isIntegral, minpoly.isIntegrallyClosed_dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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)
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.isIntegrallyClosed_dvd (hprim.isIntegral hpos) ?_

Premises used: IsPrimitiveRoot.isIntegral, minpoly.isIntegrallyClosed_dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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)
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
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 * 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
hzero : 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
hzero : 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 _ hp.pos]

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
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
inr₅ inr₆ : p * n.totient ≤ p * n.totient
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤ 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]

Premises used: Polynomial.natDegree_cyclotomic, Nat.totient_mul_of_prime_of_dvd, mul_comm, Polynomial.natDegree_expand
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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)
inr : ∀ (hm : m > 0), Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
⊢ Irreducible (M := R[X]) (cyclotomic (p ^ m) R)

Tactic:
rcases m.eq_zero_or_pos with (rfl | hm)

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
inst_1 : IsDomain R
n : ℕ
h : Irreducible (M := R[X]) (cyclotomic (p ^ n) R)
hmn : 0 ≤ n
⊢ Irreducible (M := R[X]) (cyclotomic (HPow.hPow (β := ℕ) p 0) R)

Tactic:
simpa using irreducible_X_sub_C (1 : R)

Premises used: OfNat.ofNat, Polynomial.irreducible_X_sub_C
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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
inr :
  ∀ (k : ℕ) (hmn : m ≤ m + k) (h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + k)) R)),
    Irreducible (M := R[X]) (cyclotomic (p ^ m) R)
⊢ Irreducible (M := R[X]) (cyclotomic (p ^ m) R)

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
m : ℕ
hm : m > 0
hmn : m ≤ m + 0
h : Irreducible (M := R[X]) (cyclotomic (p ^ (m + 0)) R)
⊢ Irreducible (M := R[X]) (cyclotomic (p ^ m) R)

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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)
⊢ m + k ≠ 0

Tactic:
have : m + k ≠ 0 := (add_pos_of_pos_of_nonneg hm k.zero_le).ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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]) ((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

Premises used: pow_succ, dvd_pow_self, Nat.add_succ, Polynomial.cyclotomic_expand_eq_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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
h₁ : Irreducible (M := R[X]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic (p ^ (m + k)) R) : R[X])
⊢ m + k ≠ 0

Tactic:
rw [Nat.add_succ, pow_succ, ← cyclotomic_expand_eq_cyclotomic hp <| dvd_pow_self p this] at h

Premises used: pow_succ, dvd_pow_self, Nat.add_succ, Polynomial.cyclotomic_expand_eq_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic (p ^ (m + k)) R) : R[X])
this : m + k ≠ 0
⊢ m ≤ m + k

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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]) ((expand R p : (a : R[X]) → R[X]) (cyclotomic (p ^ (m + k)) R) : R[X])
this : m + k ≠ 0
⊢ Irreducible (M := R[X]) (cyclotomic (p ^ m) R)

Tactic:
exact hk (by lia) (of_irreducible_expand hp.ne_zero h)

Premises used: Nat.Prime.ne_zero, Polynomial.of_irreducible_expand
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
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)
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)
⊢ 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)

Premises used: pow_succ, Nat.add_succ, Polynomial.cyclotomic_expand_eq_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
hn : n ≠ 0
h : Irreducible (M := R[X]) (cyclotomic (p ^ n) R)
⊢ Irreducible (M := R[X]) (cyclotomic p R)

Tactic:
pow_one p ▸ cyclotomic_irreducible_pow_of_irreducible_pow hp hn.bot_lt h

Premises used: Eq.rec, pow_one, Polynomial.cyclotomic_irreducible_pow_of_irreducible_pow, Ne.bot_lt
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this_1 : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)
rw :
  map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
    HPow.hPow (α := R[X]) (cyclotomic n R) (p - 1)
rw₁ :
  map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) (p - 1)
rw₂ :
  map (algebraMap (ZMod p) R) (HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)) =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) (p - 1)
rw₃ rw₄ :
  HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) (p - 1) =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) (p - 1)
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) (p - 1)

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

Premises used: Algebra.algebraMap, Polynomial.map_pow, ZMod, Polynomial.map_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
suffices : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (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]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
a :
  Eq (α := (ZMod p)[X]) ((fun (x : (ZMod p)[X]) ↦ cyclotomic n (ZMod p) * x) (cyclotomic (n * p) (ZMod p)))
    ((fun (x : (ZMod p)[X]) ↦ cyclotomic n (ZMod p) * x) (HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)))
⊢ cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (p - 1)

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

Premises used: Polynomial.cyclotomic_ne_zero, mul_right_injective₀, ZMod
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
a :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p))
⊢ HMul.hMul (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (cyclotomic (n * p) (ZMod p)) =
    cyclotomic n (ZMod p) * HPow.hPow (α := (ZMod p)[X]) (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]

Premises used: Nat.Prime.one_lt, tsub_add_cancel_of_le, LT.lt.le, mul_comm, ZMod.expand_card, pow_succ', Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
rw :
  ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ)) :
    (ZMod p)[X])
| ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p)) : (ZMod p)[X])

Tactic:
rw [← map_cyclotomic_int]

Premises used: Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
a :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
⊢ HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p))

Tactic:
conv_rhs => rw [← map_cyclotomic_int]

Premises used: Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
a :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
a₁ :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ * cyclotomic n ℤ)
a₂ :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    HMul.hMul (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ))
      (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
a₃ :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
a₄ a₅ :
  HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p))
⊢ HMul.hMul (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic n (ZMod p)) =
    (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (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]

Premises used: Polynomial.map_mul, Polynomial.cyclotomic_expand_eq_cyclotomic_mul, Polynomial.map_expand, Polynomial.map_cyclotomic, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this_1 : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
rw : map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) = HPow.hPow (α := R[X]) (cyclotomic n R) p
rw₁ :
  map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic (n * p) (ZMod p)) =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) p
rw₂ :
  map (algebraMap (ZMod p) R) (HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p) =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) p
rw₃ rw₄ :
  HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) p =
    HPow.hPow (α := R[X]) (map (R := ZMod p) (algebraMap (ZMod p) R) (cyclotomic n (ZMod p))) p
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) p

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

Premises used: Algebra.algebraMap, Polynomial.map_pow, ZMod, Polynomial.map_cyclotomic