-- Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean
theorem cyclotomic_comp_X_add_one_isEisensteinAt [hp : Fact p.Prime] :
    ((cyclotomic p ℤ).comp (X + 1)).IsEisensteinAt 𝓟

Proof state:
case refine_3.intro
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
k : ℕ
hk : p = 1 * p * p * k
⊢ False

Tactic:
rw [mul_assoc, mul_comm 1, mul_one] at hk

Result:
case refine_3.intro
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
k : ℕ
hk : p = p * (p * k)
⊢ False

Proof state:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬↑p ^ 2 ∣ ↑p

Tactic:
intro h

Result:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
⊢ False

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
⊢ ∑ x ∈ range p, (lcoeff ℤ i) (↑(p.choose (x + 1)) * X ^ x) ∈ Submodule.span ℤ {↑p}

Tactic:
conv =>
  congr
  congr
  next => skip
  congr
  next => skip
  ext
  rw [lcoeff_apply, ← C_eq_natCast, C_mul_X_pow_eq_monomial, coeff_monomial]

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
⊢ (∑ x ∈ range p, if x = i then ↑(p.choose (x + 1)) else 0) ∈ Submodule.span ℤ {↑p}

Proof state:
case refine_3.intro
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
k : ℕ
hk : 1 = p * k
⊢ False

Tactic:
exact Nat.Prime.not_dvd_one hp.out (Dvd.intro k hk.symm)

Result:
no goals

Proof state:
case refine_3.intro
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
k : ℕ
hk : p * 1 = p * (p * k)
⊢ False

Tactic:
rw [mul_right_inj' hp.out.ne_zero] at hk

Result:
case refine_3.intro
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
k : ℕ
hk : 1 = p * k
⊢ False

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ((cyclotomic p ℤ).comp (X + 1)).IsEisensteinAt (Submodule.span ℤ {↑p})

Tactic:
refine Monic.isEisensteinAt_of_mem_of_not_mem ?_
    (Ideal.IsPrime.ne_top <| (Ideal.span_singleton_prime (mod_cast hp.out.ne_zero)).2 <|
      Nat.prime_iff_prime_int.1 hp.out) (fun {i hi} => ?_) ?_

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ((cyclotomic p ℤ).comp (X + 1)).Monic

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic p ℤ).comp (X + 1)).coeff i ∈ Submodule.span ℤ {↑p}

case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ((cyclotomic p ℤ).comp (X + 1)).coeff 0 ∉ Submodule.span ℤ {↑p} ^ 2

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ((cyclotomic p ℤ).comp (X + 1)).Monic

Tactic:
rw [show (X + 1 : ℤ[X]) = X + C 1 by simp]

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ((cyclotomic p ℤ).comp (X + C 1)).Monic

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (cyclotomic p ℤ).natDegree * (X + 1).natDegree
⊢ X + 1 = X + C 1

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < p - 1
⊢ p ∣ p.choose (i + 1)

Tactic:
exact hp.out.dvd_choose_self i.succ_ne_zero (lt_tsub_iff_right.1 hi)

Result:
no goals

Proof state:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
⊢ False

Tactic:
obtain ⟨k, hk⟩ := Int.natCast_dvd_natCast.1 h

Result:
case refine_3.intro
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
k : ℕ
hk : p = 1 * p * p * k
⊢ False

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
h : (X + C 1).natDegree = 0
⊢ False

Tactic:
rw [natDegree_X_add_C] at h

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 = 0
⊢ False

Proof state:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ((cyclotomic p ℤ).comp (X + 1)).coeff 0 ∉ Submodule.span ℤ {↑p} ^ 2

Tactic:
rw [coeff_zero_eq_eval_zero, eval_comp, cyclotomic_prime, eval_add, eval_X, eval_one, zero_add,
  eval_geom_sum, one_geom_sum, Ideal.submodule_span_eq, Ideal.span_singleton_pow,
  Ideal.mem_span_singleton]

Result:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬↑p ^ 2 ∣ ↑p

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ X + 1 = X + C 1

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < p - 1
⊢ (∑ x ∈ range p, if x = i then ↑(p.choose (x + 1)) else 0) ∈ Submodule.span ℤ {↑p}

Tactic:
simp only [hi.trans_le (Nat.sub_le _ _), sum_ite_eq', mem_range, if_true,
  Ideal.submodule_span_eq, Ideal.mem_span_singleton, Int.natCast_dvd_natCast]

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < p - 1
⊢ p ∣ p.choose (i + 1)

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
⊢ ((cyclotomic p ℤ).comp (X + 1)).coeff i ∈ Submodule.span ℤ {↑p}

Tactic:
rw [cyclotomic_prime, geom_sum_X_comp_X_add_one_eq_sum, ← lcoeff_apply, map_sum]

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
⊢ ∑ x ∈ range p, (lcoeff ℤ i) (↑(p.choose (x + 1)) * X ^ x) ∈ Submodule.span ℤ {↑p}

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 = 0
⊢ False

Tactic:
exact zero_ne_one h.symm

Result:
no goals

Proof state:
case refine_3.intro
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
k : ℕ
hk : p = p * (p * k)
⊢ False

Tactic:
nth_rw 1 [← Nat.mul_one p] at hk

Result:
case refine_3.intro
p : ℕ
hp : Fact (Nat.Prime p)
h : ↑p ^ 2 ∣ ↑p
k : ℕ
hk : p * 1 = p * (p * k)
⊢ False

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ((cyclotomic p ℤ).comp (X + C 1)).Monic

Tactic:
refine (cyclotomic.monic p ℤ).comp (monic_X_add_C 1) fun h => ?_

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
h : (X + C 1).natDegree = 0
⊢ False

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < ((cyclotomic p ℤ).comp (X + 1)).natDegree
⊢ (∑ x ∈ range p, if x = i then ↑(p.choose (x + 1)) else 0) ∈ Submodule.span ℤ {↑p}

Tactic:
rw [natDegree_comp, show (X + 1 : ℤ[X]) = X + C 1 by simp, natDegree_X_add_C, mul_one,
  natDegree_cyclotomic, Nat.totient_prime hp.out] at hi

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < p - 1
⊢ (∑ x ∈ range p, if x = i then ↑(p.choose (x + 1)) else 0) ∈ Submodule.span ℤ {↑p}