awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f 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])
⊢ (C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) g.leadingCoeff) = (↑u : K[X])
have rw₆ : Eq (α := K[X]) ((C : (a : K) → K[X]) a : K[X]) ((C : (a : K) → K[X]) a : K[X])
Tactic: rw [← leadingCoeff_map_of_leadingCoeff_ne_zero _ hgP, ← hu, ← ha',
      leadingCoeff_mul, leadingCoeff_C, (hq_monic.map _).pow m, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (hypothesis)
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
⊢ ∃ (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)
have hr : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f 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
⊢ ∃ (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)
have right : m = 0 → IsUnit g
Tactic: use m, r, hg, hr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f 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
⊢ IsUnit g
have 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
Tactic: rw [isPrimitive_iff_isUnit_of_C_dvd] at hf_prim
Cleared hypotheses: hf_prim, hfmodP, hg_div, P, hP, hgP, map_dvd_pow_q, m, hm_1, hf, r, hg, hr, hm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (hypothesis)
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
⊢ IsUnit g
have hg₁ : g = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r
Tactic: rw [hm, pow_zero, mul_one] at hg
Cleared hypotheses: hg, hr, hm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f 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
⊢ IsUnit g
have 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])
Tactic: obtain ⟨a, rfl⟩ := Polynomial.natDegree_eq_zero.mp this
Cleared hypotheses: g, hg_div, hgP, map_dvd_pow_q, hf, r, hg, hr, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_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
⊢ IsUnit (M := R[X]) ((C : (a : R) → R[X]) a : R[X])
have h : IsUnit a
Tactic: apply IsUnit.map
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (M := K[X]) (map (algebraMap R K) q)
hq_monic : q.Monic
hf_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
⊢ (C : (a : R) → R[X]) a ∣ f
have h : ∀ (hgP : 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),
    (C : (a : R) → R[X]) a ∣ f
Tactic: rwa [leadingCoeff_C] at hgP
Cleared hypotheses: hgP, map_dvd_pow_q, hf, r, hg, hr, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f 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
⊢ IsUnit g
have right : g.natDegree = 0
Tactic: suffices g.natDegree = 0 by
    obtain ⟨a, rfl⟩ := Polynomial.natDegree_eq_zero.mp this
    apply IsUnit.map
    apply hf_prim
    rwa [leadingCoeff_C] at hgP
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f 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
⊢ g.natDegree = 0
have right : ∀ (hg' : ¬g.natDegree = 0), False
Tactic: by_contra hg'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f 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
hg' : ¬g.natDegree = 0
⊢ False
have right : g.leadingCoeff ∈ P
Tactic: apply hgP
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f 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
hg' : ¬g.natDegree = 0
⊢ g.leadingCoeff ∈ P
have right : (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r).leadingCoeff ∈ P
Tactic: rw [hg, leadingCoeff, coeff_add, ← hg, coeff_C, if_neg hg', zero_add,
    mem_ker, ← coeff_map, hr, coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f 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
hg' : ¬g.natDegree = 0
right : (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r).leadingCoeff ∈ P
⊢ g.leadingCoeff ∈ P
have right₁ : (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r).coeff
    (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r).natDegree ∈
  P
Tactic: rw [hg, leadingCoeff, coeff_add, ← hg, coeff_C, if_neg hg', zero_add,
    mem_ker, ← coeff_map, hr, coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f 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
hg' : ¬g.natDegree = 0
right : (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r).leadingCoeff ∈ P
right₁ :
  (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r).coeff
      (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r).natDegree ∈
    P
⊢ g.leadingCoeff ∈ P
have right₂ : coeff ((C : (a : R) → R[X]) g.leadingCoeff)
      (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r).natDegree +
    r.coeff (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) r).natDegree ∈
  P
Tactic: rw [hg, leadingCoeff, coeff_add, ← hg, coeff_C, if_neg hg', zero_add,
    mem_ker, ← coeff_map, hr, coeff_zero]