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 (algebraMap R K) g ∣ HPow.hPow (α := K[X]) (map (algebraMap R K) q) p
have rw : Dvd.dvd (α := K[X]) (map (algebraMap R K) g) (map (algebraMap R K) f)
Tactic: rw [← IsUnit.dvd_mul_left _, ← hfmodP]
-- 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
rw : Dvd.dvd (α := K[X]) (map (algebraMap R K) g) (map (algebraMap R K) f)
⊢ map (algebraMap R K) g ∣ HPow.hPow (α := K[X]) (map (algebraMap R K) q) p
have rw₁ : IsUnit.{u_2} (M := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) f.leadingCoeff) : K[X])
Tactic: rw [← IsUnit.dvd_mul_left _, ← hfmodP]
-- 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
⊢ ∃ (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 map_dvd_pow_q : 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
-- 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 : ℕ) (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 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)
Tactic: obtain ⟨m, hm, hf⟩ := (dvd_prime_pow hq_irr.prime _).mp map_dvd_pow_q
-- 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)
⊢ ∃ (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 hg : 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
-- 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
⊢ Eq (α := K[X]) (map (algebraMap R K) r) 0
have 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
Tactic: obtain ⟨u, hu⟩ := hf.symm
-- 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
⊢ Eq (α := K[X]) (map (algebraMap R K) r) 0
have 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
Tactic: obtain ⟨a, ha, ha'⟩ := Polynomial.isUnit_iff.mp u.isUnit
-- 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])
⊢ Eq (α := K[X]) (map (algebraMap R K) r) 0
have suffices : (C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) g.leadingCoeff) = (↑u : K[X])
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]
-- 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])
⊢ (C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) g.leadingCoeff) = (↑u : K[X])
have rw : (C : (a : K) → K[X]) (leadingCoeff (map (algebraMap R K) g)) = (↑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]
-- 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])
⊢ (C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) g.leadingCoeff) = (↑u : K[X])
have rw₁ : (C : (a : K) → K[X]) (HPow.hPow (α := K[X]) (map (algebraMap R K) q) m * (↑u : K[X])).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]
-- 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])
⊢ (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])
      (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])
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 (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])
⊢ (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])
      ((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])
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 (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])
⊢ (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]) ((HPow.hPow (α := K[X]) (map (algebraMap R K) q) m).leadingCoeff * 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 (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])
⊢ (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]) (1 * 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]