awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
hx : 0 < x + 1
hi : Ne (α := ℕ) 0 1 ∧ 0 ∣ n ∧ 0 < n
hk : Ne (α := ℕ) 0 2
⊢ False

Tactic:
exact hn'.ne' <| zero_dvd_iff.mp hi.2.1

Premises used: zero_dvd_iff, LT.lt.ne', And.right, And.left, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Eq.{u_1 + 1} (α := R) 0 (∑ i ∈ range n, x ^ i)
⊢ x = -1 ∧ Even n

Tactic:
rw [eq_comm, geom_sum_eq_zero_iff_neg_one hn'.ne'] at h

Premises used: eq_comm, geom_sum_eq_zero_iff_neg_one, LT.lt.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : x = -1 ∧ Even n
⊢ 0 < eval x (cyclotomic n R)

Tactic:
h.1.symm ▸ cyclotomic_neg_one_pos hn

Premises used: Eq.rec, And.left, _private.0.Polynomial.cyclotomic_neg_one_pos, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : x = -1 ∧ Even n
⊢ 0 < eval x (cyclotomic n R)

Tactic:
exact h.1.symm ▸ cyclotomic_neg_one_pos hn
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
h₁ : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) < 0
h₂ : eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) ≤ 0
h₃ : R
⊢ 0 < eval x (cyclotomic n R)

Tactic:
apply pos_of_mul_neg_left

Premises used: pos_of_mul_neg_left
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
h₁ h₂ h₃ h₄ : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) < 0

Tactic:
rwa [this]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ Even n ∧ x + 1 < 0

Tactic:
rw [geom_sum_neg_iff hn'.ne'] at h

Premises used: LT.lt.ne', geom_sum_neg_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
rw : Ne (α := ℕ) 2 1 ∧ 2 ∣ n ∧ 2 < n
⊢ 2 ∈ n.properDivisors.erase 1

Tactic:
rw [Finset.mem_erase, mem_properDivisors]

Premises used: Finset.mem_erase, Nat.mem_properDivisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ Ne (α := ℕ) 2 1

Tactic:
decide
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ Ne (α := ℕ) 2 1 ∧ 2 ∣ n ∧ 2 < n

Tactic:
exact ⟨by decide, even_iff_two_dvd.mp h.1, hn⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
⊢ 2 ∈ n.properDivisors.erase 1

Tactic:
have h2 : 2 ∈ n.properDivisors.erase 1 := by
      rw [Finset.mem_erase, mem_properDivisors]
      exact ⟨by decide, even_iff_two_dvd.mp h.1, hn⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
h₁ : (∏ x_1 ∈ (n.properDivisors.erase 1).erase 2, eval x (cyclotomic x_1 R)) * eval x (cyclotomic 2 R) ≤ 0
⊢ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) ≤ 0

Tactic:
rw [eval_prod, ← Finset.prod_erase_mul _ _ h2]

Premises used: Finset.prod_erase_mul, Polynomial.eval_prod
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
h₁ : LE.le.{u_1} (α := R) 0 (∏ x_1 ∈ (n.properDivisors.erase 1).erase 2, eval x (cyclotomic x_1 R))
h₂ : eval x (cyclotomic 2 R) ≤ 0
⊢ (∏ x_1 ∈ (n.properDivisors.erase 1).erase 2, eval x (cyclotomic x_1 R)) * eval x (cyclotomic 2 R) ≤ 0

Tactic:
apply mul_nonpos_of_nonneg_of_nonpos

Premises used: mul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
⊢ LE.le.{u_1} (α := R) 0 (∏ x_1 ∈ (n.properDivisors.erase 1).erase 2, eval x (cyclotomic x_1 R))

Tactic:
Finset.prod_nonneg fun i hi => le_of_lt ?_

Premises used: le_of_lt, Finset.prod_nonneg
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
h₁ : ∀ (i : ℕ) (hi : i ∈ (n.properDivisors.erase 1).erase 2), 0 < eval x (cyclotomic i R)
⊢ LE.le.{u_1} (α := R) 0 (∏ x_1 ∈ (n.properDivisors.erase 1).erase 2, eval x (cyclotomic x_1 R))

Tactic:
refine Finset.prod_nonneg fun i hi => le_of_lt ?_

Premises used: le_of_lt, Finset.prod_nonneg
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
i : ℕ
hi : i ∈ (n.properDivisors.erase 1).erase 2
⊢ i ≠ 2 ∧ i ≠ 1 ∧ i ∣ n ∧ i < n

Tactic:
simp only [Finset.mem_erase, mem_properDivisors] at hi

Premises used: Finset.mem_erase, Nat.mem_properDivisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
i : ℕ
hi : i ≠ 2 ∧ i ≠ 1 ∧ i ∣ n ∧ i < n
⊢ 0 < eval x (cyclotomic i R)

Tactic:
ih _ hi.2.2.2 (Nat.two_lt_of_ne ?_ hi.2.1 hi.1)

Premises used: Nat.two_lt_of_ne, And.right, And.left
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
i : ℕ
hi : i ≠ 2 ∧ i ≠ 1 ∧ i ∣ n ∧ i < n
h₁ : i ≠ 0
⊢ 0 < eval x (cyclotomic i R)

Tactic:
refine ih _ hi.2.2.2 (Nat.two_lt_of_ne ?_ hi.2.1 hi.1)

Premises used: Nat.two_lt_of_ne, And.right, And.left
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
hi : Ne (α := ℕ) 0 2 ∧ Ne (α := ℕ) 0 1 ∧ 0 ∣ n ∧ 0 < n
⊢ Ne (α := ℕ) 0 2 ∧ Ne (α := ℕ) 0 1 ∧ n = 0 ∧ 0 < n

Tactic:
rw [zero_dvd_iff] at hi

Premises used: zero_dvd_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
hi : Ne (α := ℕ) 0 2 ∧ Ne (α := ℕ) 0 1 ∧ n = 0 ∧ 0 < n
⊢ False

Tactic:
hn'.ne' hi.2.2.1

Premises used: LT.lt.ne', And.right, And.left
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
hi : Ne (α := ℕ) 0 2 ∧ Ne (α := ℕ) 0 1 ∧ n = 0 ∧ 0 < n
⊢ False

Tactic:
exact hn'.ne' hi.2.2.1

Premises used: LT.lt.ne', And.right, And.left
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : Even n ∧ x + 1 < 0
h2 : 2 ∈ n.properDivisors.erase 1
⊢ eval x (cyclotomic 2 R) ≤ 0

Tactic:
simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using h.right.le

Premises used: Polynomial.eval_X, Polynomial.cyclotomic_two, LT.lt.le, And.right, Polynomial.eval_add, Polynomial.eval_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
zero : (1 < x → 0 < eval x (cyclotomic 0 R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic 0 R))
succ :
  (1 < x → 0 < eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1) R)) ∧
    (1 ≤ x → 0 ≤ eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1) R))
succ₁ :
  (1 < x → 0 < eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1 + 1) R)) ∧
    (1 ≤ x → 0 ≤ eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1 + 1) R))
succ₂ :
  ∀ (n : ℕ), (1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R))
⊢ (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R))

Tactic:
rcases n with (_ | _ | _ | n)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic 0 R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic 0 R))

Tactic:
simp only [cyclotomic_zero, eval_one, zero_lt_one, implies_true, zero_le_one, and_self]

Premises used: and_self, Polynomial.cyclotomic_zero, zero_le_one, zero_lt_one, Polynomial.eval_one, implies_true
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1) R)) ∧
    (1 ≤ x → 0 ≤ eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1) R))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
succ : (1 < x → 0 < x + 1) ∧ (1 ≤ x → 0 ≤ x + 1)
⊢ (1 < x → 0 < eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1 + 1) R)) ∧
    (1 ≤ x → 0 ≤ eval x (cyclotomic (HAdd.hAdd (α := ℕ) 0 1 + 1) R))

Tactic:
simp only [zero_add, reduceAdd, cyclotomic_two, eval_add, eval_X, eval_one]

Premises used: Polynomial.eval_X, Polynomial.cyclotomic_two, Nat.reduceAdd, zero_add, Polynomial.eval_add, Polynomial.eval_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
succ : 1 < x → 0 < x + 1
succ₁ : 1 ≤ x → 0 ≤ x + 1
⊢ (1 < x → 0 < x + 1) ∧ (1 ≤ x → 0 ≤ x + 1)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
h : 1 < x
linarith : x + 1 ≤ 0 → HMul.hMul (α := R) 2 (-1) + (1 - x) + (x + 1 - 0) = 0
linarith₁ : x + 1 ≤ 0 → GT.gt.{u_1} (α := R) 2 0
⊢ 0 < x + 1

Tactic:
linarith
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
h : 1 ≤ x
linarith : x + 1 < 0 → HMul.hMul (α := R) 2 (-1) + (1 - x) + (x + 1 - 0) = 0
linarith₁ : x + 1 < 0 → GT.gt.{u_1} (α := R) 2 0
⊢ 0 ≤ x + 1

Tactic:
linarith
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
succ : 1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)
succ₁ : 1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R)
⊢ (1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R))

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
h : 1 ≤ x
succ : 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)
⊢ 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R)

Tactic:
apply le_of_lt

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
succ : 1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)
succ₁ : 1 ≤ x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)
⊢ (1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R))

Tactic:
constructor <;> intro <;> [skip; apply le_of_lt]

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
h : 1 < x
⊢ 2 < n + 1 + 1 + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
h : 1 < x
⊢ 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)

Tactic:
apply cyclotomic_pos (by lia)

Premises used: Polynomial.cyclotomic_pos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
h : 1 ≤ x
⊢ 2 < n + 1 + 1 + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
h : 1 ≤ x
⊢ 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)

Tactic:
apply cyclotomic_pos (by lia)

Premises used: Polynomial.cyclotomic_pos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : 1 < x
⊢ 0 < eval x (cyclotomic n R)

Tactic:
(cyclotomic_pos_and_nonneg n x).1 hx

Premises used: Polynomial.cyclotomic_pos_and_nonneg, And.left
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : 1 ≤ x
⊢ 0 ≤ eval x (cyclotomic n R)

Tactic:
(cyclotomic_pos_and_nonneg n x).2 hx

Premises used: Polynomial.cyclotomic_pos_and_nonneg, And.right
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
inl : ∀ (h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ 0), eval 1 (cyclotomic 0 R) = 1
inr : ∀ (hn' : n > 0), eval 1 (cyclotomic n R) = 1
⊢ eval 1 (cyclotomic n R) = 1

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn')

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ 0
⊢ eval 1 (cyclotomic 0 R) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
⊢ 1 < n

Tactic:
have hn : 1 < n := one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn'.ne', (h Nat.prime_two 0).symm⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
inr : ∀ (h : eval 1 (cyclotomic n ℤ) = 1), eval 1 (cyclotomic n R) = 1
inr₁ : ∀ (h : eval 1 (cyclotomic n ℤ) = -1), eval 1 (cyclotomic n R) = 1
rsuffices : eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1
⊢ eval 1 (cyclotomic n R) = 1

Tactic:
rsuffices h | h : eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1

Premises used: Polynomial.eval, Polynomial.cyclotomic, Int, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h_1 : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = 1
⊢ Eq (α := R) (eval (↑1 : R) (map (Int.castRingHom R) (cyclotomic n ℤ)) : R)
    (((Int.castRingHom R : ℤ →+* R) : (a : ℤ) → R) (eval (↑1 : ℤ) (cyclotomic n ℤ)) : R)

Tactic:
have := eval_intCast_map (Int.castRingHom R) (cyclotomic n ℤ) 1
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h_1 : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = 1
this :
  Eq (α := R) (eval (↑1 : R) (map (Int.castRingHom R) (cyclotomic n ℤ)) : R)
    (((Int.castRingHom R : ℤ →+* R) : (a : ℤ) → R) (eval (↑1 : ℤ) (cyclotomic n ℤ)) : R)
⊢ eval 1 (cyclotomic n R) = 1

Tactic:
simpa only [map_cyclotomic, Int.cast_one, h, eq_intCast] using this

Premises used: eq_intCast, Polynomial.map_cyclotomic, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h_1 : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
inr : False
⊢ eval 1 (cyclotomic n R) = 1

Tactic:
exfalso
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h_1 : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
linarith : -1 + (eval 1 (cyclotomic n ℤ) - -1) + (0 - eval 1 (cyclotomic n ℤ)) = 0
⊢ False

Tactic:
linarith [cyclotomic_nonneg n (le_refl (1 : ℤ))]

Premises used: le_refl, Polynomial.cyclotomic_nonneg, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
rw : ∀ (p : ℕ), Nat.Prime p → ¬p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
⊢ eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1

Tactic:
rw [← Int.natAbs_eq_natAbs_iff, Int.natAbs_one, Nat.eq_one_iff_not_exists_prime_dvd]

Premises used: Int.natAbs_eq_natAbs_iff, Int.natAbs_one, Nat.eq_one_iff_not_exists_prime_dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
⊢ Fact (Nat.Prime p)

Tactic:
haveI := Fact.mk hp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this : Fact (Nat.Prime p)
⊢ Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)

Tactic:
have := prod_cyclotomic_eq_geom_sum hn' ℤ
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this : Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
⊢ Eq (α := ℤ) (eval 1 (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ)) (eval 1 (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i))

Tactic:
apply_fun eval 1 at this

Premises used: Polynomial.eval, OfNat.ofNat