awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : ((PowerSeries.constantCoeff : (a : R⟦X⟧) → R) h : R) ∉ I
eq : f = (↑g : R⟦X⟧) * h
this : Nontrivial R
mapf :
  (PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f =
    HMul.hMul (β := (R ⧸ I)⟦X⟧) (↑(HPow.hPow (α := (R ⧸ I)[X]) X g.natDegree) : (R ⧸ I)⟦X⟧)
      ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) h : (R ⧸ I)⟦X⟧)
i : ℕ
hi : i < g.natDegree
⊢ Eq (α := R ⧸ I)
    ((PowerSeries.coeff i : (a : (R ⧸ I)⟦X⟧) → R ⧸ I)
        ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f) :
      R ⧸ I)
    (0 : R ⧸ I)

Tactic:
simp [mapf, PowerSeries.coeff_X_pow_mul', hi]

Premises used: PowerSeries.coeff_X_pow_mul'
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : ((PowerSeries.constantCoeff : (a : R⟦X⟧) → R) h : R) ∉ I
eq : f = (↑g : R⟦X⟧) * h
rw :
  (↑(WithBot.unbotD 0
          (↑((order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)).lift ⋯) :
            WithBot ℕ)) :
      ℕ∞) =
    order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)
⊢ (↑g.natDegree : ℕ∞) = order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)

Tactic:
rw [natDegree, distinguish.degree_eq_coe_lift_order_map f h notMem eq]

Premises used: Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : ((PowerSeries.constantCoeff : (a : R⟦X⟧) → R) h : R) ∉ I
eq : f = (↑g : R⟦X⟧) * h
⊢ (↑(WithBot.unbotD 0
          (↑((order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)).lift ⋯) :
            WithBot ℕ)) :
      ℕ∞) =
    order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)

Tactic:
ENat.coe_lift _ <| order_finite_iff_ne_zero.2 <|
    distinguish.map_ne_zero_of_eq_mul f h notMem eq

Premises used: Iff.mpr, Polynomial.IsDistinguishedAt.map_ne_zero_of_eq_mul, PowerSeries.order_finite_iff_ne_zero, WithTop.untop, ENat.coe_lift, WithBot.recBotCoe, ENat.lift, WithBot.unbotD
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : ((PowerSeries.constantCoeff : (a : R⟦X⟧) → R) h : R) ∉ I
eq : f = (↑g : R⟦X⟧) * h
⊢ (↑(WithBot.unbotD 0
          (↑((order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)).lift ⋯) :
            WithBot ℕ)) :
      ℕ∞) =
    order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)

Tactic:
exact ENat.coe_lift _ <| order_finite_iff_ne_zero.2 <|
    distinguish.map_ne_zero_of_eq_mul f h notMem eq

Premises used: Iff.mpr, Polynomial.IsDistinguishedAt.map_ne_zero_of_eq_mul, PowerSeries.order_finite_iff_ne_zero, ENat.coe_lift
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))

Tactic:
Monic.isEisensteinAt_of_mem_of_notMem ?_
      (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} => ?_) ?_

Premises used: Iff.mpr, Nat.prime_iff_prime_int, Iff.mp, Ideal.span_singleton_prime, Ideal.IsPrime.ne_top, Fact.out, Polynomial.Monic.isEisensteinAt_of_mem_of_notMem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
refine_1 : (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).Monic
refine_2 :
  ∀ {i : ℕ} {hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree},
    Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ)) ((comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i)
refine_3 :
  (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff 0 ∉ HPow.hPow (α := Ideal ℤ) (β := ℕ) (ℤ ∙ (↑p : ℤ)) 2
⊢ (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))

Tactic:
refine Monic.isEisensteinAt_of_mem_of_notMem ?_
      (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} => ?_) ?_

Premises used: Iff.mpr, Nat.prime_iff_prime_int, Iff.mp, Ideal.span_singleton_prime, Ideal.IsPrime.ne_top, Fact.out, Polynomial.Monic.isEisensteinAt_of_mem_of_notMem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ HAdd.hAdd (α := ℤ[X]) X 1 = HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).Monic

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

Premises used: Polynomial.monic_X_add_C, Int, Polynomial.Monic.comp, Polynomial.cyclotomic.monic, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
refine_1 : ∀ (h : (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)).natDegree = 0), False
⊢ (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).Monic

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

Premises used: Polynomial.monic_X_add_C, Int, Polynomial.Monic.comp, Polynomial.cyclotomic.monic, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)).natDegree = 0
⊢ Eq (α := ℕ) 1 0

Tactic:
rw [natDegree_X_add_C] at h

Premises used: Polynomial.natDegree_X_add_C
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : Eq (α := ℕ) 1 0
⊢ False

Tactic:
zero_ne_one h.symm

Premises used: zero_ne_one, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : Eq (α := ℕ) 1 0
⊢ False

Tactic:
exact zero_ne_one h.symm

Premises used: zero_ne_one, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
refine_2 :
  Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    (∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x))
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ)) ((comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i)

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

Premises used: Polynomial.lcoeff_apply, map_sum, Polynomial.geom_sum_X_comp_X_add_one_eq_sum, Polynomial.cyclotomic_prime
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
a : ℤ ∙ (↑p : ℤ)
a₁ : ∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x)
| Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    (∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x))

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
congr : {(↑p : ℤ)}
| ℤ ∙ (↑p : ℤ)

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
| {(↑p : ℤ)}

Tactic:
next => skip
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
congr : range p
a : fun (x : ℕ) ↦ (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x)
| ∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x)

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
| range p

Tactic:
next => skip
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
a : ∀ (x : ℕ), ((lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x) : ℤ)
| fun (x : ℕ) ↦ (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x)

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
x : ℕ
a : if x = i then (↑(p.choose (x + 1)) : ℤ) else 0
| ((lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x) : ℤ)

Tactic:
rw [lcoeff_apply, ← C_eq_natCast, C_mul_X_pow_eq_monomial, coeff_monomial]

Premises used: Polynomial.C_eq_natCast, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.coeff_monomial, Polynomial.lcoeff_apply
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
a : ∀ (x : ℕ), if x = i then (↑(p.choose (x + 1)) : ℤ) else 0
| Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    (∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x))

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

Premises used: Polynomial.C_eq_natCast, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.coeff_monomial, Polynomial.lcoeff_apply
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
refine_2 : Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ)) (∑ x ∈ range p, if x = i then (↑(p.choose (x + 1)) : ℤ) else 0)
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    (∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x))

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

Premises used: Polynomial.C_eq_natCast, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.coeff_monomial, Polynomial.lcoeff_apply
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < natDegree (cyclotomic p ℤ) * (HAdd.hAdd (α := ℤ[X]) X 1).natDegree
⊢ HAdd.hAdd (α := ℤ[X]) X 1 = HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
⊢ i < p - 1

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

Premises used: Polynomial.natDegree_cyclotomic, Polynomial.natDegree_comp, Nat.totient_prime, Polynomial.natDegree_X_add_C, mul_one, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < p - 1
refine_2 : p ∣ p.choose (i + 1)
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ)) (∑ x ∈ range p, if x = i then (↑(p.choose (x + 1)) : ℤ) else 0)

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]

Premises used: Ideal.submodule_span_eq, if_true, Finset.sum_ite_eq', Nat.sub_le, Finset.mem_range, LT.lt.trans_le, Ideal.mem_span_singleton, Int.natCast_dvd_natCast
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < p - 1
⊢ p ∣ p.choose (i + 1)

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

Premises used: lt_tsub_iff_right, Nat.Prime.dvd_choose_self, Nat.succ_ne_zero, Iff.mp, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
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)

Premises used: lt_tsub_iff_right, Nat.Prime.dvd_choose_self, Nat.succ_ne_zero, Iff.mp, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
refine_3 : ¬HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
⊢ (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff 0 ∉ HPow.hPow (α := Ideal ℤ) (β := ℕ) (ℤ ∙ (↑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]

Premises used: Polynomial.coeff_zero_eq_eval_zero, Ideal.submodule_span_eq, Polynomial.eval_X, one_geom_sum, zero_add, Polynomial.eval_comp, Polynomial.eval_add, Polynomial.eval_one, Polynomial.cyclotomic_prime, Ideal.mem_span_singleton, Ideal.span_singleton_pow, Polynomial.eval_geom_sum
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
refine_3 : ∀ (k : ℕ) (hk : p = HPow.hPow (β := ℕ) p 2 * k), False
⊢ False

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

Premises used: Iff.mp, Int.natCast_dvd_natCast
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
k : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * k
⊢ 2 ≤ p

Tactic:
have : 2 ≤ p := Nat.Prime.two_le hp.out
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
k : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * k
this : 2 ≤ p
nlinarith :
  HPow.hPow (β := ℕ) p 2 ≤ p →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 (↑p : ℤ) + (HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 - (↑p : ℤ)) +
        (0 - HSub.hSub (α := ℤ) 0 (↑p : ℤ) * HSub.hSub (α := ℤ) 2 (↑p : ℤ)) =
      0
nlinarith₁ : HPow.hPow (β := ℕ) p 2 ≤ p → GT.gt (α := ℤ) 2 0
⊢ p < HPow.hPow (β := ℕ) p 2

Tactic:
nlinarith
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
k : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * k
this : 2 ≤ p
⊢ p < HPow.hPow (β := ℕ) p 2

Tactic:
have : p < p ^ 2 := by nlinarith
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
k : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * k
this_1 : 2 ≤ p
this : p < HPow.hPow (β := ℕ) p 2
refine_3 : ∀ (hk : p = HPow.hPow (β := ℕ) p 2 * 0), False
refine_3₁ : ∀ (n : ℕ) (hk : p = HPow.hPow (β := ℕ) p 2 * (n + 1)), False
⊢ False

Tactic:
cases k
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
this_1 : 2 ≤ p
this : p < HPow.hPow (β := ℕ) p 2
hk : p = HPow.hPow (β := ℕ) p 2 * 0
⊢ False

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
this_1 : 2 ≤ p
this : p < HPow.hPow (β := ℕ) p 2
n : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * (n + 1)
⊢ False

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))

Tactic:
Monic.isEisensteinAt_of_mem_of_notMem ?_
      (Ideal.IsPrime.ne_top <| (Ideal.span_singleton_prime (mod_cast hp.out.ne_zero)).2 <|
        Nat.prime_iff_prime_int.1 hp.out) ?_ ?_

Premises used: Iff.mpr, Nat.prime_iff_prime_int, Iff.mp, Ideal.span_singleton_prime, Ideal.IsPrime.ne_top, Fact.out, Polynomial.Monic.isEisensteinAt_of_mem_of_notMem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_1 : (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).Monic
refine_2 :
  ∀ {n_1 : ℕ},
    n_1 < (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n_1)
refine_3 :
  (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff 0 ∉
    HPow.hPow (α := Ideal ℤ) (β := ℕ) (ℤ ∙ (↑p : ℤ)) 2
⊢ (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))

Tactic:
refine Monic.isEisensteinAt_of_mem_of_notMem ?_
      (Ideal.IsPrime.ne_top <| (Ideal.span_singleton_prime (mod_cast hp.out.ne_zero)).2 <|
        Nat.prime_iff_prime_int.1 hp.out) ?_ ?_

Premises used: Iff.mpr, Nat.prime_iff_prime_int, Iff.mp, Ideal.span_singleton_prime, Ideal.IsPrime.ne_top, Fact.out, Polynomial.Monic.isEisensteinAt_of_mem_of_notMem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ HAdd.hAdd (α := ℤ[X]) X 1 = HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).Monic

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

Premises used: Polynomial.monic_X_add_C, Int, Polynomial.Monic.comp, Polynomial.cyclotomic.monic, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_1 : ∀ (h : (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)).natDegree = 0), False
⊢ (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).Monic

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

Premises used: Polynomial.monic_X_add_C, Int, Polynomial.Monic.comp, Polynomial.cyclotomic.monic, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)).natDegree = 0
⊢ Eq (α := ℕ) 1 0

Tactic:
rw [natDegree_X_add_C] at h

Premises used: Polynomial.natDegree_X_add_C
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : Eq (α := ℕ) 1 0
⊢ False

Tactic:
zero_ne_one h.symm

Premises used: zero_ne_one, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : Eq (α := ℕ) 1 0
⊢ False

Tactic:
exact zero_ne_one h.symm

Premises used: zero_ne_one, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
refine_2 :
  ∀ (hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree),
    Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ)) ((comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i)
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    ((comp (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i)

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

Premises used: pow_one, Nat.zero_add
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ)) ((comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i)

Tactic:
(cyclotomic_comp_X_add_one_isEisensteinAt p).mem hi

Premises used: Polynomial.IsEisensteinAt.mem, cyclotomic_comp_X_add_one_isEisensteinAt
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ)) ((comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i)

Tactic:
exact (cyclotomic_comp_X_add_one_isEisensteinAt p).mem hi

Premises used: Polynomial.IsEisensteinAt.mem, cyclotomic_comp_X_add_one_isEisensteinAt
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n_1)
i : ℕ
hi : i < (comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
⊢ Eq (α := ZMod p) ((↑((comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i) : ZMod p) : ZMod p)
    ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p)
        ((comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i) :
      ZMod p)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n_1)
i : ℕ
hi : i < (comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
refine_2 :
  (if p ∣ i then (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) else 0) = 0
refine_2₁ : p ∣ p ^ (n + 1)
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    ((comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i)

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]

Premises used: Polynomial.map_one, Polynomial.coeff_map, Ideal.submodule_span_eq, Polynomial.pow_comp, pow_add, Polynomial.cyclotomic_mul_prime_dvd_eq_pow, Polynomial.map_add, Polynomial.map_X, Nat.Prime.pos, ZMod.intCast_zmod_eq_zero_iff_dvd, pow_one, Polynomial.coeff_expand, ZMod.expand_card, Polynomial.map_cyclotomic, Polynomial.map_comp, Ideal.mem_span_singleton, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree →
      Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
        ((comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff n_1)
i : ℕ
hi : i < (comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
refine_2 : p ∣ i → (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) = 0
⊢ (if p ∣ i then (comp (cyclotomic (p ^ (n + 1)) (ZMod p)) (HAdd.hAdd (α := (ZMod p)[X]) X 1)).coeff (i / p) else 0) = 0

Tactic:
simp only [ite_eq_right_iff]

Premises used: ite_eq_right_iff