-- Mathlib/Algebra/Polynomial/Monic.lean
lemma Monic.irreducible_iff_natDegree' (hp : p.Monic) : Irreducible p ↔ p ≠ 1 ∧
    ∀ f g : R[X], f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)

Proof state:
case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

Tactic:
constructor <;> intro h f g hf hg he <;> subst he

Result:
case h.mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → f_1.natDegree = 0 ∨ g_1.natDegree = 0
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ (f * g).natDegree)

case h.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h :
  ∀ (f_1 g_1 : R[X]),
    f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → ¬(0 < g_1.natDegree ∧ g_1.natDegree + g_1.natDegree ≤ (f * g).natDegree)
⊢ f.natDegree = 0 ∨ g.natDegree = 0

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

Tactic:
apply and_congr_right'

Result:
case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

Proof state:
case h.mpr.inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : g.natDegree ≤ f.natDegree
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree

Tactic:
exact ⟨f, g, hf, hg, rfl, h.2, add_le_add_right hl _⟩

Result:
no goals

Proof state:
case h.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h :
  ∀ (f_1 g_1 : R[X]),
    f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → ¬(0 < g_1.natDegree ∧ g_1.natDegree + g_1.natDegree ≤ (f * g).natDegree)
⊢ f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
simp_rw [hf.natDegree_mul hg, pos_iff_ne_zero] at h

Result:
case h.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h :
  ∀ (f_1 g_1 : R[X]),
    f_1.Monic →
      g_1.Monic → f_1 * g_1 = f * g → ¬(g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree)
⊢ f.natDegree = 0 ∨ g.natDegree = 0

Proof state:
case h.mpr.inl
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : f.natDegree ≤ g.natDegree
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree

Tactic:
exact ⟨g, f, hg, hf, mul_comm g f, h.1, add_le_add_left hl _⟩

Result:
no goals

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

Tactic:
simp_rw [hp.irreducible_iff_natDegree, mem_Ioc, Nat.le_div_iff_mul_le zero_lt_two, mul_two]

Result:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

Proof state:
case h.mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → f_1.natDegree = 0 ∨ g_1.natDegree = 0
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ (f * g).natDegree)

Tactic:
rw [hf.natDegree_mul hg, add_le_add_iff_right]

Result:
case h.mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → f_1.natDegree = 0 ∨ g_1.natDegree = 0
⊢ ¬(0 < g.natDegree ∧ g.natDegree ≤ f.natDegree)

Proof state:
case h.mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → f_1.natDegree = 0 ∨ g_1.natDegree = 0
⊢ ¬(0 < g.natDegree ∧ g.natDegree ≤ f.natDegree)

Tactic:
exact fun ha => (h f g hf hg rfl).elim (ha.1.trans_le ha.2).ne' ha.1.ne'

Result:
no goals

Proof state:
case h.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h :
  ∀ (f_1 g_1 : R[X]),
    f_1.Monic →
      g_1.Monic → f_1 * g_1 = f * g → ¬(g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree)
⊢ f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
contrapose! h

Result:
case h.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree

Proof state:
case h.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree

Tactic:
obtain hl | hl := le_total f.natDegree g.natDegree

Result:
case h.mpr.inl
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : f.natDegree ≤ g.natDegree
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree

case h.mpr.inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : g.natDegree ≤ f.natDegree
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree