-- Mathlib/Algebra/Polynomial/Monic.lean
/-- Alternate phrasing of `Polynomial.Monic.irreducible_iff_natDegree'` where we only have to check
one divisor at a time. -/
lemma Monic.irreducible_iff_lt_natDegree_lt {p : R[X]} (hp : p.Monic) (hp1 : p ≠ 1) :
    Irreducible p ↔ ∀ q, Monic q → natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) → ¬ q ∣ p

Proof state:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hg : g.Monic
hp : (f * g).Monic
hp1 : f * g ≠ 1
h : ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 ((f * g).natDegree / 2) → ¬q ∣ f * g
hdg : g.natDegree ∈ Ioc 0 ((f * g).natDegree / 2)
⊢ False

Tactic:
exact h g hg hdg (dvd_mul_left g f)

Result:
no goals

Proof state:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) →
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
rintro h g hg hdg ⟨f, rfl⟩

Result:
case mp.intro
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
g : R[X]
hg : g.Monic
f : R[X]
hp : (g * f).Monic
hp1 : g * f ≠ 1
h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = g * f → g_1.natDegree ∉ Ioc 0 ((g * f).natDegree / 2)
hdg : g.natDegree ∈ Ioc 0 ((g * f).natDegree / 2)
⊢ False

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
rw [hp.irreducible_iff_natDegree', and_iff_right hp1]

Result:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
constructor

Result:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) →
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)

Proof state:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)

Tactic:
rintro h f g - hg rfl hdg

Result:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hg : g.Monic
hp : (f * g).Monic
hp1 : f * g ≠ 1
h : ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 ((f * g).natDegree / 2) → ¬q ∣ f * g
hdg : g.natDegree ∈ Ioc 0 ((f * g).natDegree / 2)
⊢ False

Proof state:
case mp.intro
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
g : R[X]
hg : g.Monic
f : R[X]
hp : (g * f).Monic
hp1 : g * f ≠ 1
h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = g * f → g_1.natDegree ∉ Ioc 0 ((g * f).natDegree / 2)
hdg : g.natDegree ∈ Ioc 0 ((g * f).natDegree / 2)
⊢ False

Tactic:
exact h f g (hg.of_mul_monic_left hp) hg (mul_comm f g) hdg

Result:
no goals