awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n m : ℕ
h : n ≠ m
hnzero : n > 0
inr : ∀ (h : n ≠ 0), IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)
inr₁ : ∀ (hmzero : m > 0), IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

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

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
hnzero : n > 0
h : n ≠ 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)

Tactic:
isCoprime_one_right

Premises used: Polynomial.cyclotomic, dite, isCoprime_one_right
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n : ℕ
hnzero : n > 0
h : n ≠ 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)

Tactic:
exact isCoprime_one_right

Premises used: isCoprime_one_right
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
inr : ¬cyclotomic n ℚ ∣ cyclotomic m ℚ
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Tactic:
rw [Irreducible.coprime_iff_not_dvd <| cyclotomic.irreducible_rat <| hnzero]

Premises used: Polynomial.cyclotomic.irreducible_rat, Irreducible.coprime_iff_not_dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ ¬cyclotomic n ℚ ∣ cyclotomic m ℚ

Tactic:
fun hdiv => h <| cyclotomic_injective <|
    eq_of_monic_of_associated (cyclotomic.monic n ℚ) (cyclotomic.monic m ℚ) <|
      Irreducible.associated_of_dvd (cyclotomic.irreducible_rat hnzero)
        (cyclotomic.irreducible_rat hmzero) hdiv

Premises used: Irreducible.associated_of_dvd, Rat, Polynomial.cyclotomic_injective, Polynomial.cyclotomic.monic, Polynomial.cyclotomic.irreducible_rat, Polynomial.eq_of_monic_of_associated, Not
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ ¬cyclotomic n ℚ ∣ cyclotomic m ℚ

Tactic:
exact fun hdiv => h <| cyclotomic_injective <|
    eq_of_monic_of_associated (cyclotomic.monic n ℚ) (cyclotomic.monic m ℚ) <|
      Irreducible.associated_of_dvd (cyclotomic.irreducible_rat hnzero)
        (cyclotomic.irreducible_rat hmzero) hdiv

Premises used: Irreducible.associated_of_dvd, Rat, Polynomial.cyclotomic_injective, Polynomial.cyclotomic.monic, Polynomial.cyclotomic.irreducible_rat, Polynomial.eq_of_monic_of_associated
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
⊢ Fact (Nat.Prime p)

Tactic:
haveI : Fact p.Prime := ⟨hp⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
i : Fin p
⊢ α i = P.coeff (↑i : ℕ)

Tactic:
simp [P, ← Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
⊢ ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)

Tactic:
have hP (i : Fin p) : α i = P.coeff i := by simp [P, ← Fin.ext_iff]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
x : Fin p
h : Membership.mem (γ := Finset (Fin p)) Finset.univ x
grw : LE.le (α := WithBot ℕ) (↑(↑x : ℕ) : WithBot ℕ) (↑(p - 1) : WithBot ℕ)
⊢ (HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α x) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑x : ℕ))).degree ≤
    (↑(p - 1) : WithBot ℕ)

Tactic:
grw [degree_C_mul_X_pow_le]

Premises used: Polynomial.degree_C_mul_X_pow_le
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
x : Fin p
h : Membership.mem (γ := Finset (Fin p)) Finset.univ x
simp : (↑x : ℕ) ≤ p - 1
⊢ LE.le (α := WithBot ℕ) (↑(↑x : ℕ) : WithBot ℕ) (↑(p - 1) : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
x : Fin p
h : Membership.mem (γ := Finset (Fin p)) Finset.univ x
⊢ (↑x : ℕ) ≤ p - 1

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
⊢ P.degree ≤ (↑(p - 1) : WithBot ℕ)

Tactic:
have hP' : P.degree ≤ ↑(p - 1) :=
    (degree_sum_le ..).trans (Finset.sup_le fun _ _ ↦ by grw [degree_C_mul_X_pow_le]; simp; grind)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
trans :
  Eq.{u_1 + 1} (α := K) (∑ i : Fin p, (↑(α i) : K) * ζ ^ (↑i : ℕ)) 0 ↔
    Eq (α := K) ((aeval ζ : (a : ℚ[X]) → K) P : K) (0 : K)
trans₁ : Eq (α := K) ((aeval ζ : (a : ℚ[X]) → K) P : K) (0 : K) ↔ ∀ (i j : Fin p), α i = α j
⊢ Eq.{u_1 + 1} (α := K) (∑ i : Fin p, (↑(α i) : K) * ζ ^ (↑i : ℕ)) 0 ↔ ∀ (i j : Fin p), α i = α j

Tactic:
trans aeval ζ P = 0

Premises used: Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
⊢ Eq.{u_1 + 1} (α := K) (∑ i : Fin p, (↑(α i) : K) * ζ ^ (↑i : ℕ)) 0 ↔
    Eq (α := K) ((aeval ζ : (a : ℚ[X]) → K) P : K) (0 : K)

Tactic:
simp [P]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
rw : cyclotomic p ℚ ∣ P ↔ ∀ (i j : Fin p), α i = α j
⊢ Eq (α := K) ((aeval ζ : (a : ℚ[X]) → K) P : K) (0 : K) ↔ ∀ (i j : Fin p), α i = α j

Tactic:
rw [← minpoly.dvd_iff, ← cyclotomic_eq_minpoly_rat hζ hp.pos]

Premises used: minpoly.dvd_iff, Nat.Prime.pos, Polynomial.cyclotomic_eq_minpoly_rat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
⊢ cyclotomic p ℚ ∣ P ↔ ∀ (i j : Fin p), α i = α j

Tactic:
⟨fun ⟨c, hc⟩ ↦ ?_, fun H ↦ ⟨C (α 0), Polynomial.ext fun i ↦ if h : i < p then ?_ else ?_⟩⟩

Premises used: Polynomial.C, Polynomial.ext, dite, LT.lt, Iff.intro, Exists.intro, _private.0.IsPrimitiveRoot.sum_eq_zero_iff_forall_eq.match_1, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
refine_1 : cyclotomic p ℚ ∣ P → ∀ (c : ℚ[X]) (hc : P = cyclotomic p ℚ * c) (i j : Fin p), α i = α j
refine_2 :
  ∀ (H : ∀ (i j : Fin p), α i = α j) (i : ℕ) (h : i < p),
    P.coeff i = (HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) (α 0) : ℚ[X])).coeff i
refine_3 :
  ∀ (H : ∀ (i j : Fin p), α i = α j) (i : ℕ) (h : ¬i < p),
    P.coeff i = (HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) (α 0) : ℚ[X])).coeff i
⊢ cyclotomic p ℚ ∣ P ↔ ∀ (i j : Fin p), α i = α j

Tactic:
refine ⟨fun ⟨c, hc⟩ ↦ ?_, fun H ↦ ⟨C (α 0), Polynomial.ext fun i ↦ if h : i < p then ?_ else ?_⟩⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
h : cyclotomic p ℚ ∣ P
c : ℚ[X]
hc : P = cyclotomic p ℚ * c
⊢ (↑(p - 1) : WithBot ℕ) + c.degree ≤ (↑(p - 1) : WithBot ℕ)

Tactic:
rw [hc, degree_mul, degree_cyclotomic, Nat.totient_prime hp] at hP'

Premises used: Nat.totient_prime, Polynomial.degree_cyclotomic, Polynomial.degree_mul
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
h : cyclotomic p ℚ ∣ P
c : ℚ[X]
hc : P = cyclotomic p ℚ * c
hP'₁ : (↑(p - 1) : WithBot ℕ) + c.degree ≤ (↑(p - 1) : WithBot ℕ)
⊢ P = cyclotomic p ℚ * c

Tactic:
rw [hc, degree_mul, degree_cyclotomic, Nat.totient_prime hp] at hP'

Premises used: Nat.totient_prime, Polynomial.degree_cyclotomic, Polynomial.degree_mul
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
h : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : (↑(p - 1) : WithBot ℕ) + c.degree ≤ (↑(p - 1) : WithBot ℕ)
hc : P = cyclotomic p ℚ * c
⊢ Ne (α := WithBot ℕ) (↑(p - 1) : WithBot ℕ) ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
h : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : (↑(p - 1) : WithBot ℕ) + c.degree ≤ (↑(p - 1) : WithBot ℕ)
hc : P = cyclotomic p ℚ * c
⊢ (↑(p - 1) : WithBot ℕ) + c.degree ≤ HAdd.hAdd (α := WithBot ℕ) (↑(p - 1) : WithBot ℕ) 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
h : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : (↑(p - 1) : WithBot ℕ) + c.degree ≤ (↑(p - 1) : WithBot ℕ)
hc : P = cyclotomic p ℚ * c
⊢ c.degree ≤ 0

Tactic:
have : c.degree ≤ 0 := (WithBot.add_le_add_iff_left (x := ↑(p - 1)) (by simp)).mp (by simpa)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this_1 : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
h : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : (↑(p - 1) : WithBot ℕ) + c.degree ≤ (↑(p - 1) : WithBot ℕ)
hc : P = cyclotomic p ℚ * c
this : c.degree ≤ 0
refine_1 :
  ∀ (c : ℚ) (hP' : (↑(p - 1) : WithBot ℕ) + degree (R := ℚ) ((C : (a : ℚ) → ℚ[X]) c) ≤ (↑(p - 1) : WithBot ℕ))
    (hc : P = HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) c : ℚ[X]))
    (this : degree (R := ℚ) ((C : (a : ℚ) → ℚ[X]) c) ≤ 0) (i j : Fin p), α i = α j
⊢ ∀ (i j : Fin p), α i = α j

Tactic:
obtain ⟨c, rfl⟩ := natDegree_eq_zero.mp (natDegree_eq_zero_iff_degree_le_zero.mpr this)

Premises used: Iff.mpr, Iff.mp, Polynomial.natDegree_eq_zero_iff_degree_le_zero, Polynomial.natDegree_eq_zero, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this_1 : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
h : cyclotomic p ℚ ∣ P
c : ℚ
hP' : (↑(p - 1) : WithBot ℕ) + degree (R := ℚ) ((C : (a : ℚ) → ℚ[X]) c) ≤ (↑(p - 1) : WithBot ℕ)
hc : P = HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) c : ℚ[X])
this : degree (R := ℚ) ((C : (a : ℚ) → ℚ[X]) c) ≤ 0
⊢ ∀ (i j : Fin p), α i = α j

Tactic:
simp [hP, hc, cyclotomic_prime]

Premises used: Polynomial.cyclotomic_prime
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
H : ∀ (i j : Fin p), α i = α j
i : ℕ
h : i < p
⊢ i < p

Tactic:
h
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
H : ∀ (i j : Fin p), α i = α j
i : ℕ
h : i < p
refine_2 :
  ∀ (i : Fin p),
    P.coeff (↑i : ℕ) =
      (HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) (α 0) : ℚ[X])).coeff (↑i : ℕ)
⊢ P.coeff i = (HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) (α 0) : ℚ[X])).coeff i

Tactic:
lift i to Fin p using h

Premises used: Fin
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
H : ∀ (i j : Fin p), α i = α j
i : Fin p
⊢ P.coeff (↑i : ℕ) =
    (HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) (α 0) : ℚ[X])).coeff (↑i : ℕ)

Tactic:
simp [cyclotomic_prime, ← hP, H i 0]

Premises used: Polynomial.cyclotomic_prime, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i : Fin p, HMul.hMul (α := ℚ[X]) ((C : (a : ℚ) → ℚ[X]) (α i) : ℚ[X]) (HPow.hPow (α := ℚ[X]) X (↑i : ℕ))
hP : ∀ (i : Fin p), α i = P.coeff (↑i : ℕ)
hP' : P.degree ≤ (↑(p - 1) : WithBot ℕ)
H : ∀ (i j : Fin p), α i = α j
i : ℕ
h : ¬i < p
⊢ P.coeff i = (HMul.hMul (α := ℚ[X]) (β := ℚ[X]) (cyclotomic p ℚ) ((C : (a : ℚ) → ℚ[X]) (α 0) : ℚ[X])).coeff i

Tactic:
simp [cyclotomic_prime, P, h, Fin.forall_iff, @forall_comm _ (_ = _), Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero, forall_comm, Fin.forall_iff, Polynomial.cyclotomic_prime
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℤ
⊢ Eq.{u_1 + 1} (α := K) (∑ i : Fin p, (↑(α i) : K) * ζ ^ (↑i : ℕ)) 0 ↔ ∀ (i j : Fin p), α i = α j

Tactic:
simpa using sum_eq_zero_iff_forall_eq hp hζ (Int.cast ∘ α)

Premises used: Int.cast, Function.comp, IsPrimitiveRoot.sum_eq_zero_iff_forall_eq
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a : R
⊢ dickson k a 0 = HSub.hSub (α := R[X]) 3 (↑k : R[X])

Tactic:
rfl

Premises used: Polynomial.dickson, rfl
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a : R
⊢ Eq (α := R[X]) (dickson k a 1) X

Tactic:
rfl

Premises used: Polynomial.dickson, rfl
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a : R
⊢ dickson k a 2 =
    HPow.hPow (α := R[X]) (β := ℕ) X 2 -
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HSub.hSub (α := R[X]) 3 (↑k : R[X]))

Tactic:
simp only [dickson, sq]

Premises used: sq, Polynomial.dickson
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a : R
n : ℕ
rw rw₁ :
  HMul.hMul (α := R[X]) X (dickson k a (n + 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a n) =
    HMul.hMul (α := R[X]) X (dickson k a (n + 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a n)
⊢ dickson k a (n + 2) =
    HMul.hMul (α := R[X]) X (dickson k a (n + 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a n)

Tactic:
rw [dickson]

Premises used: Polynomial.dickson
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ n
obtain :
  ∀ (n : ℕ) (h : 2 ≤ 2 + n),
    dickson k a (2 + n) =
      HMul.hMul (α := R[X]) X (dickson k a (2 + n - 1)) -
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a (2 + n - 2))
⊢ dickson k a n =
    HMul.hMul (α := R[X]) X (dickson k a (n - 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a (n - 2))

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
rw :
  dickson k a (n + 2) =
    HMul.hMul (α := R[X]) X (dickson k a (n + 2 - 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a (n + 2 - 2))
⊢ dickson k a (2 + n) =
    HMul.hMul (α := R[X]) X (dickson k a (2 + n - 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a (2 + n - 2))

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (n + 2) =
    HMul.hMul (α := R[X]) X (dickson k a (n + 2 - 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a (n + 2 - 2))

Tactic:
dickson_add_two k a n

Premises used: Polynomial.dickson_add_two, Nat.pred
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (n + 2) =
    HMul.hMul (α := R[X]) X (dickson k a (n + 2 - 1)) -
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (dickson k a (n + 2 - 2))

Tactic:
exact dickson_add_two k a n

Premises used: Polynomial.dickson_add_two
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
k : ℕ
a : R
f : R →+* S
simp_rw : map f (HSub.hSub (α := R[X]) 3 (↑k : R[X])) = HSub.hSub (α := S[X]) 3 (↑k : S[X])
simp_rw₁ : map f 3 - map f (↑k : R[X]) = HSub.hSub (α := S[X]) 3 (↑k : S[X])
simp_rw₂ : map f 3 - (↑k : S[X]) = HSub.hSub (α := S[X]) 3 (↑k : S[X])
⊢ map f (dickson k a 0) = dickson k ((f : (a : R) → S) a) 0

Tactic:
simp_rw [dickson_zero, Polynomial.map_sub, Polynomial.map_natCast, Polynomial.map_ofNat]

Premises used: Polynomial.map_ofNat, Polynomial.map_sub, Polynomial.dickson_zero, Polynomial.map_natCast
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
k : ℕ
a : R
f : R →+* S
⊢ map f (dickson k a 1) = dickson k ((f : (a : R) → S) a) 1

Tactic:
simp only [dickson_one, map_X]

Premises used: Polynomial.map_X, Polynomial.dickson_one
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
simp :
  X * map f (dickson k a (n + 1)) -
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X]) (map f (dickson k a n)) =
    HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
        (dickson k ((f : (a : R) → S) a) n : S[X])
⊢ map f (dickson k a (n + 2)) = dickson k ((f : (a : R) → S) a) (n + 2)

Tactic:
simp only [dickson_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, map_C]

Premises used: Polynomial.map_mul, Polynomial.map_X, Polynomial.dickson_add_two, Polynomial.map_sub, Polynomial.map_C
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
rw :
  X * map f (dickson k a (n + 1)) -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
        (dickson k ((f : (a : R) → S) a) n : S[X]) =
    HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
        (dickson k ((f : (a : R) → S) a) n : S[X])
rw₁ rw₂ :
  HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
        (dickson k ((f : (a : R) → S) a) n : S[X]) =
    HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
        (dickson k ((f : (a : R) → S) a) n : S[X])
⊢ X * map f (dickson k a (n + 1)) -
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X]) (map f (dickson k a n)) =
    HMul.hMul (α := S[X]) (β := S[X]) (X : S[X]) (dickson k ((f : (a : R) → S) a) (n + 1) : S[X]) -
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
        (dickson k ((f : (a : R) → S) a) n : S[X])

Tactic:
rw [map_dickson f n, map_dickson f (n + 1)]

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Dickson
Goal:
R : Type u_1
inst : CommRing R
⊢ HSub.hSub (α := R[X]) 3 (↑2 : R[X]) = 1

Tactic:
norm_num