awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (hypothesis)
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
H :
  Eq (α := (R ⧸ I)⟦X⟧) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f : (R ⧸ I)⟦X⟧)
    (0 : (R ⧸ I)⟦X⟧)
⊢ False
have 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⟧)
Tactic: have mapf : f.map (Ideal.Quotient.mk I) = (Polynomial.X ^ g.natDegree : (R ⧸ I)[X]) *
      h.map (Ideal.Quotient.mk I) := by
    simp [← map_eq_X_pow distinguish, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (hypothesis)
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
H :
  Eq (α := (R ⧸ I)⟦X⟧) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f : (R ⧸ I)⟦X⟧)
    (0 : (R ⧸ I)⟦X⟧)
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⟧)
⊢ False
have H₁ : Eq (α := R ⧸ I)
  ((PowerSeries.coeff g.natDegree : (a : (R ⧸ I)⟦X⟧) → R ⧸ I)
      ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f) :
    R ⧸ I)
  ((PowerSeries.coeff g.natDegree : (a : (R ⧸ I)⟦X⟧) → R ⧸ I) 0 : R ⧸ I)
Tactic: apply_fun PowerSeries.coeff g.natDegree at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (hypothesis)
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
⊢ g.degree =
    (↑((order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)).lift ⋯) :
      WithBot ℕ)
have this : Nontrivial R
Tactic: have : Nontrivial R := _root_.nontrivial_iff.mpr
    ⟨0, PowerSeries.constantCoeff h, ne_of_mem_of_not_mem I.zero_mem notMem⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (goal)
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
⊢ g.degree =
    (↑((order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)).lift ⋯) :
      WithBot ℕ)
have rw : Ne (α := R ⧸ I)
    ((PowerSeries.coeff g.natDegree : (a : (R ⧸ I)⟦X⟧) → R ⧸ I)
        ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f) :
      R ⧸ I)
    (0 : R ⧸ I) ∧
  ∀ 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: rw [Polynomial.degree_eq_natDegree distinguish.monic.ne_zero, Nat.cast_inj, ← ENat.coe_inj,
    ENat.coe_lift, Eq.comm, PowerSeries.order_eq_nat]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (hypothesis)
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
⊢ Ne (α := R ⧸ I)
      ((PowerSeries.coeff g.natDegree : (a : (R ⧸ I)⟦X⟧) → R ⧸ I)
          ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f) :
        R ⧸ I)
      (0 : R ⧸ I) ∧
    ∀ 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)
have 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⟧)
Tactic: have mapf : f.map (Ideal.Quotient.mk I) = (Polynomial.X ^ g.natDegree : (R ⧸ I)[X]) *
      h.map (Ideal.Quotient.mk I) := by
    simp [← map_eq_X_pow distinguish, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (goal)
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⟧)
⊢ Ne (α := R ⧸ I)
      ((PowerSeries.coeff g.natDegree : (a : (R ⧸ I)⟦X⟧) → R ⧸ I)
          ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f) :
        R ⧸ I)
      (0 : R ⧸ I) ∧
    ∀ 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)
have left : Ne (α := R ⧸ I)
  ((PowerSeries.coeff g.natDegree : (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: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (goal)
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⟧)
left :
  Ne (α := R ⧸ I)
    ((PowerSeries.coeff g.natDegree : (a : (R ⧸ I)⟦X⟧) → R ⧸ I)
        ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f) :
      R ⧸ I)
    (0 : R ⧸ I)
⊢ Ne (α := R ⧸ I)
      ((PowerSeries.coeff g.natDegree : (a : (R ⧸ I)⟦X⟧) → R ⧸ I)
          ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f) :
        R ⧸ I)
      (0 : R ⧸ I) ∧
    ∀ 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)
have right : ∀ 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: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (goal)
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
⊢ (↑g.natDegree : ℕ∞) = order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)
have rw : (↑(WithBot.unbotD 0
        (↑((order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)).lift sorry) :
          WithBot ℕ)) :
    ℕ∞) =
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))
have refine_1 : (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).Monic
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} => ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
refine_1 : (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).Monic
⊢ (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))
have 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)
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} => ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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)
⊢ (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))
have refine_3 : (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff 0 ∉ HPow.hPow (α := Ideal ℤ) (β := ℕ) (ℤ ∙ (↑p : ℤ)) 2
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} => ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).Monic
have refine_1 : ∀ (h : (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)).natDegree = 0), False
Tactic: refine (cyclotomic.monic p ℤ).comp (monic_X_add_C 1) fun h => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)).natDegree = 0
⊢ False
have h₁ : Eq (α := ℕ) 1 0
Tactic: rw [natDegree_X_add_C] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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)
have refine_2 : Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
  (∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x))
Tactic: rw [cyclotomic_prime, geom_sum_X_comp_X_add_one_eq_sum, ← lcoeff_apply, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
| Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    (∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x))
have a : ℤ ∙ (↑p : ℤ)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
a : ℤ ∙ (↑p : ℤ)
| Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    (∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x))
have a₁ : ∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
| ℤ ∙ (↑p : ℤ)
have congr : {(↑p : ℤ)}
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
| ∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x)
have congr : range p
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
congr : range p
| ∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x)
have a : fun (x : ℕ) ↦ (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
| fun (x : ℕ) ↦ (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x)
have a : ∀ (x : ℕ), ((lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x) : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
x : ℕ
| ((lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x) : ℤ)
have a : if x = i then (↑(p.choose (x + 1)) : ℤ) else 0
Tactic: rw [lcoeff_apply, ← C_eq_natCast, C_mul_X_pow_eq_monomial, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
| Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    (∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x))
have a : ∀ (x : ℕ), if x = i then (↑(p.choose (x + 1)) : ℤ) else 0
Tactic: congr
      congr
      next => skip
      congr
      next => skip
      ext
      rw [lcoeff_apply, ← C_eq_natCast, C_mul_X_pow_eq_monomial, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    (∑ x ∈ range p, (lcoeff ℤ i : (a : ℤ[X]) → ℤ) ((↑(p.choose (x + 1)) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x))
have refine_2 : Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ)) (∑ x ∈ range p, if x = i then (↑(p.choose (x + 1)) : ℤ) else 0)
Tactic: conv =>
      congr
      congr
      next => skip
      congr
      next => skip
      ext
      rw [lcoeff_apply, ← C_eq_natCast, C_mul_X_pow_eq_monomial, coeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ)) (∑ x ∈ range p, if x = i then (↑(p.choose (x + 1)) : ℤ) else 0)
have hi₁ : 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
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < p - 1
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ)) (∑ x ∈ range p, if x = i then (↑(p.choose (x + 1)) : ℤ) else 0)
have refine_2 : p ∣ p.choose (i + 1)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (comp (cyclotomic p ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff 0 ∉ HPow.hPow (α := Ideal ℤ) (β := ℕ) (ℤ ∙ (↑p : ℤ)) 2
have refine_3 : ¬HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
⊢ False
have refine_3 : ∀ (k : ℕ) (hk : p = HPow.hPow (β := ℕ) p 2 * k), False
Tactic: obtain ⟨k, hk⟩ := Int.natCast_dvd_natCast.1 h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
k : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * k
⊢ False
have this : 2 ≤ p
Tactic: have : 2 ≤ p := Nat.Prime.two_le hp.out
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
⊢ p < HPow.hPow (β := ℕ) p 2
have nlinarith₁ : HPow.hPow (β := ℕ) p 2 ≤ p → GT.gt (α := ℤ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 2 ∣ (↑p : ℤ)
k : ℕ
hk : p = HPow.hPow (β := ℕ) p 2 * k
this : 2 ≤ p
⊢ False
have this₁ : p < HPow.hPow (β := ℕ) p 2
Tactic: have : p < p ^ 2 := by nlinarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
⊢ False
have refine_3 : ∀ (hk : p = HPow.hPow (β := ℕ) p 2 * 0), False
Tactic: cases k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
⊢ False
have refine_3₁ : ∀ (n : ℕ) (hk : p = HPow.hPow (β := ℕ) p 2 * (n + 1)), False
Tactic: cases k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))
have refine_1 : (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).Monic
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) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_1 : (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).Monic
⊢ (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))
have 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)
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) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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)
⊢ (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).IsEisensteinAt (ℤ ∙ (↑p : ℤ))
have refine_3 : (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff 0 ∉
  HPow.hPow (α := Ideal ℤ) (β := ℕ) (ℤ ∙ (↑p : ℤ)) 2
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) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (comp (cyclotomic (p ^ (n + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1))).Monic
have refine_1 : ∀ (h : (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)).natDegree = 0), False
Tactic: refine (cyclotomic.monic _ ℤ).comp (monic_X_add_C 1) fun h => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h : (HAdd.hAdd (α := ℤ[X]) X ((C : (a : ℤ) → ℤ[X]) 1)).natDegree = 0
⊢ False
have h₁ : Eq (α := ℕ) 1 0
Tactic: rw [natDegree_X_add_C] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hi : i < (comp (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).natDegree
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    ((comp (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i)
have 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)
Tactic: rw [Nat.zero_add, pow_one] at hi ⊢
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
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
⊢ Membership.mem (γ := Ideal ℤ) (ℤ ∙ (↑p : ℤ))
    ((comp (cyclotomic (p ^ (n + 1 + 1)) ℤ) (HAdd.hAdd (α := ℤ[X]) X 1)).coeff i)
have 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
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]