awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hfmodP :
  map (algebraMap R K) f =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) f.leadingCoeff) : K[X])
      (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r
hr : Eq (α := K[X]) (map (algebraMap R K) r) 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n) + s
hs : Eq (α := K[X]) (map (algebraMap R K) s) 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
neg : HAdd.hAdd (α := R[X]) 0 0 + 0 + r * s %ₘ q = r * s %ₘ q
neg₁ : q ∣ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) * s
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n) %ₘ
            q +
          r * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n) %ₘ q +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) * s %ₘ q +
      r * s %ₘ q =
    r * s %ₘ q
have neg₂ : q ∣ r * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n)
Tactic: iterate 3 rw [(modByMonic_eq_zero_iff_dvd hq_monic).mpr]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hfmodP :
  map (algebraMap R K) f =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) f.leadingCoeff) : K[X])
      (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r
hr : Eq (α := K[X]) (map (algebraMap R K) r) 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n) + s
hs : Eq (α := K[X]) (map (algebraMap R K) s) 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
neg : HAdd.hAdd (α := R[X]) 0 0 + 0 + r * s %ₘ q = r * s %ₘ q
neg₁ : q ∣ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) * s
neg₂ : q ∣ r * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n)
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n) %ₘ
            q +
          r * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n) %ₘ q +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) * s %ₘ q +
      r * s %ₘ q =
    r * s %ₘ q
have neg₃ : q ∣
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) *
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n)
Tactic: iterate 3 rw [(modByMonic_eq_zero_iff_dvd hq_monic).mpr]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hfmodP :
  map (algebraMap R K) f =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) f.leadingCoeff) : K[X])
      (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r
hr : Eq (α := K[X]) (map (algebraMap R K) r) 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n) + s
hs : Eq (α := K[X]) (map (algebraMap R K) s) 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ q ∣ r * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n)
have neg : q ∣ HMul.hMul (β := R[X]) r ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) * q ^ n
Tactic: simp only [← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ Irreducible f
have hfP₁ : Ne (α := FractionRing (R ⧸ P))
  ((algebraMap R (FractionRing (R ⧸ P)) : (a : R) → FractionRing (R ⧸ P)) f.leadingCoeff : FractionRing (R ⧸ P))
  (0 : FractionRing (R ⧸ P))
Tactic: apply generalizedEisenstein (K := FractionRing (R ⧸ P)) (q := X) (p := f.natDegree)
    (by simp [map_X, irreducible_X]) monic_X hu
    (natDegree_pos_iff_degree_pos.mpr hfd0)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
hfP₁ :
  Ne (α := FractionRing (R ⧸ P))
    ((algebraMap R (FractionRing (R ⧸ P)) : (a : R) → FractionRing (R ⧸ P)) f.leadingCoeff : FractionRing (R ⧸ P))
    (0 : FractionRing (R ⧸ P))
⊢ Irreducible f
have hfmodP : map (algebraMap R (FractionRing (R ⧸ P))) f =
  HMul.hMul (α := (FractionRing (R ⧸ P))[X])
    ((C : (a : FractionRing (R ⧸ P)) → (FractionRing (R ⧸ P))[X])
        ((algebraMap R (FractionRing (R ⧸ P)) : (a : R) → FractionRing (R ⧸ P)) f.leadingCoeff) :
      (FractionRing (R ⧸ P))[X])
    (HPow.hPow (α := (FractionRing (R ⧸ P))[X]) (map (algebraMap R (FractionRing (R ⧸ P))) X) f.natDegree)
Tactic: apply generalizedEisenstein (K := FractionRing (R ⧸ P)) (q := X) (p := f.natDegree)
    (by simp [map_X, irreducible_X]) monic_X hu
    (natDegree_pos_iff_degree_pos.mpr hfd0)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
hfP₁ :
  Ne (α := FractionRing (R ⧸ P))
    ((algebraMap R (FractionRing (R ⧸ P)) : (a : R) → FractionRing (R ⧸ P)) f.leadingCoeff : FractionRing (R ⧸ P))
    (0 : FractionRing (R ⧸ P))
hfmodP :
  map (algebraMap R (FractionRing (R ⧸ P))) f =
    HMul.hMul (α := (FractionRing (R ⧸ P))[X])
      ((C : (a : FractionRing (R ⧸ P)) → (FractionRing (R ⧸ P))[X])
          ((algebraMap R (FractionRing (R ⧸ P)) : (a : R) → FractionRing (R ⧸ P)) f.leadingCoeff) :
        (FractionRing (R ⧸ P))[X])
      (HPow.hPow (α := (FractionRing (R ⧸ P))[X]) (map (algebraMap R (FractionRing (R ⧸ P))) X) f.natDegree)
⊢ Irreducible f
have hfmodP2 : map
    (Ideal.Quotient.mk
      (HPow.hPow (α := Ideal R) (β := ℕ) (ker (F := R →+* FractionRing (R ⧸ P)) (algebraMap R (FractionRing (R ⧸ P))))
        2))
    (f %ₘ X) ≠
  0
Tactic: apply generalizedEisenstein (K := FractionRing (R ⧸ P)) (q := X) (p := f.natDegree)
    (by simp [map_X, irreducible_X]) monic_X hu
    (natDegree_pos_iff_degree_pos.mpr hfd0)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ Ne (α := FractionRing (R ⧸ P))
    ((algebraMap R (FractionRing (R ⧸ P)) : (a : R) → FractionRing (R ⧸ P)) f.leadingCoeff : FractionRing (R ⧸ P))
    (0 : FractionRing (R ⧸ P))
have hfP₁ : ¬Eq (α := R ⧸ P) ((Ideal.Quotient.mk P : (a : R) → R ⧸ P) f.leadingCoeff : R ⧸ P) (0 : R ⧸ P)
Tactic: simp only [IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P)),
      Quotient.algebraMap_eq, coe_comp, Function.comp_apply, ne_eq,
      FaithfulSMul.algebraMap_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ map (algebraMap R (FractionRing (R ⧸ P))) f =
    HMul.hMul (α := (FractionRing (R ⧸ P))[X])
      ((C : (a : FractionRing (R ⧸ P)) → (FractionRing (R ⧸ P))[X])
          ((algebraMap R (FractionRing (R ⧸ P)) : (a : R) → FractionRing (R ⧸ P)) f.leadingCoeff) :
        (FractionRing (R ⧸ P))[X])
      (HPow.hPow (α := (FractionRing (R ⧸ P))[X]) (map (algebraMap R (FractionRing (R ⧸ P))) X) f.natDegree)
have hfmodP : Eq (α := (FractionRing (R ⧸ P))[X]) (map (algebraMap R (FractionRing (R ⧸ P))) f)
  (map (algebraMap R (FractionRing (R ⧸ P)))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)))
Tactic: rw [← map_C, ← Polynomial.map_pow, ← Polynomial.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ Eq (α := (FractionRing (R ⧸ P))[X]) (map (algebraMap R (FractionRing (R ⧸ P))) f)
    (map (algebraMap R (FractionRing (R ⧸ P)))
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)))
have hfmodP : Eq (α := (FractionRing (R ⧸ P))[X]) (map (algebraMap (R ⧸ P) (FractionRing (R ⧸ P))) (map (Ideal.Quotient.mk P) f))
  (map (algebraMap (R ⧸ P) (FractionRing (R ⧸ P)))
    (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))))
Tactic: simp only [IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P)),
      Quotient.algebraMap_eq, ← map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ Eq (α := (FractionRing (R ⧸ P))[X]) (map (algebraMap (R ⧸ P) (FractionRing (R ⧸ P))) (map (Ideal.Quotient.mk P) f))
    (map (algebraMap (R ⧸ P) (FractionRing (R ⧸ P)))
      (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))))
have hfmodP : map (Ideal.Quotient.mk P) f =
  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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ map (Ideal.Quotient.mk P) f =
    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))
have hfmodP : ∀ (n : ℕ),
  (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: ext n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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 : ℕ
⊢ (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
have 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
Tactic: simp only [coeff_map, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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 : ℕ
⊢ 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
have hfmodP : (if n = f.natDegree then f.coeff n - f.leadingCoeff else f.coeff n) ∈ P
Tactic: simp only [coeff_C_mul, coeff_X_pow, mul_ite, mul_one, mul_zero, sub_ite, sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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 : ℕ
⊢ (if n = f.natDegree then f.coeff n - f.leadingCoeff else f.coeff n) ∈ P
have pos : ∀ (hn : n = f.natDegree), f.coeff n - f.leadingCoeff ∈ P
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ (if n = f.natDegree then f.coeff n - f.leadingCoeff else f.coeff n) ∈ P
have neg : ∀ (hn : ¬n = f.natDegree), f.coeff n ∈ P
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ f.coeff n - f.leadingCoeff ∈ P
have pos : 0 ∈ P
Tactic: rw [hn, leadingCoeff, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ f.coeff n ∈ P
have pos : ∀ (hn' : n < f.natDegree), f.coeff n ∈ P
Tactic: by_cases hn' : n < f.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ f.coeff n ∈ P
have neg : ∀ (hn' : ¬n < f.natDegree), f.coeff n ∈ P
Tactic: by_cases hn' : n < f.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
have neg : 0 ∈ P
Tactic: rw [f.coeff_eq_zero_of_natDegree_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ f.coeff n ∈ P
have neg₁ : f.natDegree < n
Tactic: rw [f.coeff_eq_zero_of_natDegree_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ map
      (Ideal.Quotient.mk
        (HPow.hPow (α := Ideal R) (β := ℕ) (ker (F := R →+* FractionRing (R ⧸ P)) (algebraMap R (FractionRing (R ⧸ P))))
          2))
      (f %ₘ X) ≠
    0
have hfmodP2 : f.coeff 0 ∉
  HPow.hPow (α := Ideal R) (β := ℕ) (ker (F := R →+* FractionRing (R ⧸ P)) (algebraMap R (FractionRing (R ⧸ P)))) 2
Tactic: rw [modByMonic_X, map_C, ne_eq, C_eq_zero, Ideal.Quotient.eq_zero_iff_mem,
      ← coeff_zero_eq_eval_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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 (α := Ideal R) (β := ℕ) (ker (F := R →+* FractionRing (R ⧸ P)) (algebraMap R (FractionRing (R ⧸ P)))) 2
have h : ker (F := R →+* FractionRing (R ⧸ P)) (algebraMap R (FractionRing (R ⧸ P))) = P
Tactic: convert! h0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ ker (F := R →+* FractionRing (R ⧸ P))
      (@RingHom.comp _ (R ⧸ P) _ _ Semiring.toNonAssocSemiring _ (algebraMap (R ⧸ P) (FractionRing (R ⧸ P)))
        (algebraMap R (R ⧸ P))) =
    P
have h : ker (F := R →+* R ⧸ P) (algebraMap R (R ⧸ P)) = P
Tactic: rw [ker_comp_of_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ ker (F := R →+* FractionRing (R ⧸ P))
      (@RingHom.comp _ (R ⧸ P) _ _ Semiring.toNonAssocSemiring _ (algebraMap (R ⧸ P) (FractionRing (R ⧸ P)))
        (algebraMap R (R ⧸ P))) =
    P
have 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))
Tactic: rw [ker_comp_of_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
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
⊢ ker (F := R →+* R ⧸ P) (algebraMap R (R ⧸ P)) = P
have h : ∀ (a : R), Membership.mem (γ := Ideal R) (ker (F := R →+* R ⧸ P) (algebraMap R (R ⧸ P))) a ↔ a ∈ P
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
⊢ map (Ideal.Quotient.mk I) f = HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree
have a : ∀ (i : ℕ), (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
I : Ideal R
distinguish : f.IsDistinguishedAt I
i : ℕ
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i
have pos : ∀ (ne : i = f.natDegree), (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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (goal)
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
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i
have neg : ∀ (ne : ¬i = f.natDegree), (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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (goal)
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
have neg : ∀ (lt : i < f.natDegree), (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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished (goal)
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
⊢ (map (Ideal.Quotient.mk I) f).coeff i = (HPow.hPow (α := (R ⧸ I)[X]) X f.natDegree).coeff i
have neg₁ : ∀ (gt : f.natDegree < 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