-- Mathlib/Algebra/Polynomial/SpecificDegree.lean
theorem Monic.irreducible_iff_roots_eq_zero_of_degree_le_three {p : R[X]} (hp : p.Monic)
    (hp2 : 2 ≤ p.natDegree) (hp3 : p.natDegree ≤ 3) : Irreducible p ↔ p.roots = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ Irreducible p ↔ p.roots = 0

Tactic:
have hp1 : p ≠ 1 := by rintro rfl; rw [natDegree_one] at hp2; cases hp2

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ Irreducible p ↔ p.roots = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ Irreducible p ↔ p.roots = 0

Tactic:
have hp0 : p ≠ 0 := hp.ne_zero

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ Irreducible p ↔ p.roots = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hp : Monic 1
hp2 : 2 ≤ 0
hp3 : natDegree 1 ≤ 3
hp0 : 1 ≠ 0
⊢ False

Tactic:
cases hp2

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p) ↔ p.roots = 0

Tactic:
simp_rw [show p.natDegree / 2 = 1 from
    (Nat.div_le_div_right hp3).antisymm
      (by apply Nat.div_le_div_right (c := 2) hp2),
  show Finset.Ioc 0 1 = {1} from rfl,
  Finset.mem_singleton, Multiset.eq_zero_iff_forall_not_mem, mem_roots hp0, ← dvd_iff_isRoot]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree = 1 → ¬q ∣ p) ↔ ∀ (a : R), ¬X - C a ∣ p

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬X - C a ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬X - C (-q.coeff 0) ∣ p

Tactic:
apply h

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ 3 / 2 ≤ p.natDegree / 2

Tactic:
apply Nat.div_le_div_right (c := 2) hp2

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬X - C a ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬q ∣ p

Tactic:
rw [hq.eq_X_add_C hq1, ← sub_neg_eq_add, ← C_neg]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬X - C a ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬X - C (-q.coeff 0) ∣ p

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ p ≠ 1

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hp : Monic 1
hp2 : 2 ≤ natDegree 1
hp3 : natDegree 1 ≤ 3
hp0 : 1 ≠ 0
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree = 1 → ¬q ∣ p) ↔ ∀ (a : R), ¬X - C a ∣ p

Tactic:
refine ⟨fun h r ↦ h _ (monic_X_sub_C r) (natDegree_X_sub_C r), fun h q hq hq1 ↦ ?_⟩

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬X - C a ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬q ∣ p

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ Irreducible p ↔ p.roots = 0

Tactic:
rw [hp.irreducible_iff_lt_natDegree_lt hp1]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p) ↔ p.roots = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hp : Monic 1
hp2 : 2 ≤ natDegree 1
hp3 : natDegree 1 ≤ 3
hp0 : 1 ≠ 0
⊢ False

Tactic:
rw [natDegree_one] at hp2

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hp : Monic 1
hp2 : 2 ≤ 0
hp3 : natDegree 1 ≤ 3
hp0 : 1 ≠ 0
⊢ False