-- Mathlib/Algebra/Polynomial/Monic.lean
lemma Monic.not_irreducible_iff_exists_add_mul_eq_coeff (hm : p.Monic) (hnd : p.natDegree = 2) :
    ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Proof state:
case inr.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂) →
    ∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)

Tactic:
rintro ⟨c₁, c₂, hmul, hadd⟩

Result:
case inr.mpr.intro.intro.intro
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ ∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)

Proof state:
case inr.mpr.intro.intro.intro.refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ 0 < 1 ∧ 1 ≤ 2 / 2

Tactic:
simp

Result:
no goals

Proof state:
case inr.mpr.intro.intro.intro.refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₁) * (X + C c₂) = p

Tactic:
rw [p.as_sum_range_C_mul_X_pow, hnd, Finset.sum_range_succ, Finset.sum_range_succ,
  Finset.sum_range_one, ← hnd, hm.coeff_natDegree, hnd, hmul, hadd, C_mul, C_add, C_1]

Result:
case inr.mpr.intro.intro.intro.refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₁) * (X + C c₂) = C c₁ * C c₂ * X ^ 0 + (C c₁ + C c₂) * X ^ 1 + 1 * X ^ 2

Proof state:
case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
hm : Monic 1
hnd : natDegree 1 = 2
⊢ False

Tactic:
simp [natDegree_one] at hnd

Result:
no goals

Proof state:
case inr.mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) →
    ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
rintro ⟨a, b, ha, hb, rfl, hdb⟩

Result:
case inr.mp.intro.intro.intro.intro.intro
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
a b : R[X]
ha : a.Monic
hb : b.Monic
hdb : b.natDegree ∈ Ioc 0 (2 / 2)
hm : (a * b).Monic
hnd : (a * b).natDegree = 2
⊢ ∃ c₁ c₂, (a * b).coeff 0 = c₁ * c₂ ∧ (a * b).coeff 1 = c₁ + c₂

Proof state:
case inr.mp.intro.intro.intro.intro.intro
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
a b : R[X]
ha : a.Monic
hb : b.Monic
hm : (a * b).Monic
hnd : (a * b).natDegree = 2
hdb : b.natDegree = 1
⊢ ∃ c₁ c₂, (a * b).coeff 0 = c₁ * c₂ ∧ (a * b).coeff 1 = c₁ + c₂

Tactic:
have hda := hnd

Result:
case inr.mp.intro.intro.intro.intro.intro
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
a b : R[X]
ha : a.Monic
hb : b.Monic
hm : (a * b).Monic
hnd : (a * b).natDegree = 2
hdb : b.natDegree = 1
hda : (a * b).natDegree = 2
⊢ ∃ c₁ c₂, (a * b).coeff 0 = c₁ * c₂ ∧ (a * b).coeff 1 = c₁ + c₂