awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u_2
inst : Field K
inst_1 : NeZero.{u_2} (R := K) (↑n : K)
⊢ Squarefree (R := K[X]) (cyclotomic n K)

Tactic:
(separable_cyclotomic n K).squarefree

Premises used: Polynomial.Separable.squarefree, Polynomial.separable_cyclotomic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hn : Fact (Nat.Prime p)
⊢ eval 1 (cyclotomic p R) = (↑p : R)

Tactic:
simp only [cyclotomic_prime, eval_X, one_pow, Finset.sum_const, eval_pow, eval_finsetSum,
    Finset.card_range, smul_one_eq_cast]

Premises used: one_pow, Polynomial.eval_X, Polynomial.eval_pow, Finset.card_range, Polynomial.eval_finsetSum, Nat.smul_one_eq_cast, Polynomial.cyclotomic_prime, Finset.sum_const
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Semiring S
f : R →+* S
p : ℕ
inst_2 : Fact (Nat.Prime p)
⊢ eval₂ f 1 (cyclotomic p R) = (↑p : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ eval 1 (cyclotomic (p ^ (k + 1)) R) = (↑p : R)

Tactic:
simp only [cyclotomic_prime_pow_eq_geom_sum hn.out, eval_X, one_pow, Finset.sum_const, eval_pow,
    eval_finsetSum, Finset.card_range, smul_one_eq_cast]

Premises used: one_pow, Polynomial.eval_X, Polynomial.eval_pow, Finset.card_range, Polynomial.cyclotomic_prime_pow_eq_geom_sum, Polynomial.eval_finsetSum, Nat.smul_one_eq_cast, Fact.out, Finset.sum_const
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Semiring S
f : R →+* S
p k : ℕ
inst_2 : Fact (Nat.Prime p)
⊢ eval₂ f 1 (cyclotomic (p ^ (k + 1)) R) = (↑p : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
⊢ NeZero n

Tactic:
haveI := NeZero.of_gt hn
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
rw : 0 < eval (↑(-1) : ℤ) (cyclotomic n ℤ)
⊢ 0 < eval (-1) (cyclotomic n R)

Tactic:
rw [← map_cyclotomic_int, ← Int.cast_one, ← Int.cast_neg, eval_intCast_map, Int.coe_castRingHom,
    Int.cast_pos]

Premises used: Int.cast_neg, Int.coe_castRingHom, Polynomial.eval_intCast_map, Polynomial.map_cyclotomic_int, Int.cast_pos, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
this : 0 < eval (↑(-1) : ℝ) (cyclotomic n ℝ)
⊢ LT.lt (α := ℝ) 0 ((fun (x : ℤ) ↦ ((↑x : ℝ) : ℝ)) (eval (↑(-1) : ℤ) (cyclotomic n ℤ)))

Tactic:
rw [← map_cyclotomic_int n ℝ, eval_intCast_map, Int.coe_castRingHom] at this

Premises used: Real, Int.coe_castRingHom, Polynomial.eval_intCast_map, Polynomial.map_cyclotomic_int
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
this : LT.lt (α := ℝ) 0 ((fun (x : ℤ) ↦ ((↑x : ℝ) : ℝ)) (eval (↑(-1) : ℤ) (cyclotomic n ℤ)))
⊢ 0 < eval (↑(-1) : ℤ) (cyclotomic n ℤ)

Tactic:
simpa only [Int.cast_pos] using this

Premises used: Int.cast_pos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
suffices : 0 < eval (↑(-1) : ℝ) (cyclotomic n ℝ)
⊢ 0 < eval (↑(-1) : ℤ) (cyclotomic n ℤ)

Tactic:
suffices 0 < eval (↑(-1 : ℤ)) (cyclotomic n ℝ) by
    rw [← map_cyclotomic_int n ℝ, eval_intCast_map, Int.coe_castRingHom] at this
    simpa only [Int.cast_pos] using this
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
simp : 0 < eval (-1) (cyclotomic n ℝ)
⊢ 0 < eval (↑(-1) : ℝ) (cyclotomic n ℝ)

Tactic:
simp only [Int.cast_one, Int.cast_neg]

Premises used: Int.cast_neg, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
⊢ coeff (cyclotomic n ℝ) 0 = 1

Tactic:
have h0 := cyclotomic_coeff_zero ℝ hn.le
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
h0 : coeff (cyclotomic n ℝ) 0 = 1
⊢ eval 0 (cyclotomic n ℝ) = 1

Tactic:
rw [coeff_zero_eq_eval_zero] at h0

Premises used: Polynomial.coeff_zero_eq_eval_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
by_contra! : ∀ (hx : eval (-1) (cyclotomic n ℝ) ≤ 0), False
⊢ 0 < eval (-1) (cyclotomic n ℝ)

Tactic:
by_contra! hx
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
⊢ Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)

Tactic:
have := intermediate_value_univ (-1) 0 (cyclotomic n ℝ).continuous
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)
⊢ 0 ∈ Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ))

Tactic:
simpa [h0] using hx
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)
obtain : ∀ (y : ℝ) (hy : IsRoot (cyclotomic n ℝ) y), False
⊢ False

Tactic:
obtain ⟨y, hy : IsRoot _ y⟩ := this (show (0 : ℝ) ∈ Set.Icc _ _ by simpa [h0] using hx)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)
y : ℝ
hy : IsRoot (cyclotomic n ℝ) y
⊢ IsPrimitiveRoot y n

Tactic:
rw [@isRoot_cyclotomic_iff] at hy

Premises used: Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)
y : ℝ
hy : IsPrimitiveRoot y n
⊢ 2 < orderOf y

Tactic:
rw [hy.eq_orderOf] at hn

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)
y : ℝ
hy : IsPrimitiveRoot y n
hn₁ : 2 < orderOf y
⊢ IsPrimitiveRoot y n

Tactic:
rw [hy.eq_orderOf] at hn

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)
y : ℝ
hn : 2 < orderOf y
hy : IsPrimitiveRoot y n
⊢ False

Tactic:
hn.not_ge LinearOrderedRing.orderOf_le_two

Premises used: LT.lt.not_ge, LinearOrderedRing.orderOf_le_two
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
this_1 : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun (x : ℝ) ↦ eval x (cyclotomic n ℝ)
y : ℝ
hn : 2 < orderOf y
hy : IsPrimitiveRoot y n
⊢ False

Tactic:
exact hn.not_ge LinearOrderedRing.orderOf_le_two

Premises used: LT.lt.not_ge, LinearOrderedRing.orderOf_le_two
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn : 2 < n
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
h : ∀ (n : ℕ) (ih : ∀ m < n, ∀ (hn : 2 < m), 0 < eval x (cyclotomic m R)) (hn : 2 < n), 0 < eval x (cyclotomic n R)
⊢ 0 < eval x (cyclotomic n R)

Tactic:
induction n using Nat.strong_induction_on with | _ n ih
-- 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
⊢ 0 < n

Tactic:
have hn' : 0 < n := pos_of_gt 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
⊢ 1 < n

Tactic:
have hn'' : 1 < n := one_lt_two.trans 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
⊢ Eq.{u_1 + 1} (α := R[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)

Tactic:
have := prod_cyclotomic_eq_geom_sum hn' R
-- 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 : Eq.{u_1 + 1} (α := R[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)
⊢ eval x (∏ i ∈ n.divisors.erase 1, cyclotomic i R) = eval x (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)

Tactic:
apply_fun eval x at this

Premises used: Polynomial.eval
-- 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 (∏ i ∈ n.divisors.erase 1, cyclotomic i R) = eval x (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)
⊢ eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i

Tactic:
rw [← cons_self_properDivisors hn'.ne', Finset.erase_cons_of_ne _ hn''.ne', Finset.prod_cons,
    eval_mul, eval_geom_sum] at this

Premises used: Polynomial.eval_mul, LT.lt.ne', Nat.cons_self_properDivisors, Finset.prod_cons, Finset.erase_cons_of_ne, Polynomial.eval_geom_sum
-- 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 : ∀ (h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)), 0 < eval x (cyclotomic n R)
h₁ : ∀ (h : Eq.{u_1 + 1} (α := R) 0 (∑ i ∈ range n, x ^ i)), 0 < eval x (cyclotomic n R)
h₂ : ∀ (h : LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0), 0 < eval x (cyclotomic n R)
⊢ 0 < eval x (cyclotomic n R)

Tactic:
rcases lt_trichotomy 0 (∑ i ∈ Finset.range n, x ^ i) with (h | h | h)

Premises used: Finset.range, HPow.hPow, OfNat.ofNat, Finset.sum, lt_trichotomy
-- 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) 0 (∑ i ∈ range n, x ^ i)
h₁ : 0 < eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R)
h₂ : 0 ≤ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R)
h₃ : R
⊢ 0 < eval x (cyclotomic n R)

Tactic:
apply pos_of_mul_pos_left

Premises used: pos_of_mul_pos_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) 0 (∑ i ∈ range n, x ^ i)
h₁ h₂ h₃ h₄ : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
⊢ 0 < eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R)

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) 0 (∑ i ∈ range n, x ^ i)
h₁ : LE.le.{u_1} (α := R) 0 (∏ j ∈ n.properDivisors.erase 1, eval x (cyclotomic j R))
⊢ 0 ≤ eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R)

Tactic:
rw [eval_prod]

Premises used: 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 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
⊢ LE.le.{u_1} (α := R) 0 (∏ j ∈ n.properDivisors.erase 1, eval x (cyclotomic j R))

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

Premises used: 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 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
h₁ : ∀ (i : ℕ) (hi : i ∈ n.properDivisors.erase 1), 0 ≤ eval x (cyclotomic i R)
⊢ LE.le.{u_1} (α := R) 0 (∏ j ∈ n.properDivisors.erase 1, eval x (cyclotomic j R))

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

Premises used: 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 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
i : ℕ
hi : i ∈ n.properDivisors.erase 1
⊢ 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 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
h₁ : ∀ (h : Odd n ∨ 0 < x + 1) (i : ℕ) (hi : i ≠ 1 ∧ i ∣ n ∧ i < n), 0 ≤ eval x (cyclotomic i R)
⊢ 0 ≤ eval x (cyclotomic i R)

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

Premises used: geom_sum_pos_iff, 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 : Odd n ∨ 0 < x + 1
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
h₁ : ∀ (hk : Odd n), 0 ≤ eval x (cyclotomic i R)
h₂ : ∀ (hx : 0 < x + 1), 0 ≤ eval x (cyclotomic i R)
⊢ 0 ≤ eval x (cyclotomic i R)

Tactic:
rcases h with hk | hx
-- 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
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
⊢ 0 ≤ eval x (cyclotomic i R)

Tactic:
(ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 ?_)).le

Premises used: Nat.two_lt_of_ne, LT.lt.le, 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
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
h : i ≠ 0
h₁ : i ≠ 2
⊢ 0 ≤ eval x (cyclotomic i R)

Tactic:
refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 ?_)).le

Premises used: Nat.two_lt_of_ne, LT.lt.le, 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
hk : Odd n
hi : Ne (α := ℕ) 0 1 ∧ 0 ∣ n ∧ 0 < n
⊢ False

Tactic:
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
hk : Odd n
hi : Ne (α := ℕ) 0 1 ∧ 0 ∣ n ∧ 0 < n
⊢ 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
hk : Odd n
hi : Ne (α := ℕ) 2 1 ∧ 2 ∣ n ∧ 2 < n
⊢ False

Tactic:
not_odd_iff_even.2 (even_iff_two_dvd.mpr hi.2.1) hk

Premises used: Iff.mpr, Nat.not_odd_iff_even, And.right, And.left, even_iff_two_dvd
-- 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
hk : Odd n
hi : Ne (α := ℕ) 2 1 ∧ 2 ∣ n ∧ 2 < n
⊢ False

Tactic:
exact not_odd_iff_even.2 (even_iff_two_dvd.mpr hi.2.1) hk

Premises used: Iff.mpr, Nat.not_odd_iff_even, And.right, And.left, even_iff_two_dvd
-- 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
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
h : ∀ (hi : Ne (α := ℕ) 2 1 ∧ 2 ∣ n ∧ 2 < n), 0 ≤ eval x (cyclotomic 2 R)
h₁ : ∀ (hk : i ≠ 2), 0 ≤ eval x (cyclotomic i R)
⊢ 0 ≤ eval x (cyclotomic i R)

Tactic:
rcases eq_or_ne i 2 with (rfl | hk)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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 (α := ℕ) 2 1 ∧ 2 ∣ n ∧ 2 < n
⊢ 0 ≤ eval x (cyclotomic 2 R)

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

Premises used: Polynomial.eval_X, Polynomial.cyclotomic_two, LT.lt.le, 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
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
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
hk : i ≠ 2
⊢ 0 ≤ eval x (cyclotomic i R)

Tactic:
(ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 hk)).le

Premises used: Nat.two_lt_of_ne, LT.lt.le, 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
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
hk : i ≠ 2
h : i ≠ 0
⊢ 0 ≤ eval x (cyclotomic i R)

Tactic:
refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 hk)).le

Premises used: Nat.two_lt_of_ne, LT.lt.le, 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
hx : 0 < x + 1
hi : Ne (α := ℕ) 0 1 ∧ 0 ∣ n ∧ 0 < n
hk : Ne (α := ℕ) 0 2
⊢ False

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

Premises used: zero_dvd_iff, LT.lt.ne', And.right, And.left, Iff.mp