awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
forall₄_congr fun a b ha hb => ?_

Premises used: forall₄_congr
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
neg :
  ∀ (a b : R[X]) (ha : a.Monic) (hb : b.Monic),
    a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a.natDegree = 0 ∨ b.natDegree = 0
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
refine forall₄_congr fun a b ha hb => ?_

Premises used: forall₄_congr
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
a b : R[X]
ha : a.Monic
hb : b.Monic
neg : a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a = 1 ∨ b.natDegree = 0
neg₁ neg₂ : a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a = 1 ∨ b = 1
⊢ a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a.natDegree = 0 ∨ b.natDegree = 0

Tactic:
rw [ha.natDegree_eq_zero, hb.natDegree_eq_zero]

Premises used: Polynomial.Monic.natDegree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
simp_rw :
  (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)
⊢ 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]

Premises used: Polynomial.Monic.irreducible_iff_natDegree, Nat.le_div_iff_mul_le, Finset.mem_Ioc, zero_lt_two, mul_two
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
h :
  (∀ (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)
⊢ (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'

Premises used: and_congr_right'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
h :
  (∀ (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)
h₁ :
  (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)) →
    ∀ (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 → 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
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
h₁ :
  ∀ (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)
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

Tactic:
subst he
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ (f * g).Monic

Tactic:
subst he
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
hp₁ : (f * g).Monic
⊢ ∀ (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)

Tactic:
subst he
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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
h₁ : ¬(0 < g.natDegree ∧ g.natDegree ≤ f.natDegree)
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ (f * g).natDegree)

Tactic:
rw [hf.natDegree_mul hg, add_le_add_iff_right]

Premises used: add_le_add_iff_right, Polynomial.Monic.natDegree_mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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:
fun ha => (h f g hf hg rfl).elim (ha.1.trans_le ha.2).ne' ha.1.ne'

Premises used: LT.lt.ne', And.right, And.left, LT.lt.trans_le, Or.elim, Not, rfl
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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'

Premises used: Or.elim, rfl
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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_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)

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

Premises used: Polynomial.Monic.natDegree_mul, pos_iff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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)
h₁ :
  ∀ (h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0),
    ∃ (f_1 : R[X]) (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
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
h₁ :
  ∀ (hl : f.natDegree ≤ g.natDegree),
    ∃ (f_1 : R[X]) (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
h₂ :
  ∀ (hl : g.natDegree ≤ f.natDegree),
    ∃ (f_1 : R[X]) (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_1 : R[X]) (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

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

Premises used: le_total, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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.natDegree + f.natDegree ≤ f.natDegree + g.natDegree

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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 : R[X]) (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

Tactic:
exact ⟨g, f, hg, hf, mul_comm g f, h.1, by gcongr⟩
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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
⊢ g.natDegree + g.natDegree ≤ f.natDegree + g.natDegree

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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 : R[X]) (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

Tactic:
exact ⟨f, g, hf, hg, rfl, h.2, by gcongr⟩
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
rw :
  (∀ (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
⊢ 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]

Premises used: and_iff_right, Polynomial.Monic.irreducible_iff_natDegree'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
mp :
  (∀ (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
mpr :
  (∀ (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)
⊢ (∀ (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
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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:
h f g (hg.of_mul_monic_left hp) hg (mul_comm f g) hdg

Premises used: Polynomial.Monic.of_mul_monic_left, mul_comm
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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

Premises used: Polynomial.Monic.of_mul_monic_left, mul_comm
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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:
h g hg hdg (dvd_mul_left g f)

Premises used: dvd_mul_left
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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)

Premises used: dvd_mul_left
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
inl : Subsingleton R → (¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂)
inr : Nontrivial R → (¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂)
⊢ ¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Subsingleton R
⊢ ¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
simp [natDegree_of_subsingleton] at hnd

Premises used: Polynomial.natDegree_of_subsingleton
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Nontrivial R
inr :
  (¬∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (2 / 2)) ↔
    ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
inr₁ : p ≠ 1
⊢ ¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
rw [hm.irreducible_iff_natDegree', and_iff_right, hnd]

Premises used: and_iff_right, Polynomial.Monic.irreducible_iff_natDegree'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Nontrivial R
inr :
  (∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) ↔
    ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
⊢ (¬∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (2 / 2)) ↔
    ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h : Nontrivial R
inr :
  (∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) →
    ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
inr₁ :
  (∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂) →
    ∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)
⊢ (∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) ↔
    ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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
⊢ b.natDegree = 1

Tactic:
simp only [Nat.Ioc_succ_singleton, zero_add, mem_singleton] at hdb

Premises used: Finset.mem_singleton, Nat.Ioc_succ_singleton, zero_add
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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
⊢ (a * b).natDegree = 2

Tactic:
have hda := hnd
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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
⊢ a.natDegree + 1 = 2

Tactic:
rw [ha.natDegree_mul hb, hdb] at hda

Premises used: Polynomial.Monic.natDegree_mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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.natDegree + 1 = 2
right : (a * b).coeff 1 = a.coeff 0 + b.coeff 0
⊢ ∃ (c₁ : R) (c₂ : R), (a * b).coeff 0 = c₁ * c₂ ∧ (a * b).coeff 1 = c₁ + c₂

Tactic:
use a.coeff 0, b.coeff 0, mul_coeff_zero a b

Premises used: Polynomial.coeff, Polynomial.mul_coeff_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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.natDegree + 1 = 2
⊢ (a * b).coeff 1 = a.coeff 0 + b.coeff 0

Tactic:
simpa only [nextCoeff, hnd, add_right_cancel hda, hdb] using ha.nextCoeff_mul hb

Premises used: Polynomial.Monic.nextCoeff_mul, add_right_cancel, Polynomial.nextCoeff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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 : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)

Tactic:
⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩

Premises used: Polynomial.C, Polynomial.monic_X_add_C, HAdd.hAdd, And.intro, Exists.intro, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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₂
inr :
  HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₁ : R[X]) *
      HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₂ : R[X]) =
    p
inr₁ : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₂ : R[X])).natDegree ∈ Ioc 0 (2 / 2)
⊢ ∃ (f : R[X]) (g : R[X]), f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)

Tactic:
refine
        ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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₂
inr :
  HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₁ : R[X]) *
      HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₂ : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c₁ : R[X]) ((C : (a : R) → R[X]) c₂ : R[X]) *
          HPow.hPow (α := R[X]) (β := ℕ) X 0 +
        HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c₁ : R[X]) ((C : (a : R) → R[X]) c₂ : R[X]) *
          HPow.hPow (α := R[X]) (β := ℕ) X 1 +
      1 * HPow.hPow (α := R[X]) (β := ℕ) X 2
⊢ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₁ : R[X]) *
      HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₂ : R[X]) =
    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]

Premises used: Polynomial.C_1, Finset.sum_range_one, Polynomial.C_mul, Polynomial.Monic.coeff_natDegree, Polynomial.as_sum_range_C_mul_X_pow, Polynomial.C_add, Finset.sum_range_succ
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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₂
⊢ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₁ : R[X]) *
      HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₂ : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c₁ : R[X]) ((C : (a : R) → R[X]) c₂ : R[X]) *
          HPow.hPow (α := R[X]) (β := ℕ) X 0 +
        HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c₁ : R[X]) ((C : (a : R) → R[X]) c₂ : R[X]) *
          HPow.hPow (α := R[X]) (β := ℕ) X 1 +
      1 * HPow.hPow (α := R[X]) (β := ℕ) X 2

Tactic:
ring
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : 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₂
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c₂ : R[X])).natDegree ∈ Ioc 0 (2 / 2)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
h : Nontrivial R
hm : Monic.{u} (R := R) 1
hnd : natDegree.{u} (R := R) 1 = 2
⊢ False

Tactic:
simp [natDegree_one] at hnd

Premises used: Polynomial.natDegree_one
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).natDegree = P.natDegree

Tactic:
le_antisymm natDegree_map_le (le_natDegree_of_ne_zero ?_)

Premises used: le_antisymm, Polynomial.natDegree_map_le, Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
refine : (Polynomial.map f P).coeff P.natDegree ≠ 0
⊢ (Polynomial.map f P).natDegree = P.natDegree

Tactic:
refine le_antisymm natDegree_map_le (le_natDegree_of_ne_zero ?_)

Premises used: le_antisymm, Polynomial.natDegree_map_le, Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
rw : Ne.{v + 1} (α := S) 1 0
⊢ (Polynomial.map f P).coeff P.natDegree ≠ 0

Tactic:
rw [coeff_map, Monic.coeff_natDegree hmo, map_one]

Premises used: Polynomial.coeff_map, map_one, Polynomial.Monic.coeff_natDegree
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ Ne.{v + 1} (α := S) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ Ne.{v + 1} (α := S) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).degree = P.degree

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
hp : (map f p).Monic
a : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) ((f : (a : R) → S) 1 : S)
⊢ p.Monic

Tactic:
apply hf
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : R[X]
hp : (map f p).Monic
a : (map f p).leadingCoeff = (f : (a : R) → S) 1
a₁ : Eq.{v + 1} (α := S) (1 : S) ((f : (a : R) → S) 1 : S)
a₂ a₃ : Eq.{v + 1} (α := S) 1 1
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) ((f : (a : R) → S) 1 : S)

Tactic:
rw [← leadingCoeff_map_of_injective hf, hp.leadingCoeff, f.map_one]

Premises used: RingHom.map_one, Polynomial.leadingCoeff_map_of_injective, Polynomial.Monic.leadingCoeff