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

Proof state:
case refine_2.succ.intro
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn : ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff k ∈ Submodule.span ℤ {↑p}
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff k = 0

Tactic:
rw [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ← ZMod.intCast_zmod_eq_zero_iff_dvd,
   show ↑(_ : ℤ) = Int.castRingHom (ZMod p) _ by rfl, ← coeff_map] at hn

Result:
case refine_2.succ.intro
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn : (Polynomial.map (Int.castRingHom (ZMod p)) ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1))).coeff k = 0
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff k = 0

Proof state:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range p, eval 1 ((X ^ p ^ n) ^ i) ∉ Submodule.span ℤ {↑p} ^ 2

Tactic:
simp only [eval_pow, eval_X, one_pow, sum_const, card_range, Nat.smul_one_eq_cast,
  submodule_span_eq, Ideal.submodule_span_eq, Ideal.span_singleton_pow,
  Ideal.mem_span_singleton]

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

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((cyclotomic (p ^ (n + 1)) ℤ).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) ?_ ?_

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

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}

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

Proof state:
case refine_3.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
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)
n : ℕ
h : ↑p ^ 2 ∣ ↑p
k : ℕ
hk : p = p * (p * k)
⊢ False

Proof state:
case refine_2.succ.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ}, n_1 < p ^ n * (p - 1) → ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}
i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff (i / p) = 0

Tactic:
rw [hk, mul_comm, Nat.mul_div_cancel _ hp.out.pos]

Result:
case refine_2.succ.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ}, n_1 < p ^ n * (p - 1) → ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}
i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff k = 0

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

Tactic:
intro h

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

Proof state:
case refine_2.succ.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ}, n_1 < p ^ n * (p - 1) → ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}
i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff k = 0

Tactic:
replace hn := hn (lt_of_mul_lt_mul_left' hi)

Result:
case refine_2.succ.intro
p : ℕ
hp : Fact (Nat.Prime p)
n i k : ℕ
hi : p * k < p * (p ^ n * (p - 1))
hk : i = p * k
hn : ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff k ∈ Submodule.span ℤ {↑p}
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff k = 0

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

Tactic:
rw [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ← ZMod.intCast_zmod_eq_zero_iff_dvd,
  show ↑(_ : ℤ) = Int.castRingHom (ZMod p) _ by rfl, ← coeff_map, map_comp, map_cyclotomic,
  Polynomial.map_add, map_X, Polynomial.map_one, pow_add, pow_one,
  cyclotomic_mul_prime_dvd_eq_pow, pow_comp, ← ZMod.expand_card, coeff_expand hp.out.pos]

Result:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ (if p ∣ i then ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff (i / p) else 0) = 0

case refine_2.succ.hn
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ p ∣ p ^ (n + 1)

Proof state:
case refine_2.zero
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:
exact (cyclotomic_comp_X_add_one_isEisensteinAt p).mem hi

Result:
no goals

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

Tactic:
rw [Nat.zero_add, pow_one] at hi ⊢

Result:
case refine_2.zero
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}

Proof state:
case refine_3.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
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
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
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)
n : ℕ
h : ↑p ^ 2 ∣ ↑p
k : ℕ
hk : p = 1 * p * p * k
⊢ False

Proof state:
case refine_2.succ.hn
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ p ∣ p ^ (n + 1)

Tactic:
exact ⟨p ^ n, by rw [pow_succ']⟩

Result:
no goals

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}

Tactic:
induction' n with n hn

Result:
case refine_2.zero
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ {n : ℕ},
    n < ((cyclotomic (p ^ (0 + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (0 + 1)) ℤ).comp (X + 1)).coeff n ∈ Submodule.span ℤ {↑p}

case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}
⊢ ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}