awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hfmodP :
  f.coeff n -
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).coeff
        n ∈
    P
⊢ (map (Ideal.Quotient.mk P) f).coeff n =
    (map (Ideal.Quotient.mk P)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X f.natDegree))).coeff
      n

Tactic:
simp only [coeff_map, Ideal.Quotient.mk_eq_mk_iff_sub_mem]

Premises used: Polynomial.coeff_map, Ideal.Quotient.mk_eq_mk_iff_sub_mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hfmodP : (if n = f.natDegree then f.coeff n - f.leadingCoeff else f.coeff n) ∈ P
⊢ f.coeff n -
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).coeff
        n ∈
    P

Tactic:
simp only [coeff_C_mul, coeff_X_pow, mul_ite, mul_one, mul_zero, sub_ite, sub_zero]

Premises used: sub_zero, Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, mul_ite, MulZeroClass.mul_zero, sub_ite, mul_one
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
pos : ∀ (hn : n = f.natDegree), f.coeff n - f.leadingCoeff ∈ P
neg : ∀ (hn : ¬n = f.natDegree), f.coeff n ∈ P
⊢ (if n = f.natDegree then f.coeff n - f.leadingCoeff else f.coeff n) ∈ P

Tactic:
split_ifs with hn
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hn : n = f.natDegree
pos : 0 ∈ P
⊢ f.coeff n - f.leadingCoeff ∈ P

Tactic:
rw [hn, leadingCoeff, sub_self]

Premises used: sub_self, Polynomial.leadingCoeff
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hn : n = f.natDegree
⊢ 0 ∈ P

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hn : n = f.natDegree
⊢ 0 ∈ P

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
pos : ∀ (hn' : n < f.natDegree), f.coeff n ∈ P
neg : ∀ (hn' : ¬n < f.natDegree), f.coeff n ∈ P
⊢ f.coeff n ∈ P

Tactic:
by_cases hn' : n < f.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : n < f.natDegree
⊢ f.coeff n ∈ P

Tactic:
hfP _ (coe_lt_degree.mpr hn')

Premises used: Iff.mpr, Polynomial.coe_lt_degree, Set.Mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : n < f.natDegree
⊢ f.coeff n ∈ P

Tactic:
exact hfP _ (coe_lt_degree.mpr hn')

Premises used: Iff.mpr, Polynomial.coe_lt_degree
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : ¬n < f.natDegree
neg : 0 ∈ P
neg₁ : f.natDegree < n
⊢ f.coeff n ∈ P

Tactic:
rw [f.coeff_eq_zero_of_natDegree_lt]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : ¬n < f.natDegree
⊢ 0 ∈ P

Tactic:
P.zero_mem

Premises used: Set.Mem, Ideal.zero_mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : ¬n < f.natDegree
⊢ 0 ∈ P

Tactic:
exact P.zero_mem

Premises used: Ideal.zero_mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : ¬n < f.natDegree
⊢ f.natDegree < n

Tactic:
simp [Nat.lt_iff_le_and_ne, ← Nat.not_lt, hn', Ne.symm hn]

Premises used: Nat.lt_iff_le_and_ne, Nat.not_lt, Ne.symm
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
hfmodP2 :
  f.coeff 0 ∉
    HPow.hPow (α := Ideal R) (β := ℕ) (ker (F := R →+* FractionRing (R ⧸ P)) (algebraMap R (FractionRing (R ⧸ P)))) 2
⊢ map
      (Ideal.Quotient.mk
        (HPow.hPow (α := Ideal R) (β := ℕ) (ker (F := R →+* FractionRing (R ⧸ P)) (algebraMap R (FractionRing (R ⧸ P))))
          2))
      (f %ₘ X) ≠
    0

Tactic:
rw [modByMonic_X, map_C, ne_eq, C_eq_zero, Ideal.Quotient.eq_zero_iff_mem,
      ← coeff_zero_eq_eval_zero]

Premises used: Polynomial.coeff_zero_eq_eval_zero, Polynomial.C_eq_zero, ne_eq, Ideal.Quotient.eq_zero_iff_mem, Polynomial.modByMonic_X, Polynomial.map_C
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
⊢ f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2

Tactic:
h0
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
h : ker (F := R →+* FractionRing (R ⧸ P)) (algebraMap R (FractionRing (R ⧸ P))) = P
⊢ f.coeff 0 ∉
    HPow.hPow (α := Ideal R) (β := ℕ) (ker (F := R →+* FractionRing (R ⧸ P)) (algebraMap R (FractionRing (R ⧸ P)))) 2

Tactic:
convert! h0
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
h : ker (F := R →+* R ⧸ P) (algebraMap R (R ⧸ P)) = P
h₁ :
  Function.Injective.{u_1 + 1, u_1 + 1} (α := R ⧸ P) (β := FractionRing (R ⧸ P))
    (⇑(algebraMap (R ⧸ P) (FractionRing (R ⧸ P))) : (a : R ⧸ P) → FractionRing (R ⧸ P))
⊢ ker (F := R →+* FractionRing (R ⧸ P))
      (@RingHom.comp _ (R ⧸ P) _ _ Semiring.toNonAssocSemiring _ (algebraMap (R ⧸ P) (FractionRing (R ⧸ P)))
        (algebraMap R (R ⧸ P))) =
    P

Tactic:
rw [ker_comp_of_injective]

Premises used: RingHom.ker_comp_of_injective
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
h : ∀ (a : R), Membership.mem (γ := Ideal R) (ker (F := R →+* R ⧸ P) (algebraMap R (R ⧸ P))) a ↔ a ∈ P
⊢ ker (F := R →+* R ⧸ P) (algebraMap R (R ⧸ P)) = P

Tactic:
ext a
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
a : R
⊢ Membership.mem (γ := Ideal R) (ker (F := R →+* R ⧸ P) (algebraMap R (R ⧸ P))) a ↔ a ∈ P

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R ⧸ P) (β := FractionRing (R ⧸ P))
    (⇑(algebraMap (R ⧸ P) (FractionRing (R ⧸ P))) : (a : R ⧸ P) → FractionRing (R ⧸ P))

Tactic:
FaithfulSMul.algebraMap_injective (R ⧸ P) (FractionRing (R ⧸ P))

Premises used: FractionRing, HasQuotient.Quotient, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), (↑n : WithBot ℕ) < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ HPow.hPow (β := ℕ) P 2
hu : f.IsPrimitive
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R ⧸ P) (β := FractionRing (R ⧸ P))
    (⇑(algebraMap (R ⧸ P) (FractionRing (R ⧸ P))) : (a : R ⧸ P) → FractionRing (R ⧸ P))

Tactic:
exact FaithfulSMul.algebraMap_injective (R ⧸ P) (FractionRing (R ⧸ P))

Premises used: FractionRing, HasQuotient.Quotient, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Goal:
R : Type u_1
inst : CommRing R
f f' : R[X]
I : Ideal R
hf : f.IsDistinguishedAt I
hf' : f'.IsDistinguishedAt I
⊢ (f * f').IsDistinguishedAt I

Tactic:
⟨hf.toIsWeaklyEisensteinAt.mul hf'.toIsWeaklyEisensteinAt, hf.monic.mul hf'.monic⟩

Premises used: Polynomial.IsWeaklyEisensteinAt.mul, Polynomial.IsDistinguishedAt.monic, Polynomial.IsDistinguishedAt.mk, Polynomial.IsDistinguishedAt.toIsWeaklyEisensteinAt, Polynomial.Monic.mul
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
a : ∀ (i : ℕ), (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i
⊢ map (Ideal.Quotient.mk I) f = HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
pos :
  ∀ (ne : i = f.natDegree), (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i
neg :
  ∀ (ne : ¬i = f.natDegree), (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i

Tactic:
by_cases ne : i = f.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
ne : i = f.natDegree
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i

Tactic:
simp [ne, distinguish.monic]

Premises used: Polynomial.IsDistinguishedAt.monic
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
ne : ¬i = f.natDegree
neg :
  ∀ (lt : i < f.natDegree), (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i
neg₁ :
  ∀ (gt : f.natDegree < i), (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i

Tactic:
rcases lt_or_gt_of_ne ne with lt | gt

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
ne : ¬i = f.natDegree
lt : i < f.natDegree
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i

Tactic:
simpa [ne, eq_zero_iff_mem] using (distinguish.mem lt)

Premises used: Ideal.Quotient.eq_zero_iff_mem, Polynomial.IsDistinguishedAt.toIsWeaklyEisensteinAt, Polynomial.IsWeaklyEisensteinAt.mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
ne : ¬i = f.natDegree
gt : f.natDegree < i
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i

Tactic:
simp [ne, Polynomial.coeff_eq_zero_of_natDegree_lt gt]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- 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
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⟧)
⊢ (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:
simp [← map_eq_X_pow distinguish, eq]

Premises used: Polynomial.IsDistinguishedAt.map_eq_X_pow
-- 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
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⟧)
⊢ (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]
-- 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
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⟧)
⊢ 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

Premises used: PowerSeries.coeff, 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
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⟧)
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)
⊢ False

Tactic:
simp [mapf, PowerSeries.coeff_X_pow_mul', eq_zero_iff_mem, notMem] at H

Premises used: Ideal.Quotient.eq_zero_iff_mem, 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
⊢ Nontrivial R

Tactic:
have : Nontrivial R := _root_.nontrivial_iff.mpr
    ⟨0, PowerSeries.constantCoeff h, ne_of_mem_of_not_mem I.zero_mem notMem⟩
-- 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
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)
⊢ g.degree =
    (↑((order.{u_1} (R := R ⧸ I) ((PowerSeries.map (Ideal.Quotient.mk I) : (a : R⟦X⟧) → (R ⧸ I)⟦X⟧) f)).lift ⋯) :
      WithBot ℕ)

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]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.IsDistinguishedAt.monic, Nat.cast_inj, ENat.coe_inj, ENat.coe_lift, Eq.comm, Polynomial.Monic.ne_zero, PowerSeries.order_eq_nat
-- 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
⊢ (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:
simp [← map_eq_X_pow distinguish, eq]

Premises used: Polynomial.IsDistinguishedAt.map_eq_X_pow
-- 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
⊢ (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]
-- 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⟧)
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)
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)
⊢ 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:
constructor
-- 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⟧)
⊢ 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:
simp [mapf, PowerSeries.coeff_X_pow_mul', eq_zero_iff_mem, notMem]

Premises used: Ideal.Quotient.eq_zero_iff_mem, PowerSeries.coeff_X_pow_mul'