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 : ∀ (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
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
⊢ g.leadingCoeff ∈ P
have right₃ : coeff ((C : (a : R) → R[X]) g.leadingCoeff) g.natDegree + r.coeff g.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
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
right₃ : coeff ((C : (a : R) → R[X]) g.leadingCoeff) g.natDegree + r.coeff g.natDegree ∈ P
⊢ g.leadingCoeff ∈ P
have right₄ : (if g.natDegree = 0 then g.leadingCoeff else 0) + r.coeff g.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
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
right₃ : coeff ((C : (a : R) → R[X]) g.leadingCoeff) g.natDegree + r.coeff g.natDegree ∈ P
right₄ : (if g.natDegree = 0 then g.leadingCoeff else 0) + r.coeff g.natDegree ∈ P
⊢ g.leadingCoeff ∈ P
have right₅ : 0 + r.coeff g.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
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
right₃ : coeff ((C : (a : R) → R[X]) g.leadingCoeff) g.natDegree + r.coeff g.natDegree ∈ P
right₄ : (if g.natDegree = 0 then g.leadingCoeff else 0) + r.coeff g.natDegree ∈ P
right₅ : 0 + r.coeff g.natDegree ∈ P
⊢ g.leadingCoeff ∈ P
have right₆ : r.coeff g.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
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
right₃ : coeff ((C : (a : R) → R[X]) g.leadingCoeff) g.natDegree + r.coeff g.natDegree ∈ P
right₄ : (if g.natDegree = 0 then g.leadingCoeff else 0) + r.coeff g.natDegree ∈ P
right₅ : 0 + r.coeff g.natDegree ∈ P
right₆ : r.coeff g.natDegree ∈ P
⊢ g.leadingCoeff ∈ P
have right₇ : Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (r.coeff g.natDegree) : K) (0 : K)
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
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
right₃ : coeff ((C : (a : R) → R[X]) g.leadingCoeff) g.natDegree + r.coeff g.natDegree ∈ P
right₄ : (if g.natDegree = 0 then g.leadingCoeff else 0) + r.coeff g.natDegree ∈ P
right₅ : 0 + r.coeff g.natDegree ∈ P
right₆ : r.coeff g.natDegree ∈ P
right₇ : Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (r.coeff g.natDegree) : K) (0 : K)
⊢ g.leadingCoeff ∈ P
have right₈ : coeff (map (algebraMap R K) r) g.natDegree = 0
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
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
right₃ : coeff ((C : (a : R) → R[X]) g.leadingCoeff) g.natDegree + r.coeff g.natDegree ∈ P
right₄ : (if g.natDegree = 0 then g.leadingCoeff else 0) + r.coeff g.natDegree ∈ P
right₅ : 0 + r.coeff g.natDegree ∈ P
right₆ : r.coeff g.natDegree ∈ P
right₇ : Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (r.coeff g.natDegree) : K) (0 : K)
right₈ : coeff (map (algebraMap R K) r) g.natDegree = 0
⊢ g.leadingCoeff ∈ P
have right₉ : Eq.{u_2 + 1} (α := K) (coeff 0 g.natDegree) 0
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
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
right₃ : coeff ((C : (a : R) → R[X]) g.leadingCoeff) g.natDegree + r.coeff g.natDegree ∈ P
right₄ : (if g.natDegree = 0 then g.leadingCoeff else 0) + r.coeff g.natDegree ∈ P
right₅ : 0 + r.coeff g.natDegree ∈ P
right₆ : r.coeff g.natDegree ∈ P
right₇ : Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (r.coeff g.natDegree) : K) (0 : K)
right₈ : coeff (map (algebraMap R K) r) g.natDegree = 0
right₉ : Eq.{u_2 + 1} (α := K) (coeff 0 g.natDegree) 0
⊢ g.leadingCoeff ∈ P
have right₁₀ : Eq.{u_2 + 1} (α := K) 0 0
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 : 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
⊢ IsUnit g ∨ IsUnit h
have obtain : ∀ (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), IsUnit g ∨ IsUnit h
Tactic: obtain ⟨m, r, hg, hr, hm0⟩ :=
      generalizedEisenstein_aux hq_irr hq_monic hfP hf_prim hfmodP (h_eq ▸ dvd_mul_right g h)
-- 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_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
⊢ IsUnit g ∨ IsUnit h
have obtain : ∀ (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), IsUnit g ∨ IsUnit h
Tactic: obtain ⟨n, s, hh, hs, hn0⟩ :=
      generalizedEisenstein_aux hq_irr hq_monic hfP hf_prim hfmodP (h_eq ▸ dvd_mul_left h g)
-- 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_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
⊢ IsUnit g ∨ IsUnit h
have pos : ∀ (hm : m = 0), IsUnit g ∨ IsUnit h
Tactic: by_cases hm : m = 0
-- 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_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
pos : ∀ (hm : m = 0), IsUnit g ∨ IsUnit h
⊢ IsUnit g ∨ IsUnit h
have neg : ∀ (hm : ¬m = 0), IsUnit g ∨ IsUnit h
Tactic: by_cases hm : m = 0
-- 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_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
⊢ IsUnit g ∨ IsUnit h
have pos : IsUnit g
Tactic: left