awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
⊢ (p.scaleRoots x).IsWeaklyEisensteinAt P

Tactic:
⟨fun i => ?_⟩

Premises used: Polynomial.IsWeaklyEisensteinAt.mk
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
refine : ∀ {n : ℕ} (i : n < (p.scaleRoots x).natDegree), (p.scaleRoots x).coeff n ∈ P
⊢ (p.scaleRoots x).IsWeaklyEisensteinAt P

Tactic:
refine ⟨fun i => ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n : ℕ
i : n < (p.scaleRoots x).natDegree
rw : p.coeff n * x ^ (p.natDegree - n) ∈ P
⊢ (p.scaleRoots x).coeff n ∈ P

Tactic:
rw [coeff_scaleRoots]

Premises used: Polynomial.coeff_scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n : ℕ
i : n < (p.scaleRoots x).natDegree
⊢ 0 < p.natDegree - n

Tactic:
rw [natDegree_scaleRoots, ← tsub_pos_iff_lt] at i

Premises used: tsub_pos_iff_lt, Polynomial.natDegree_scaleRoots
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n : ℕ
i : 0 < p.natDegree - n
⊢ p.coeff n * x ^ (p.natDegree - n) ∈ P

Tactic:
Ideal.mul_mem_left _ _ (Ideal.pow_mem_of_mem P hP _ i)

Premises used: Ideal.pow_mem_of_mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n : ℕ
i : 0 < p.natDegree - n
⊢ p.coeff n * x ^ (p.natDegree - n) ∈ P

Tactic:
exact Ideal.mul_mem_left _ _ (Ideal.pow_mem_of_mem P hP _ i)

Premises used: Ideal.pow_mem_of_mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
rw : Membership.mem (γ := Ideal R) (span {x}) (y ^ (p.scaleRoots x).natDegree)
⊢ x ∣ y ^ p.natDegree

Tactic:
rw [← natDegree_scaleRoots p x, ← Ideal.mem_span_singleton]

Premises used: Polynomial.natDegree_scaleRoots, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
⊢ Membership.mem (γ := Ideal R) (span {x}) (y ^ (p.scaleRoots x).natDegree)

Tactic:
(scaleRoots.isWeaklyEisensteinAt _
          (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem
      ?_ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl

Premises used: Iff.mpr, Polynomial.scaleRoots.isWeaklyEisensteinAt, le_rfl, Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem, Ideal.mem_span_singleton, dvd_refl, Polynomial.monic_scaleRoots_iff
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
dvd_refl : (p.scaleRoots x).IsRoot y
⊢ Membership.mem (γ := Ideal R) (span {x}) (y ^ (p.scaleRoots x).natDegree)

Tactic:
refine
    (scaleRoots.isWeaklyEisensteinAt _
          (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem
      ?_ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl

Premises used: Iff.mpr, Polynomial.scaleRoots.isWeaklyEisensteinAt, le_rfl, Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem, Ideal.mem_span_singleton, dvd_refl, Polynomial.monic_scaleRoots_iff
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : Function.Injective.{u + 1, u_1 + 1} (α := R) (β := A) (⇑f : (a : R) → A)
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
rw :
  ∀ (hf : ∀ (a : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) a : A) (0 : A) ↔ a = 0) {p : R[X]} (hp : p.Monic)
    (x y : R) (z : A) (h : eval₂ f z p = 0) (hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y),
    (p.scaleRoots x).IsRoot y
⊢ (p.scaleRoots x).IsRoot y

Tactic:
rw [injective_iff_map_eq_zero'] at hf

Premises used: injective_iff_map_eq_zero'
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : ∀ (a : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) a : A) (0 : A) ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
⊢ eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) x : A) z) (p.scaleRoots x) = 0

Tactic:
have : eval₂ f _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
f : R →+* A
hf : ∀ (a : R), Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) a : A) (0 : A) ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : HMul.hMul (α := A) ((f : (a : R) → A) x : A) z = (f : (a : R) → A) y
this : eval₂ f (HMul.hMul (α := A) ((f : (a : R) → A) x : A) z) (p.scaleRoots x) = 0
rwa : ∀ (this : eval₂ f ((f : (a : R) → A) y) (p.scaleRoots x) = 0), (p.scaleRoots x).IsRoot y
rwa₁ :
  ∀ (this : Eq.{u_1 + 1} (α := A) ((f : (a : R) → A) (eval y (p.scaleRoots x)) : A) (0 : A)), (p.scaleRoots x).IsRoot y
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : eval y (p.scaleRoots x) = 0), (p.scaleRoots x).IsRoot y
⊢ (p.scaleRoots x).IsRoot y

Tactic:
rwa [hz, Polynomial.eval₂_at_apply, hf] at this

Premises used: Polynomial.eval₂_at_apply
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
A : Type u_1
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsDomain R
inst_3 : Algebra R A
inst_4 : Nontrivial A
inst_5 : Module.IsTorsionFree R A
p : R[X]
hp : p.Monic
x y : R
z : A
h : Eq.{u_1 + 1} (α := A) ((aeval z : (a : R[X]) → A) p : A) (0 : A)
hz : HMul.hMul (β := A) z ((algebraMap R A : (a : R) → A) x : A) = (algebraMap R A : (a : R) → A) y
⊢ x ∣ y ^ p.natDegree

Tactic:
dvd_pow_natDegree_of_eval₂_eq_zero (FaithfulSMul.algebraMap_injective R A) hp x y z h
    ((mul_comm _ _).trans hz)

Premises used: FaithfulSMul.algebraMap_injective, mul_comm, Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.Monic
h : 𝓟 ≠ ⊤
⊢ f.leadingCoeff ∉ 𝓟

Tactic:
hf.leadingCoeff.symm ▸ (Ideal.ne_top_iff_one _).1 h

Premises used: Ideal.ne_top_iff_one, Eq.rec, Iff.mp, Polynomial.Monic.leadingCoeff, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.Monic
h : 𝓟 ≠ ⊤
hmem : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hnotMem : f.coeff 0 ∉ HPow.hPow (β := ℕ) 𝓟 2
⊢ f.IsEisensteinAt 𝓟

Tactic:
{ leading := Polynomial.Monic.leadingCoeff_notMem hf h
    mem := fun hn => hmem hn
    notMem := hnotMem }

Premises used: Polynomial.IsEisensteinAt.mk, Polynomial.Monic.leadingCoeff_notMem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
⊢ f.IsWeaklyEisensteinAt 𝓟

Tactic:
⟨fun h => hf.mem h⟩

Premises used: Polynomial.IsWeaklyEisensteinAt.mk, Polynomial.IsEisensteinAt.mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
inl : ∀ (h₁ : n < f.natDegree), f.coeff n ∈ 𝓟
inr : ∀ (h₂ : f.natDegree < n), f.coeff n ∈ 𝓟
⊢ f.coeff n ∈ 𝓟

Tactic:
rcases ne_iff_lt_or_gt.1 hn with h₁ | h₂

Premises used: ne_iff_lt_or_gt, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₁ : n < f.natDegree
⊢ f.coeff n ∈ 𝓟

Tactic:
hf.mem h₁

Premises used: Polynomial.IsEisensteinAt.mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₁ : n < f.natDegree
⊢ f.coeff n ∈ 𝓟

Tactic:
exact hf.mem h₁

Premises used: Polynomial.IsEisensteinAt.mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : f.natDegree < n
inr : 0 ∈ 𝓟
⊢ f.coeff n ∈ 𝓟

Tactic:
rw [coeff_eq_zero_of_natDegree_lt h₂]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : f.natDegree < n
⊢ 0 ∈ 𝓟

Tactic:
Ideal.zero_mem _

Premises used: Ideal.zero_mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : f.natDegree < n
⊢ 0 ∈ 𝓟

Tactic:
exact Ideal.zero_mem _

Premises used: Ideal.zero_mem
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
hprime : 𝓟.IsPrime
hu : f.IsPrimitive
hfd0 : 0 < f.natDegree
⊢ Irreducible f

Tactic:
irreducible_of_eisenstein_criterion hprime hf.leading (fun _ hn => hf.mem (coe_lt_degree.1 hn))
    (natDegree_pos_iff_degree_pos.1 hfd0) hf.notMem hu

Premises used: Polynomial.coe_lt_degree, Polynomial.irreducible_of_eisenstein_criterion, Polynomial.IsEisensteinAt.mem, Iff.mp, Polynomial.natDegree_pos_iff_degree_pos, Polynomial.IsEisensteinAt.leading, Polynomial.IsEisensteinAt.notMem
-- 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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
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)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
⊢ P.IsPrime

Tactic:
have hP : P.IsPrime := ker_isPrime (algebraMap R K)
-- 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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
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)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
simp : ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K)
⊢ g.leadingCoeff ∉ P

Tactic:
simp only [mem_ker, P]

Premises used: RingHom.mem_ker
-- 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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
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)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
obtain :
  ∀ (h : R[X]) (hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (g * h).leadingCoeff : K) (0 : K))
    (hf_prim : (g * h).IsPrimitive)
    (hfmodP :
      map (algebraMap R K) (g * h) =
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) (g * h).leadingCoeff) : K[X])
          (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)),
    ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K)
⊢ ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K)

Tactic:
obtain ⟨h, rfl⟩ := hg_div

Premises used: rfl
-- 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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
h : R[X]
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (g * h).leadingCoeff : K) (0 : K)
hf_prim : (g * h).IsPrimitive
hfmodP :
  map (algebraMap R K) (g * h) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) (g * h).leadingCoeff) : K[X])
      (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
⊢ ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K) ∧
    ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) h.leadingCoeff : K) (0 : K)

Tactic:
simp only [leadingCoeff_mul, map_mul, ne_eq, mul_eq_zero, not_or] at hf_lC

Premises used: Polynomial.leadingCoeff_mul, mul_eq_zero, ne_eq, not_or, map_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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
h : R[X]
hf_prim : (g * h).IsPrimitive
hfmodP :
  map (algebraMap R K) (g * h) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) (g * h).leadingCoeff) : K[X])
      (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
hf_lC :
  ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K) ∧
    ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) h.leadingCoeff : K) (0 : K)
⊢ ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K)

Tactic:
hf_lC.1

Premises used: And.left
-- 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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
h : R[X]
hf_prim : (g * h).IsPrimitive
hfmodP :
  map (algebraMap R K) (g * h) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) (g * h).leadingCoeff) : K[X])
      (HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
hf_lC :
  ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K) ∧
    ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) h.leadingCoeff : K) (0 : K)
⊢ ¬Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) g.leadingCoeff : K) (0 : K)

Tactic:
exact hf_lC.1

Premises used: And.left
-- 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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
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)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
⊢ g.leadingCoeff ∉ P

Tactic:
have hgP : g.leadingCoeff ∉ P := by
    simp only [mem_ker, P]
    obtain ⟨h, rfl⟩ := hg_div
    simp only [leadingCoeff_mul, map_mul, ne_eq, mul_eq_zero, not_or] at hf_lC
    exact hf_lC.1
-- 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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
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)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
rw : Dvd.dvd (α := K[X]) (map (algebraMap R K) g) (map (algebraMap R K) f)
rw₁ : IsUnit.{u_2} (M := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) f.leadingCoeff) : K[X])
⊢ map (algebraMap R K) g ∣ HPow.hPow (α := K[X]) (map (algebraMap R K) q) p

Tactic:
rw [← IsUnit.dvd_mul_left _, ← hfmodP]

Premises used: IsUnit.dvd_mul_left
-- 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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
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)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
⊢ Dvd.dvd (α := K[X]) (map (algebraMap R K) g) (map (algebraMap R K) f)

Tactic:
Polynomial.map_dvd _ hg_div

Premises used: Polynomial.map_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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
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)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
⊢ Dvd.dvd (α := K[X]) (map (algebraMap R K) g) (map (algebraMap R K) f)

Tactic:
exact Polynomial.map_dvd _ hg_div

Premises used: Polynomial.map_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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
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)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
⊢ IsUnit.{u_2} (M := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) f.leadingCoeff) : K[X])

Tactic:
simp_all
-- 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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
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)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
⊢ map (algebraMap R K) g ∣ HPow.hPow (α := K[X]) (map (algebraMap R K) q) p

Tactic:
have map_dvd_pow_q :
      g.map (algebraMap R K) ∣ q.map (algebraMap R K) ^ p := by
    rw [← IsUnit.dvd_mul_left _, ← hfmodP]
    · exact Polynomial.map_dvd _ hg_div
    · simp_all
-- 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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
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)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ HPow.hPow (α := K[X]) (map (algebraMap R K) q) p
obtain :
  ∀ (m : ℕ) (hm : m ≤ p) (hf : Associated (map (algebraMap R K) g) (HPow.hPow (α := K[X]) (map (algebraMap R K) q) m)),
    ∃ (m : ℕ) (r : R[X]),
      g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r ∧
        Eq (α := K[X]) (map (algebraMap R K) r) 0 ∧ (m = 0 → IsUnit g)
⊢ ∃ (m : ℕ) (r : R[X]),
    g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r ∧
      Eq (α := K[X]) (map (algebraMap R K) r) 0 ∧ (m = 0 → IsUnit g)

Tactic:
obtain ⟨m, hm, hf⟩ := (dvd_prime_pow hq_irr.prime _).mp map_dvd_pow_q

Premises used: Iff.mp, dvd_prime_pow, Irreducible.prime
-- 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 g : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : f.IsPrimitive
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)
hg_div : g ∣ f
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ HPow.hPow (α := K[X]) (map (algebraMap R K) q) p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (HPow.hPow (α := K[X]) (map (algebraMap R K) q) m)
r : R[X] := g - HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m)
⊢ g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r

Tactic:
ring