-- Mathlib/Algebra/Polynomial/Roots.lean
theorem Monic.irreducible_iff_degree_lt {p : R[X]} (p_monic : Monic p) (p_1 : p ≠ 1) :
    Irreducible p ↔ ∀ q, degree q ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

Proof state:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ False

Tactic:
refine (h _ (monic_of_isUnit_leadingCoeff_inv_smul hu) ?_ ?_ (dvd_trans ?_ dvd)).elim

Result:
case mp.refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ 0 < (hu.unit⁻¹ • q).degree

case mp.refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ (hu.unit⁻¹ • q).degree ≤ ↑(p.natDegree / 2)

case mp.refine_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ hu.unit⁻¹ • q ∣ q

Proof state:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
⊢ False

Tactic:
have := degree_pos_of_not_isUnit_of_dvd_monic p_monic q_unit dvd

Result:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
⊢ False

Proof state:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
⊢ IsUnit q

Tactic:
by_contra q_unit

Result:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
⊢ False

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

Tactic:
simp only [p_monic.irreducible_iff_lt_natDegree_lt p_1, Finset.mem_Ioc, and_imp,
  natDegree_pos_iff_degree_pos, natDegree_le_iff_degree_le]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p) ↔
    ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

Proof state:
case mp.refine_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ hu.unit⁻¹ • q ∣ q

Tactic:
rw [Units.smul_def, Polynomial.smul_eq_C_mul, (isUnit_C.mpr (Units.isUnit _)).mul_left_dvd]

Result:
no goals

Proof state:
case mp.refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ 0 < (hu.unit⁻¹ • q).degree

Tactic:
rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]

Result:
no goals

Proof state:
case mp.refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ (hu.unit⁻¹ • q).degree ≤ ↑(p.natDegree / 2)

Tactic:
rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q
q : R[X]
a✝ : q.Monic
deg_pos : 0 < q.degree
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
⊢ False

Tactic:
exact deg_pos.ne' <| degree_eq_zero_of_isUnit (h q deg_le dvd)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p) ↔
    ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

Tactic:
constructor

Result:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p) →
    ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q) →
    ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p

Proof state:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
⊢ False

Tactic:
have hu := p_monic.isUnit_leadingCoeff_of_dvd dvd

Result:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ False

Proof state:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p) →
    ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

Tactic:
rintro h q deg_le dvd

Result:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
⊢ IsUnit q

Proof state:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q) →
    ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p

Tactic:
rintro h q _ deg_pos deg_le dvd

Result:
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q
q : R[X]
a✝ : q.Monic
deg_pos : 0 < q.degree
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
⊢ False