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 : map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (f %ₘ q) = 0
⊢ False

Tactic:
apply hfmodP2
-- 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_1 : R[X]
h_eq : f = g * h_1
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_1 = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h_1.leadingCoeff : R[X]) (q ^ n) + s
hs : Eq (α := K[X]) (map (algebraMap R K) s) 0
hn0 : n = 0 → IsUnit h_1
hm : ¬m = 0
hn : ¬n = 0
this : f %ₘ q = r * s %ₘ q
h : map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (r * s) = 0
⊢ map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (f %ₘ q) = 0

Tactic:
simp [this, h, map_modByMonic, hq_monic]

Premises used: Polynomial.map_modByMonic
-- 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
this : f %ₘ q = r * s %ₘ q
suffices : map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (r * s) = 0
⊢ map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (f %ₘ q) = 0

Tactic:
suffices h : map (Ideal.Quotient.mk (P ^ 2)) (r * s) = 0 by
        simp [this, h, map_modByMonic, hq_monic]
-- 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
this : f %ₘ q = r * s %ₘ q
a : ∀ (n : ℕ), (map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (r * s)).coeff n = coeff 0 n
⊢ map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (r * s) = 0

Tactic:
ext n
-- 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_1 : ℕ
s : R[X]
hh : h = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n_1) + s
hs : Eq (α := K[X]) (map (algebraMap R K) s) 0
hn0 : n_1 = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n_1 = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
rw : r.coeff x.1 * s.coeff x.2 ∈ P * P
⊢ Eq (α := R ⧸ HPow.hPow (β := ℕ) P 2)
    ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2) : (a : R) → R ⧸ P ^ 2) (r.coeff x.1 * s.coeff x.2) :
      R ⧸ HPow.hPow (β := ℕ) P 2)
    (0 : R ⧸ HPow.hPow (β := ℕ) P 2)

Tactic:
rw [eq_zero_iff_mem, pow_two]

Premises used: pow_two, Ideal.Quotient.eq_zero_iff_mem
-- 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_1 : ℕ
s : R[X]
hh : h = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n_1) + s
hs : Eq (α := K[X]) (map (algebraMap R K) s) 0
hn0 : n_1 = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n_1 = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
hr₁ : r.coeff x.1 ∈ P
hs₁ : s.coeff x.2 ∈ P
⊢ r.coeff x.1 * s.coeff x.2 ∈ P * P

Tactic:
apply mul_mem_mul

Premises used: Ideal.mul_mem_mul
-- 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_1 : ℕ
s : R[X]
hh : h = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n_1) + s
hs : Eq (α := K[X]) (map (algebraMap R K) s) 0
hn0 : n_1 = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n_1 = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
hr₁ : Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (r.coeff x.1) : K) (0 : K)
hr₂ : coeff (map (algebraMap R K) r) x.1 = 0
hr₃ : Eq.{u_2 + 1} (α := K) (coeff 0 x.1) 0
hr₄ hr₅ : Eq.{u_2 + 1} (α := K) 0 0
⊢ r.coeff x.1 ∈ P

Tactic:
rw [mem_ker, ← coeff_map, hr, coeff_zero]

Premises used: Polynomial.coeff_map, RingHom.mem_ker, Polynomial.coeff_zero
-- 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_1 : ℕ
s : R[X]
hh : h = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n_1) + s
hs : Eq (α := K[X]) (map (algebraMap R K) s) 0
hn0 : n_1 = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n_1 = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
x : ℕ × ℕ
hs₁ : Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (s.coeff x.2) : K) (0 : K)
hs₂ : coeff (map (algebraMap R K) s) x.2 = 0
hs₃ : Eq.{u_2 + 1} (α := K) (coeff 0 x.2) 0
hs₄ hs₅ : Eq.{u_2 + 1} (α := K) 0 0
⊢ s.coeff x.2 ∈ P

Tactic:
rw [mem_ker, ← coeff_map, hs, coeff_zero]

Premises used: Polynomial.coeff_map, RingHom.mem_ker, Polynomial.coeff_zero
-- 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_1 : ℕ
s : R[X]
hh : h = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n_1) + s
hs : Eq (α := K[X]) (map (algebraMap R K) s) 0
hn0 : n_1 = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n_1 = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
⊢ ∀ (x : ℕ × ℕ),
    Eq (α := R ⧸ HPow.hPow (β := ℕ) P 2)
      ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2) : (a : R) → R ⧸ P ^ 2) (r.coeff x.1 * s.coeff x.2) :
        R ⧸ HPow.hPow (β := ℕ) P 2)
      (0 : R ⧸ HPow.hPow (β := ℕ) P 2)

Tactic:
have h (x : ℕ × ℕ) : (Ideal.Quotient.mk (P ^ 2)) (r.coeff x.1 * s.coeff x.2) = 0 := by
        rw [eq_zero_iff_mem, pow_two]
        apply mul_mem_mul
        · rw [mem_ker, ← coeff_map, hr, coeff_zero]
        · rw [mem_ker, ← coeff_map, hs, coeff_zero]
-- 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_1 : R[X]
h_eq : f = g * h_1
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_1 : ℕ
s : R[X]
hh : h_1 = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h_1.leadingCoeff : R[X]) (q ^ n_1) + s
hs : Eq (α := K[X]) (map (algebraMap R K) s) 0
hn0 : n_1 = 0 → IsUnit h_1
hm : ¬m = 0
hn : ¬n_1 = 0
this : f %ₘ q = r * s %ₘ q
n : ℕ
h :
  ∀ (x : ℕ × ℕ),
    Eq (α := R ⧸ HPow.hPow (β := ℕ) P 2)
      ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2) : (a : R) → R ⧸ P ^ 2) (r.coeff x.1 * s.coeff x.2) :
        R ⧸ HPow.hPow (β := ℕ) P 2)
      (0 : R ⧸ HPow.hPow (β := ℕ) P 2)
⊢ (map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (r * s)).coeff n = coeff 0 n

Tactic:
simp [-Polynomial.map_mul, coeff_mul, h]

Premises used: Polynomial.map_mul, Polynomial.coeff_mul
-- 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 : f %ₘ q = r * s %ₘ q
⊢ map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (f %ₘ q) = 0

Tactic:
suffices f %ₘ q = (r * s) %ₘ q by
      -- Since the coefficients of `r` and `s` are in `P`, those of `r * s` are in `P ^ 2`
      suffices h : map (Ideal.Quotient.mk (P ^ 2)) (r * s) = 0 by
        simp [this, h, map_modByMonic, hq_monic]
      ext n
      have h (x : ℕ × ℕ) : (Ideal.Quotient.mk (P ^ 2)) (r.coeff x.1 * s.coeff x.2) = 0 := by
        rw [eq_zero_iff_mem, pow_two]
        apply mul_mem_mul
        · rw [mem_ker, ← coeff_map, hr, coeff_zero]
        · rw [mem_ker, ← coeff_map, hs, coeff_zero]
      simp [-Polynomial.map_mul, coeff_mul, h]
-- 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 :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r) *
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n) + s) %ₘ
      q =
    r * s %ₘ q
⊢ f %ₘ q = r * s %ₘ q

Tactic:
rw [h_eq, hg, hh]
-- 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]) (β := R[X])
        ((q.modByMonicHom : (a : R[X]) → R[X])
            (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)) :
          R[X])
        ((q.modByMonicHom : (a : R[X]) → R[X])
            (r * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n)) :
          R[X]) +
      HAdd.hAdd (α := R[X]) (β := R[X])
        ((q.modByMonicHom : (a : R[X]) → R[X])
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) * s) :
          R[X])
        ((q.modByMonicHom : (a : R[X]) → R[X]) (r * s) : R[X]) =
    (q.modByMonicHom : (a : R[X]) → R[X]) (r * s)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r) *
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n) + s) %ₘ
      q =
    r * s %ₘ q

Tactic:
simp only [add_mul, mul_add, map_add, ← modByMonicHom_apply]

Premises used: add_mul, Polynomial.modByMonicHom_apply, map_add, mul_add
-- 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 :
  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
⊢ HAdd.hAdd (α := R[X]) (β := R[X])
        ((q.modByMonicHom : (a : R[X]) → R[X])
            (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)) :
          R[X])
        ((q.modByMonicHom : (a : R[X]) → R[X])
            (r * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) h.leadingCoeff : R[X]) (q ^ n)) :
          R[X]) +
      HAdd.hAdd (α := R[X]) (β := R[X])
        ((q.modByMonicHom : (a : R[X]) → R[X])
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) * s) :
          R[X])
        ((q.modByMonicHom : (a : R[X]) → R[X]) (r * s) : R[X]) =
    (q.modByMonicHom : (a : R[X]) → R[X]) (r * s)

Tactic:
simp only [← add_assoc, modByMonicHom_apply]

Premises used: add_assoc, Polynomial.modByMonicHom_apply
-- 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 :
  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
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:
rw [(modByMonic_eq_zero_iff_dvd hq_monic).mpr]

Premises used: Iff.mpr, Polynomial.modByMonic_eq_zero_iff_dvd