-- 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_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : 1 = 0
⊢ False

Tactic:
exact zero_ne_one h.symm

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
rw [coeff_zero_eq_eval_zero, eval_comp, cyclotomic_prime_pow_eq_geom_sum hp.out, eval_add,
  eval_X, eval_one, zero_add, eval_finset_sum]

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

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 : ℕ
hi : i < p ^ (n + 1) * (p - 1)
k : ℕ
hk : i = p * k
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff (i / p) = 0

Tactic:
rw [hk, pow_succ', mul_assoc] at hi

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 (i / p) = 0

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((cyclotomic (p ^ (n + 1)) ℤ).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)
n : ℕ
⊢ ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).Monic

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
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)
n : ℕ
h : 1 = 0
⊢ False

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

Tactic:
simp

Result:
no goals

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_right_inj' hp.out.ne_zero] at hk

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

Proof state:
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) = 0
⊢ ↑(((cyclotomic (p ^ (n + 1)) ℤ).comp (X + C 1)).coeff k) = (Int.castRingHom (ZMod p)) ?m.35639

Tactic:
rfl

Result:
no goals

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
⊢ p ∣ i → ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff (i / p) = 0

Tactic:
rintro ⟨k, hk⟩

Result:
case refine_2.succ.intro
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
k : ℕ
hk : i = p * k
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff (i / p) = 0

Proof state:
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}

Tactic:
intro i hi

Result:
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}

Proof state:
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) = (Int.castRingHom (ZMod p)) ?m.24966

Tactic:
rfl

Result:
no goals

Proof state:
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 ^ (n + 1) = p * p ^ n

Tactic:
rw [pow_succ']

Result:
no goals

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}
⊢ ∀ {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}

Tactic:
intro i hi

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
⊢ ((cyclotomic (p ^ (n + 1 + 1)) ℤ).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 : 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)
n : ℕ
h : ↑p ^ 2 ∣ ↑p
k : ℕ
hk : p * 1 = p * (p * k)
⊢ False

Proof state:
case refine_2.succ.intro
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
k : ℕ
hk : i = p * k
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff (i / p) = 0

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

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 : ℕ
hi : i < p ^ (n + 1) * (p - 1)
k : ℕ
hk : i = p * k
⊢ ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff (i / p) = 0

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

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

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

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 : (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

Tactic:
simpa [map_comp] using hn

Result:
no goals