-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic_coeff_zero (R : Type*) [CommRing R] {n : ℕ} (hn : 1 < n) :
    (cyclotomic n R).coeff 0 = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : 1 < n
⊢ (cyclotomic n R).coeff 0 = 1

Tactic:
induction' n using Nat.strong_induction_on with n hi

Result:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
⊢ (cyclotomic n R).coeff 0 = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
⊢ (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0

Tactic:
rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
  Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
  hprod, mul_neg, mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1
⊢ ∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0 = 1

Tactic:
rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1
⊢ ∏ x ∈ n.properDivisors.erase 1, 1 = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
⊢ n ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : -1 = -(cyclotomic n R).coeff 0
hzero : (X ^ n - 1).coeff 0 = -1
⊢ (cyclotomic n R).coeff 0 = 1

Tactic:
exact neg_inj.mp (Eq.symm heq)

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
j : ℕ
hj : j ∈ n.properDivisors.erase 1
⊢ 1 < j

Tactic:
exact (Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
  (Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
⊢ (cyclotomic n R).coeff 0 = 1

Tactic:
have hzero : (X ^ n - 1 : R[X]).coeff 0 = (-1 : R) := by
  rw [coeff_zero_eq_eval_zero _]
  simp only [zero_pow (by positivity : n ≠ 0), eval_X, eval_one, zero_sub, eval_pow, eval_sub]

Result:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
hzero : (X ^ n - 1).coeff 0 = -1
⊢ (cyclotomic n R).coeff 0 = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
⊢ eval 0 (X ^ n - 1) = -1

Tactic:
simp only [zero_pow (by positivity : n ≠ 0), eval_X, eval_one, zero_sub, eval_pow, eval_sub]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1
hrw : ∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0 = 1
⊢ (X - 1).coeff 0 * ∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0 = -1

Tactic:
simp only [hrw, mul_one, zero_sub, coeff_one_zero, coeff_X_zero, coeff_sub]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
⊢ (X ^ n - 1).coeff 0 = -1

Tactic:
rw [coeff_zero_eq_eval_zero _]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
⊢ eval 0 (X ^ n - 1) = -1

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1
⊢ ∏ x ∈ n.properDivisors.erase 1, 1 = 1

Tactic:
simp only [Finset.prod_const_one]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
hzero : (X ^ n - 1).coeff 0 = -1
⊢ (cyclotomic n R).coeff 0 = 1

Tactic:
rw [hzero] at heq

Result:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : -1 = -(cyclotomic n R).coeff 0
hzero : (X ^ n - 1).coeff 0 = -1
⊢ (cyclotomic n R).coeff 0 = 1

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
⊢ (cyclotomic n R).coeff 0 = 1

Tactic:
have hprod : (∏ i ∈ Nat.properDivisors n, (Polynomial.cyclotomic i R).coeff 0) = -1 := by
  rw [← Finset.insert_erase (Nat.one_mem_properDivisors_iff_one_lt.2
    (lt_of_lt_of_le one_lt_two hn)), Finset.prod_insert (Finset.not_mem_erase 1 _),
    cyclotomic_one R]
  have hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j := by
    intro j hj
    apply Nat.succ_le_of_lt
    exact (Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
      (Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))
  have hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1 := by
    intro j hj
    exact hi j (Nat.mem_properDivisors.1 (Finset.mem_erase.1 hj).2).2 (hleq j hj)
  have hrw : (∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0) = 1 := by
    rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]
    simp only [Finset.prod_const_one]
  simp only [hrw, mul_one, zero_sub, coeff_one_zero, coeff_X_zero, coeff_sub]

Result:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
⊢ (cyclotomic n R).coeff 0 = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
j : ℕ
hj : j ∈ n.properDivisors.erase 1
⊢ 2 ≤ j

Tactic:
apply Nat.succ_le_of_lt

Result:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
j : ℕ
hj : j ∈ n.properDivisors.erase 1
⊢ 1 < j