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_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 ℤ))
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
have 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 ℤ))
Tactic: rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int,
      map_cyclotomic]
-- 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_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 ℤ))
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
have rw₅ : HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (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]
-- 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
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
have inr : (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
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]
-- 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
⊢ (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
have inr : cyclotomic (n * p) ℤ * cyclotomic n ℤ ∣ (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)
Tactic: refine eq_of_monic_of_dvd_of_natDegree_le ((cyclotomic.monic _ ℤ).mul (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
hnpos : n > 0
this : NeZero n
inr : cyclotomic (n * p) ℤ * cyclotomic n ℤ ∣ (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)
⊢ (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
have inr₁ : natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
  (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
Tactic: refine eq_of_monic_of_dvd_of_natDegree_le ((cyclotomic.monic _ ℤ).mul (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
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℤ * cyclotomic n ℤ ∣ (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)
have inr : map (Int.castRingHom ℚ) (cyclotomic (n * p) ℤ * cyclotomic n ℤ) ∣
  map (Int.castRingHom ℚ) ((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 ?_
-- 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
⊢ map (Int.castRingHom ℚ) (cyclotomic (n * p) ℤ * cyclotomic n ℤ) ∣
    map (Int.castRingHom ℚ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ))
have inr : cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ (expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ)
Tactic: rw [Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic_int, map_expand, 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
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ (expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ)
have inr : ∀ (h : n * p = n), False
Tactic: refine IsCoprime.mul_dvd (cyclotomic.isCoprime_rat fun h => ?_) ?_ ?_
-- 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 : ∀ (h : n * p = n), False
⊢ cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ (expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ)
have inr₁ : Dvd.dvd (α := ℚ[X]) (cyclotomic (n * p) ℚ) ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))
Tactic: refine IsCoprime.mul_dvd (cyclotomic.isCoprime_rat fun h => ?_) ?_ ?_
-- 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 : ∀ (h : n * p = n), False
inr₁ : Dvd.dvd (α := ℚ[X]) (cyclotomic (n * p) ℚ) ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))
⊢ cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ (expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ)
have inr₂ : Dvd.dvd (α := ℚ[X]) (cyclotomic n ℚ) ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))
Tactic: refine IsCoprime.mul_dvd (cyclotomic.isCoprime_rat fun h => ?_) ?_ ?_
-- 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
hnpos : n > 0
this : NeZero n
h : n * p = n
⊢ False
have h₁ : n * p = n * 1
Tactic: replace h : n * p = n * 1 := by simp [h]
Cleared hypotheses: h
-- 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
hnpos : 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 : 0 < n * p := mul_pos hnpos 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
hnpos : 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'
-- 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
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_rat 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
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 ℚ))
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.dvd ℚ _ ?_
-- 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
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
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
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
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
have h : n = n
Tactic: rw [Nat.mul_div_cancel _ (Nat.Prime.pos hp)]
-- 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
hnpos : n > 0
this : NeZero n
⊢ Dvd.dvd (α := ℚ[X]) (cyclotomic n ℚ) ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))
have hprim : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) n
Tactic: have hprim := Complex.isPrimitiveRoot_exp _ hnpos.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
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) n
⊢ Dvd.dvd (α := ℚ[X]) (cyclotomic n ℚ) ((expand ℚ p : (a : ℚ[X]) → ℚ[X]) (cyclotomic n ℚ))
have 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 : ℂ)))))
Tactic: rw [cyclotomic_eq_minpoly_rat hprim hnpos]
-- 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
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 : ℂ)))))
have 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 : ℂ)
Tactic: refine minpoly.dvd ℚ _ ?_
-- 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
hprim : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))) 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 : ℂ)
have inr : IsPrimitiveRoot (Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ)) ^ p) n
Tactic: rw [← eval_map_algebraMap, map_expand, expand_eval, ← IsRoot.def, ←
        cyclotomic_eq_minpoly_rat hprim hnpos, map_cyclotomic, @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
hnpos : n > 0
this : NeZero n
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr : natDegree (cyclotomic n ℤ) * p ≤ (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]
-- 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
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr₁ : n.totient * p ≤ (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]
-- 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
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr₂ : n.totient * p ≤ natDegree (cyclotomic (n * p) ℤ) + natDegree (cyclotomic n ℤ)
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 ℤ)
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr₃ : n.totient * p ≤ (n * p).totient + natDegree (cyclotomic n ℤ)
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 ℤ)
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr₄ : n.totient * p ≤ (n * p).totient + n.totient
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
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr₅ : n.totient * p ≤ (p * n).totient + n.totient
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
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr₆ : n.totient * p ≤ p.totient * n.totient + n.totient
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
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr₇ : n.totient * p ≤ (p - 1) * n.totient + n.totient
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
⊢ natDegree (R := ℤ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) ≤
    (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
have inr₈ : n.totient * p ≤ n.totient * (p - 1) + n.totient
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]