R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
⊢ (p ≠ 1 ∧ ∀ (f g : R[X]), Monic f → Monic g → f * g = p → natDegree f = 0 ∨ natDegree g = 0) ↔
    p ≠ 1 ∧ ∀ (f g : R[X]), Monic f → Monic g → f * g = p → ¬(0 < natDegree g ∧ natDegree g + natDegree g ≤ natDegree p)
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), Monic f → Monic g → f * g = p → ¬natDegree g ∈ Ioc 0 (natDegree p / 2)
simp_rw [hp.irreducible_iff_natDegree, mem_Ioc, Nat.le_div_iff_mul_le zero_lt_two, mul_two]
case h
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
⊢ (∀ (f g : R[X]), Monic f → Monic g → f * g = p → natDegree f = 0 ∨ natDegree g = 0) ↔
    ∀ (f g : R[X]), Monic f → Monic g → f * g = p → ¬(0 < natDegree g ∧ natDegree g + natDegree g ≤ natDegree p)
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
⊢ (p ≠ 1 ∧ ∀ (f g : R[X]), Monic f → Monic g → f * g = p → natDegree f = 0 ∨ natDegree g = 0) ↔
    p ≠ 1 ∧ ∀ (f g : R[X]), Monic f → Monic g → f * g = p → ¬(0 < natDegree g ∧ natDegree g + natDegree g ≤ natDegree p)
apply and_congr_right'
case h.mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h : ∀ (f_1 g_1 : R[X]), Monic f_1 → Monic g_1 → f_1 * g_1 = f * g → natDegree f_1 = 0 ∨ natDegree g_1 = 0
⊢ ¬(0 < natDegree g ∧ natDegree g + natDegree g ≤ natDegree (f * g))

case h.mpr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h :
  ∀ (f_1 g_1 : R[X]),
    Monic f_1 → Monic g_1 → f_1 * g_1 = f * g → ¬(0 < natDegree g_1 ∧ natDegree g_1 + natDegree g_1 ≤ natDegree (f * g))
⊢ natDegree f = 0 ∨ natDegree g = 0
case h
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
⊢ (∀ (f g : R[X]), Monic f → Monic g → f * g = p → natDegree f = 0 ∨ natDegree g = 0) ↔
    ∀ (f g : R[X]), Monic f → Monic g → f * g = p → ¬(0 < natDegree g ∧ natDegree g + natDegree g ≤ natDegree p)
constructor <;> intro h f g hf hg he <;> subst he
case h.mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h : ∀ (f_1 g_1 : R[X]), Monic f_1 → Monic g_1 → f_1 * g_1 = f * g → natDegree f_1 = 0 ∨ natDegree g_1 = 0
⊢ ¬(0 < natDegree g ∧ natDegree g ≤ natDegree f)
case h.mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h : ∀ (f_1 g_1 : R[X]), Monic f_1 → Monic g_1 → f_1 * g_1 = f * g → natDegree f_1 = 0 ∨ natDegree g_1 = 0
⊢ ¬(0 < natDegree g ∧ natDegree g + natDegree g ≤ natDegree (f * g))
rw [hf.natDegree_mul hg, add_le_add_iff_right]
no goals
case h.mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h : ∀ (f_1 g_1 : R[X]), Monic f_1 → Monic g_1 → f_1 * g_1 = f * g → natDegree f_1 = 0 ∨ natDegree g_1 = 0
⊢ ¬(0 < natDegree g ∧ natDegree g ≤ natDegree f)
exact fun ha => (h f g hf hg rfl).elim (ha.1.trans_le ha.2).ne' ha.1.ne'
case h.mpr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h :
  ∀ (f_1 g_1 : R[X]),
    Monic f_1 →
      Monic g_1 → f_1 * g_1 = f * g → ¬(natDegree g_1 ≠ 0 ∧ natDegree g_1 + natDegree g_1 ≤ natDegree f + natDegree g)
⊢ natDegree f = 0 ∨ natDegree g = 0
case h.mpr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h :
  ∀ (f_1 g_1 : R[X]),
    Monic f_1 → Monic g_1 → f_1 * g_1 = f * g → ¬(0 < natDegree g_1 ∧ natDegree g_1 + natDegree g_1 ≤ natDegree (f * g))
⊢ natDegree f = 0 ∨ natDegree g = 0
simp_rw [hf.natDegree_mul hg, pos_iff_ne_zero] at h
case h.mpr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h : natDegree f ≠ 0 ∧ natDegree g ≠ 0
⊢ ∃ f_1 g_1,
    Monic f_1 ∧
      Monic g_1 ∧ f_1 * g_1 = f * g ∧ natDegree g_1 ≠ 0 ∧ natDegree g_1 + natDegree g_1 ≤ natDegree f + natDegree g
case h.mpr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h :
  ∀ (f_1 g_1 : R[X]),
    Monic f_1 →
      Monic g_1 → f_1 * g_1 = f * g → ¬(natDegree g_1 ≠ 0 ∧ natDegree g_1 + natDegree g_1 ≤ natDegree f + natDegree g)
⊢ natDegree f = 0 ∨ natDegree g = 0
contrapose! h
case h.mpr.inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h : natDegree f ≠ 0 ∧ natDegree g ≠ 0
hl : natDegree f ≤ natDegree g
⊢ ∃ f_1 g_1,
    Monic f_1 ∧
      Monic g_1 ∧ f_1 * g_1 = f * g ∧ natDegree g_1 ≠ 0 ∧ natDegree g_1 + natDegree g_1 ≤ natDegree f + natDegree g

case h.mpr.inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h : natDegree f ≠ 0 ∧ natDegree g ≠ 0
hl : natDegree g ≤ natDegree f
⊢ ∃ f_1 g_1,
    Monic f_1 ∧
      Monic g_1 ∧ f_1 * g_1 = f * g ∧ natDegree g_1 ≠ 0 ∧ natDegree g_1 + natDegree g_1 ≤ natDegree f + natDegree g
case h.mpr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h : natDegree f ≠ 0 ∧ natDegree g ≠ 0
⊢ ∃ f_1 g_1,
    Monic f_1 ∧
      Monic g_1 ∧ f_1 * g_1 = f * g ∧ natDegree g_1 ≠ 0 ∧ natDegree g_1 + natDegree g_1 ≤ natDegree f + natDegree g
obtain hl | hl := le_total f.natDegree g.natDegree
no goals
case h.mpr.inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h : natDegree f ≠ 0 ∧ natDegree g ≠ 0
hl : natDegree f ≤ natDegree g
⊢ ∃ f_1 g_1,
    Monic f_1 ∧
      Monic g_1 ∧ f_1 * g_1 = f * g ∧ natDegree g_1 ≠ 0 ∧ natDegree g_1 + natDegree g_1 ≤ natDegree f + natDegree g
exact ⟨g, f, hg, hf, mul_comm g f, h.1, add_le_add_left hl _⟩
no goals
case h.mpr.inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q f g : R[X]
hf : Monic f
hg : Monic g
hp : Monic (f * g)
h : natDegree f ≠ 0 ∧ natDegree g ≠ 0
hl : natDegree g ≤ natDegree f
⊢ ∃ f_1 g_1,
    Monic f_1 ∧
      Monic g_1 ∧ f_1 * g_1 = f * g ∧ natDegree g_1 ≠ 0 ∧ natDegree g_1 + natDegree g_1 ≤ natDegree f + natDegree g
exact ⟨f, g, hf, hg, rfl, h.2, add_le_add_right hl _⟩