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
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 + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) * s %ₘ q +
      r * s %ₘ q =
    r * s %ₘ q
neg₁ : q ∣ r * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n)
⊢ 0 + 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

Tactic:
rw [(modByMonic_eq_zero_iff_dvd hq_monic).mpr]

Premises used: Iff.mpr, Polynomial.modByMonic_eq_zero_iff_dvd
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
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
⊢ HAdd.hAdd (α := R[X]) 0 0 + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) * s %ₘ q +
      r * s %ₘ q =
    r * s %ₘ q

Tactic:
rw [(modByMonic_eq_zero_iff_dvd hq_monic).mpr]

Premises used: Iff.mpr, Polynomial.modByMonic_eq_zero_iff_dvd
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
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)
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)
⊢ 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

Tactic:
iterate 3 rw [(modByMonic_eq_zero_iff_dvd hq_monic).mpr]

Premises used: Iff.mpr, Polynomial.modByMonic_eq_zero_iff_dvd
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
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
⊢ HAdd.hAdd (α := R[X]) 0 0 + 0 + r * s %ₘ q = r * s %ₘ q

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
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 ∣ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) * s

Tactic:
((dvd_pow_self q hm).mul_left _).mul_right _

Premises used: Dvd.dvd.mul_right, Dvd.dvd.mul_left, dvd_pow_self
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
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 ∣ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) * s

Tactic:
exact ((dvd_pow_self q hm).mul_left _).mul_right _

Premises used: Dvd.dvd.mul_right, Dvd.dvd.mul_left, dvd_pow_self
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
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 : q ∣ HMul.hMul (β := R[X]) r ((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)

Tactic:
simp only [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
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 ∣ HMul.hMul (β := R[X]) r ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) * q ^ n

Tactic:
(dvd_pow_self q hn).mul_left _

Premises used: Dvd.dvd.mul_left, dvd_pow_self
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
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 ∣ HMul.hMul (β := R[X]) r ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) * q ^ n

Tactic:
exact (dvd_pow_self q hn).mul_left _

Premises used: Dvd.dvd.mul_left, dvd_pow_self
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
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 ∣
    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:
((dvd_pow_self q hn).mul_left _).mul_left _

Premises used: Dvd.dvd.mul_left, dvd_pow_self
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
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 ∣
    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:
exact ((dvd_pow_self q hn).mul_left _).mul_left _

Premises used: Dvd.dvd.mul_left, dvd_pow_self
-- 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
⊢ Irreducible (M := (FractionRing (R ⧸ P))[X]) (map (algebraMap R (FractionRing (R ⧸ P))) X)

Tactic:
simp [map_X, irreducible_X]

Premises used: Polynomial.map_X, Polynomial.irreducible_X
-- 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
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)
hfmodP2 :
  map
      (Ideal.Quotient.mk
        (HPow.hPow (α := Ideal R) (β := ℕ) (ker (F := R →+* FractionRing (R ⧸ P)) (algebraMap R (FractionRing (R ⧸ P))))
          2))
      (f %ₘ X) ≠
    0
⊢ Irreducible f

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)

Premises used: Iff.mpr, Polynomial.generalizedEisenstein, Polynomial.natDegree_pos_iff_degree_pos, Polynomial.monic_X
-- 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
hfP₁ : ¬Eq (α := R ⧸ P) ((Ideal.Quotient.mk P : (a : R) → R ⧸ P) f.leadingCoeff : R ⧸ P) (0 : R ⧸ P)
⊢ Ne (α := FractionRing (R ⧸ P))
    ((algebraMap R (FractionRing (R ⧸ P)) : (a : R) → FractionRing (R ⧸ P)) f.leadingCoeff : FractionRing (R ⧸ P))
    (0 : FractionRing (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]

Premises used: Ideal.Quotient.algebraMap_eq, FractionRing, ne_eq, HasQuotient.Quotient, IsScalarTower.algebraMap_eq, RingHom.coe_comp, Function.comp_apply, FaithfulSMul.algebraMap_eq_zero_iff
-- 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
hfP₁ : f.leadingCoeff ∉ P
⊢ ¬Eq (α := R ⧸ P) ((Ideal.Quotient.mk P : (a : R) → R ⧸ P) f.leadingCoeff : R ⧸ P) (0 : R ⧸ P)

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem]

Premises used: Ideal.Quotient.eq_zero_iff_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
⊢ f.leadingCoeff ∉ P

Tactic:
hfl

Premises used: 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
⊢ f.leadingCoeff ∉ P

Tactic:
exact hfl
-- 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
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)))
⊢ 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:
rw [← map_C, ← Polynomial.map_pow, ← Polynomial.map_mul]

Premises used: Polynomial.map_mul, Polynomial.map_pow, 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
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))))
⊢ 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:
simp only [IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P)),
      Quotient.algebraMap_eq, ← map_map]

Premises used: Ideal.Quotient.algebraMap_eq, FractionRing, HasQuotient.Quotient, IsScalarTower.algebraMap_eq, Polynomial.map_map
-- 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
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))
⊢ 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:
congr 1
-- 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
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
⊢ 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:
ext n