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 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:
have hg : g = C g.leadingCoeff * q ^ m + r := by ring
-- 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)
hg : g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r
obtain :
  ∀ (u : K[X]ˣ) (hu : HPow.hPow (α := K[X]) (map (algebraMap R K) q) m * (↑u : K[X]) = map (algebraMap R K) g),
    Eq (α := K[X]) (map (algebraMap R K) r) 0
⊢ Eq (α := K[X]) (map (algebraMap R K) r) 0

Tactic:
obtain ⟨u, hu⟩ := hf.symm

Premises used: Associated.symm
-- 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)
hg : g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r
u : K[X]ˣ
hu : HPow.hPow (α := K[X]) (map (algebraMap R K) q) m * (↑u : K[X]) = map (algebraMap R K) g
obtain :
  ∀ (a : K) (ha : IsUnit a) (ha' : (C : (a : K) → K[X]) a = (↑u : K[X])), Eq (α := K[X]) (map (algebraMap R K) r) 0
⊢ Eq (α := K[X]) (map (algebraMap R K) r) 0

Tactic:
obtain ⟨a, ha, ha'⟩ := Polynomial.isUnit_iff.mp u.isUnit

Premises used: Polynomial.isUnit_iff, Iff.mp, Units.isUnit
-- 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)
hg : g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r
u : K[X]ˣ
hu : HPow.hPow (α := K[X]) (map (algebraMap R K) q) m * (↑u : K[X]) = map (algebraMap R K) g
a : K
ha : IsUnit a
ha' : (C : (a : K) → K[X]) a = (↑u : K[X])
this : (C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) g.leadingCoeff) = (↑u : K[X])
⊢ Eq (α := K[X]) (map (algebraMap R K) r) 0

Tactic:
simp [r, ← this, Polynomial.map_sub, ← hu, Polynomial.map_mul, map_C,
        Polynomial.map_pow, mul_comm]

Premises used: Polynomial.map_mul, Polynomial.map_pow, mul_comm, Polynomial.map_sub, Polynomial.map_C
-- 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)
hg : g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r
u : K[X]ˣ
hu : HPow.hPow (α := K[X]) (map (algebraMap R K) q) m * (↑u : K[X]) = map (algebraMap R K) g
a : K
ha : IsUnit a
ha' : (C : (a : K) → K[X]) a = (↑u : K[X])
suffices : (C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) g.leadingCoeff) = (↑u : K[X])
⊢ Eq (α := K[X]) (map (algebraMap R K) r) 0

Tactic:
suffices C (algebraMap R K g.leadingCoeff) = u by
      simp [r, ← this, Polynomial.map_sub, ← hu, Polynomial.map_mul, map_C,
        Polynomial.map_pow, mul_comm]
-- 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)
hg : g = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m) + r
u : K[X]ˣ
hu : HPow.hPow (α := K[X]) (map (algebraMap R K) q) m * (↑u : K[X]) = map (algebraMap R K) g
a : K
ha : IsUnit a
ha' : (C : (a : K) → K[X]) a = (↑u : K[X])
rw : (C : (a : K) → K[X]) (leadingCoeff (map (algebraMap R K) g)) = (↑u : K[X])
rw₁ : (C : (a : K) → K[X]) (HPow.hPow (α := K[X]) (map (algebraMap R K) q) m * (↑u : K[X])).leadingCoeff = (↑u : K[X])
rw₂ :
  Eq (α := K[X])
    ((C : (a : K) → K[X])
        (HMul.hMul (β := K[X]) (HPow.hPow (α := K[X]) (map (algebraMap R K) q) m)
            ((C : (a : K) → K[X]) a : K[X])).leadingCoeff :
      K[X])
    ((C : (a : K) → K[X]) a : K[X])
rw₃ :
  Eq (α := K[X])
    ((C : (a : K) → K[X])
        ((HPow.hPow (α := K[X]) (map (algebraMap R K) q) m).leadingCoeff * leadingCoeff ((C : (a : K) → K[X]) a)) :
      K[X])
    ((C : (a : K) → K[X]) a : K[X])
rw₄ :
  Eq (α := K[X]) ((C : (a : K) → K[X]) ((HPow.hPow (α := K[X]) (map (algebraMap R K) q) m).leadingCoeff * a) : K[X])
    ((C : (a : K) → K[X]) a : K[X])
rw₅ : Eq (α := K[X]) ((C : (a : K) → K[X]) (1 * a) : K[X]) ((C : (a : K) → K[X]) a : K[X])
rw₆ rw₇ : Eq (α := K[X]) ((C : (a : K) → K[X]) a : K[X]) ((C : (a : K) → K[X]) a : K[X])
⊢ (C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) g.leadingCoeff) = (↑u : K[X])

Tactic:
rw [← leadingCoeff_map_of_leadingCoeff_ne_zero _ hgP, ← hu, ← ha',
      leadingCoeff_mul, leadingCoeff_C, (hq_monic.map _).pow m, one_mul]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.Monic.pow, Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero, Polynomial.leadingCoeff_C, Polynomial.Monic.map, one_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 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)
hg : 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

Tactic:
have hr : r.map (algebraMap R K) = 0 := by
    obtain ⟨u, hu⟩ := hf.symm
    obtain ⟨a, ha, ha'⟩ := Polynomial.isUnit_iff.mp u.isUnit
    suffices C (algebraMap R K g.leadingCoeff) = u by
      simp [r, ← this, Polynomial.map_sub, ← hu, Polynomial.map_mul, map_C,
        Polynomial.map_pow, mul_comm]
    rw [← leadingCoeff_map_of_leadingCoeff_ne_zero _ hgP, ← hu, ← ha',
      leadingCoeff_mul, leadingCoeff_C, (hq_monic.map _).pow m, one_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 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)
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
right : 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:
use m, r, hg, hr
-- 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_1 : 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)
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
hm : m = 0
right :
  ∀ (hf_prim : ∀ (r : R), (C : (a : R) → R[X]) r ∣ f → IsUnit r)
    (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),
    let 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)),
      let r := g - HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (q ^ m);
      ∀ (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) (hm : m = 0), IsUnit g
⊢ IsUnit g

Tactic:
rw [isPrimitive_iff_isUnit_of_C_dvd] at hf_prim

Premises used: Polynomial.isPrimitive_iff_isUnit_of_C_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 : ∀ (r : R), (C : (a : R) → R[X]) r ∣ f → IsUnit r
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_1 : 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)
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
hm : m = 0
⊢ g = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r

Tactic:
rw [hm, pow_zero, mul_one] at hg

Premises used: pow_zero, mul_one
-- 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 : ∀ (r : R), (C : (a : R) → R[X]) r ∣ f → IsUnit r
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_1 : 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)
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
hm : m = 0
hg₁ : g = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r
⊢ Eq (α := K[X]) (map (algebraMap R K) r) 0

Tactic:
rw [hm, pow_zero, mul_one] at hg

Premises used: pow_zero, mul_one
-- 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 : ∀ (r : R), (C : (a : R) → R[X]) r ∣ f → IsUnit r
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_1 : 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)
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
hm : m = 0
hg₁ : g = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r
hr₁ : Eq (α := K[X]) (map (algebraMap R K) r) 0
⊢ m = 0

Tactic:
rw [hm, pow_zero, mul_one] at hg

Premises used: pow_zero, mul_one
-- 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 : ∀ (r : R), (C : (a : R) → R[X]) r ∣ f → IsUnit r
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_1 : 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)
hg : g = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r
hr : Eq (α := K[X]) (map (algebraMap R K) r) 0
hm : m = 0
this : g.natDegree = 0
obtain :
  ∀ (a : R) (hg_div : (C : (a : R) → R[X]) a ∣ f) (hgP : leadingCoeff ((C : (a : R) → R[X]) a) ∉ P)
    (map_dvd_pow_q : map (algebraMap R K) ((C : (a : R) → R[X]) a) ∣ HPow.hPow (α := K[X]) (map (algebraMap R K) q) p)
    (hf :
      Associated (map (algebraMap R K) ((C : (a : R) → R[X]) a)) (HPow.hPow (α := K[X]) (map (algebraMap R K) q) m)),
    let r :=
      HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        ((C : (a : R) → R[X]) (leadingCoeff ((C : (a : R) → R[X]) a)) * q ^ m);
    ∀ (hg : (C : (a : R) → R[X]) a = (C : (a : R) → R[X]) (leadingCoeff ((C : (a : R) → R[X]) a)) + r)
      (hr : Eq (α := K[X]) (map (algebraMap R K) r) 0) (this : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) = 0),
      IsUnit (M := R[X]) ((C : (a : R) → R[X]) a : R[X])
⊢ IsUnit g

Tactic:
obtain ⟨a, rfl⟩ := Polynomial.natDegree_eq_zero.mp this

Premises used: Iff.mp, Polynomial.natDegree_eq_zero, 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 f : 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 : ∀ (r : R), (C : (a : R) → R[X]) r ∣ f → IsUnit r
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)
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
m : ℕ
hm_1 : m ≤ p
hm : m = 0
a : R
hg_div : (C : (a : R) → R[X]) a ∣ f
hgP : leadingCoeff ((C : (a : R) → R[X]) a) ∉ P
map_dvd_pow_q : map (algebraMap R K) ((C : (a : R) → R[X]) a) ∣ HPow.hPow (α := K[X]) (map (algebraMap R K) q) p
hf : Associated (map (algebraMap R K) ((C : (a : R) → R[X]) a)) (HPow.hPow (α := K[X]) (map (algebraMap R K) q) m)
r : R[X] :=
  HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
    ((C : (a : R) → R[X]) (leadingCoeff ((C : (a : R) → R[X]) a)) * q ^ m)
hg : (C : (a : R) → R[X]) a = (C : (a : R) → R[X]) (leadingCoeff ((C : (a : R) → R[X]) a)) + r
hr : Eq (α := K[X]) (map (algebraMap R K) r) 0
this : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) = 0
h : IsUnit a
⊢ IsUnit (M := R[X]) ((C : (a : R) → R[X]) a : R[X])

Tactic:
apply IsUnit.map

Premises used: IsUnit.map
-- 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_lC : Ne.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) f.leadingCoeff : K) (0 : K)
hf_prim : ∀ (r : R), (C : (a : R) → R[X]) r ∣ f → IsUnit r
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)
P : Ideal R := ker (F := R →+* K) (algebraMap R K)
hP : P.IsPrime
m : ℕ
hm_1 : m ≤ p
hm : m = 0
a : R
hg_div : (C : (a : R) → R[X]) a ∣ f
hgP : leadingCoeff ((C : (a : R) → R[X]) a) ∉ P
map_dvd_pow_q : map (algebraMap R K) ((C : (a : R) → R[X]) a) ∣ HPow.hPow (α := K[X]) (map (algebraMap R K) q) p
hf : Associated (map (algebraMap R K) ((C : (a : R) → R[X]) a)) (HPow.hPow (α := K[X]) (map (algebraMap R K) q) m)
r : R[X] :=
  HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
    ((C : (a : R) → R[X]) (leadingCoeff ((C : (a : R) → R[X]) a)) * q ^ m)
hg : (C : (a : R) → R[X]) a = (C : (a : R) → R[X]) (leadingCoeff ((C : (a : R) → R[X]) a)) + r
hr : Eq (α := K[X]) (map (algebraMap R K) r) 0
this : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) = 0
h : (C : (a : R) → R[X]) a ∣ f
⊢ IsUnit a

Tactic:
apply hf_prim