-- Mathlib/RingTheory/EisensteinCriterion.lean
theorem irreducible_of_eisenstein_criterion {f : R[X]} {P : Ideal R} (hP : P.IsPrime)
    (hfl : f.leadingCoeff ∉ P) (hfP : ∀ n : ℕ, ↑n < degree f → f.coeff n ∈ P) (hfd0 : 0 < degree f)
    (h0 : f.coeff 0 ∉ P ^ 2) (hu : f.IsPrimitive) : Irreducible f :=
  have hf0 : f ≠ 0 := fun _ => by simp_all only [not_true, Submodule.zero_mem, coeff_zero]
  have hf : f.map (mk P) = C (mk P (leadingCoeff f)) * X ^ natDegree f :=
    map_eq_C_mul_X_pow_of_forall_coeff_mem hfP
  have hfd0 : 0 < f.natDegree := WithBot.coe_lt_coe.1 (lt_of_lt_of_le hfd0 degree_le_natDegree)
  ⟨mt degree_eq_zero_of_isUnit fun h => by simp_all only [lt_irrefl], by
    rintro p q rfl
    rw [Polynomial.map_mul] at hf
    rcases mul_eq_mul_prime_pow
        (show Prime (X : Polynomial (R ⧸ P)) from monic_X.prime_of_degree_eq_one degree_X) hf with
      ⟨m, n, b, c, hmnd, hbc, hp, hq⟩
    have hmn : 0 < m → 0 < n → False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : P.IsPrime
p q : R[X]
hfl : (p * q).leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P
hfd0✝ : 0 < (p * q).degree
h0 : (p * q).coeff 0 ∉ P ^ 2
hu : (p * q).IsPrimitive
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree
hfd0 : 0 < (p * q).natDegree
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = (p * q).natDegree
hbc : C ((mk P) (p * q).leadingCoeff) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hm0 : 0 < m
hn0 : 0 < n
⊢ eval 0 p * eval 0 q ∈ P * P

Tactic:
exact
  Ideal.mul_mem_mul (eval_zero_mem_ideal_of_eq_mul_X_pow hp hm0.ne')
    (eval_zero_mem_ideal_of_eq_mul_X_pow hq hn0.ne')

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : P.IsPrime
p q : R[X]
hfl : (p * q).leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P
hfd0✝ : 0 < (p * q).degree
h0 : (p * q).coeff 0 ∉ P ^ 2
hu : (p * q).IsPrimitive
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree
hfd0 : 0 < (p * q).natDegree
m n : ℕ
b c : (R ⧸ P)[X]
hbc : C ((mk P) (p * q).leadingCoeff) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : (mk P) (p * q).leadingCoeff ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : b.degree = 0 ∧ c.degree = 0
hmp : m ≤ p.natDegree
hnq : n ≤ q.natDegree
hmnd : ¬(p.natDegree = m ∧ q.natDegree = n)
⊢ ¬m + n = p.natDegree + q.natDegree

Tactic:
apply ne_of_lt

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : P.IsPrime
p q : R[X]
hfl : (p * q).leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P
hfd0✝ : 0 < (p * q).degree
h0 : (p * q).coeff 0 ∉ P ^ 2
hu : (p * q).IsPrimitive
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree
hfd0 : 0 < (p * q).natDegree
m n : ℕ
b c : (R ⧸ P)[X]
hbc : C ((mk P) (p * q).leadingCoeff) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : (mk P) (p * q).leadingCoeff ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : b.degree = 0 ∧ c.degree = 0
hmp : m ≤ p.natDegree
hnq : n ≤ q.natDegree
hmnd : ¬(p.natDegree = m ∧ q.natDegree = n)
⊢ m + n < p.natDegree + q.natDegree

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : P.IsPrime
p q : R[X]
hfl : (p * q).leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P
hfd0✝ : 0 < (p * q).degree
h0 : (p * q).coeff 0 ∉ P ^ 2
hu : (p * q).IsPrimitive
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree
hfd0 : 0 < (p * q).natDegree
m n : ℕ
b c : (R ⧸ P)[X]
hbc : C ((mk P) (p * q).leadingCoeff) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : (mk P) (p * q).leadingCoeff ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : b.degree = 0 ∧ c.degree = 0
hmp : m ≤ p.natDegree
hnq : n ≤ q.natDegree
hmnd : ¬(p.natDegree = m ∧ q.natDegree = n)
⊢ m + n < p.natDegree + q.natDegree

Tactic:
rw [not_and_or] at hmnd

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : P.IsPrime
p q : R[X]
hfl : (p * q).leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P
hfd0✝ : 0 < (p * q).degree
h0 : (p * q).coeff 0 ∉ P ^ 2
hu : (p * q).IsPrimitive
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree
hfd0 : 0 < (p * q).natDegree
m n : ℕ
b c : (R ⧸ P)[X]
hbc : C ((mk P) (p * q).leadingCoeff) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : (mk P) (p * q).leadingCoeff ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : b.degree = 0 ∧ c.degree = 0
hmp : m ≤ p.natDegree
hnq : n ≤ q.natDegree
hmnd : ¬p.natDegree = m ∨ ¬q.natDegree = n
⊢ m + n < p.natDegree + q.natDegree

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : P.IsPrime
p q : R[X]
hfl : (p * q).leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P
hfd0✝ : 0 < (p * q).degree
h0 : (p * q).coeff 0 ∉ P ^ 2
hu : (p * q).IsPrimitive
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree
hfd0 : 0 < (p * q).natDegree
m : ℕ
b c : (R ⧸ P)[X]
hbc : C ((mk P) (p * q).leadingCoeff) = b * c
hp : map (mk P) p = b * X ^ m
hpql0 : (mk P) (p * q).leadingCoeff ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : b.degree = 0 ∧ c.degree = 0
hmp : m ≤ p.natDegree
hmnd : m + 0 = (p * q).natDegree
hq : map (mk P) q = c * X ^ 0
hmn : 0 < m → 0 < 0 → False
hnq : 0 ≤ q.natDegree
hpmqn : p.natDegree = m ∧ q.natDegree = 0
⊢ (q * p).IsPrimitive

Tactic:
simpa [mul_comm] using hu

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : P.IsPrime
p q : R[X]
hfl : (p * q).leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P
hfd0✝ : 0 < (p * q).degree
h0 : (p * q).coeff 0 ∉ P ^ 2
hu : (p * q).IsPrimitive
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree
hfd0 : 0 < (p * q).natDegree
n : ℕ
b c : (R ⧸ P)[X]
hbc : C ((mk P) (p * q).leadingCoeff) = b * c
hq : map (mk P) q = c * X ^ n
hpql0 : (mk P) (p * q).leadingCoeff ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : b.degree = 0 ∧ c.degree = 0
hnq : n ≤ q.natDegree
hmnd : 0 + n = (p * q).natDegree
hp : map (mk P) p = b * X ^ 0
hmn : 0 < 0 → 0 < n → False
hmp : 0 ≤ p.natDegree
hpmqn : p.natDegree = 0 ∧ q.natDegree = n
⊢ IsUnit p ∨ IsUnit q

Tactic:
exact Or.inl (isUnit_of_natDegree_eq_zero_of_isPrimitive hu hpmqn.1)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : P.IsPrime
p q : R[X]
hfl : (p * q).leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P
hfd0✝ : 0 < (p * q).degree
h0 : (p * q).coeff 0 ∉ P ^ 2
hu : (p * q).IsPrimitive
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree
hfd0 : 0 < (p * q).natDegree
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = (p * q).natDegree
hbc : C ((mk P) (p * q).leadingCoeff) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : (mk P) (p * q).leadingCoeff ≠ 0
hp0 : p ≠ 0
h : q = 0
⊢ False

Tactic:
simp_all only [eq_self_iff_true, not_true, Ne, mul_zero]

Result:
no goals