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 : 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 h₁ h₂ 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
⊢ (C : (a : R) → R[X]) a ∣ f

Tactic:
rwa [leadingCoeff_C] at hgP

Premises used: Polynomial.leadingCoeff_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 : ∀ (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
right : g.natDegree = 0
⊢ IsUnit g

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
-- 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
right : ∀ (hg' : ¬g.natDegree = 0), False
⊢ g.natDegree = 0

Tactic:
by_contra hg'
-- 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
hg' : ¬g.natDegree = 0
right : g.leadingCoeff ∈ P
⊢ False

Tactic:
apply hgP
-- 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
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
right₁₀ right₁₁ : Eq.{u_2 + 1} (α := K) 0 0
⊢ g.leadingCoeff ∈ P

Tactic:
rw [hg, leadingCoeff, coeff_add, ← hg, coeff_C, if_neg hg', zero_add,
    mem_ker, ← coeff_map, hr, coeff_zero]

Premises used: Polynomial.coeff_map, RingHom.mem_ker, Polynomial.leadingCoeff, Polynomial.coeff_add, Polynomial.coeff_C, zero_add, Polynomial.coeff_zero, if_neg
-- 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_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)
hfmodP2 :
  map (Ideal.Quotient.mk (HPow.hPow (α := Ideal R) (β := ℕ) (ker (F := R →+* K) (algebraMap R K)) 2)) (f %ₘ q) ≠ 0
h : f.degree = 0
⊢ False

Tactic:
simp_all [natDegree_pos_iff_degree_pos]

Premises used: Polynomial.natDegree_pos_iff_degree_pos
-- 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_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)
hfmodP2 :
  map (Ideal.Quotient.mk (HPow.hPow (α := Ideal R) (β := ℕ) (ker (F := R →+* K) (algebraMap R K)) 2)) (f %ₘ q) ≠ 0
g h : R[X]
h_eq : f = g * h
⊢ let P : Ideal R := ker (F := R →+* K) (algebraMap R K);
  map (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P 2)) (f %ₘ q) ≠ 0

Tactic:
set P : Ideal R := ker (algebraMap R K)

Premises used: Algebra.algebraMap, Ideal, RingHom.ker
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f : 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
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
⊢ 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)

Premises used: _private.0.Polynomial.generalizedEisenstein_aux
-- 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_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
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
⊢ 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)

Premises used: _private.0.Polynomial.generalizedEisenstein_aux
-- 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_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
neg : ∀ (hm : ¬m = 0), IsUnit g ∨ IsUnit h
⊢ IsUnit g ∨ IsUnit h

Tactic:
by_cases hm : m = 0
-- 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_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
pos : IsUnit g
⊢ IsUnit g ∨ IsUnit h

Tactic:
left
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
q f : 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

Tactic:
hm0 hm
-- 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_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

Tactic:
exact hm0 hm
-- 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_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
pos : ∀ (hn : n = 0), IsUnit g ∨ IsUnit h
neg : ∀ (hn : ¬n = 0), IsUnit g ∨ IsUnit h
⊢ IsUnit g ∨ IsUnit h

Tactic:
by_cases hn : n = 0
-- 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_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
hn : n = 0
pos : IsUnit h
⊢ IsUnit g ∨ IsUnit h

Tactic:
right
-- 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_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
hn : n = 0
⊢ IsUnit h

Tactic:
hn0 hn
-- 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_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
hn : n = 0
⊢ IsUnit h

Tactic:
exact hn0 hn
-- 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_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
hn : ¬n = 0
neg : False
⊢ IsUnit g ∨ IsUnit h

Tactic:
exfalso