awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f : R[X]
p :
  ∀ {a b : R[X]},
    DvdNotUnit a b →
      Prod.Lex.{0, u_1} (β := R) (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit
        ((fun (p : R[X]) ↦ (if p = 0 then ⊤ else (↑p.degree : WithTop (WithBot ℕ)), p.leadingCoeff)) a)
        ((fun (p : R[X]) ↦ (if p = 0 then ⊤ else (↑p.degree : WithTop (WithBot ℕ)), p.leadingCoeff)) b)
⊢ WellFounded.{u_1 + 1} (α := R[X]) DvdNotUnit

Tactic:
refine
        RelHomClass.wellFounded
          (⟨fun p : R[X] =>
              ((if p = 0 then ⊤ else ↑p.degree : WithTop (WithBot ℕ)), p.leadingCoeff), ?_⟩ :
            DvdNotUnit →r Prod.Lex (· < ·) DvdNotUnit)
          (wellFounded_lt.prod_lex ‹WfDvdMonoid R›.wf)

Premises used: RelHomClass.wellFounded, Polynomial.leadingCoeff, Prod.mk, Polynomial.degree, IsWellFounded.wf, WithTop.some, wellFounded_lt, RelHom.mk, Top.top, OfNat.ofNat, Eq, WellFounded.prod_lex, ite
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
rw :
  Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    (if a * c = 0 then ⊤ else (↑(a.degree + c.degree) : WithTop (WithBot ℕ)), (a * c).leadingCoeff)
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit
    (if a = 0 then ⊤ else (↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    (if a * c = 0 then ⊤ else (↑(a * c).degree : WithTop (WithBot ℕ)), (a * c).leadingCoeff)

Tactic:
rw [Polynomial.degree_mul, if_neg ane0]

Premises used: if_neg, Polynomial.degree_mul
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
pos :
  ∀ (hac : a * c = 0),
    Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit
      ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff) (⊤, (a * c).leadingCoeff)
neg :
  ∀ (hac : ¬a * c = 0),
    Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit
      ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
      ((↑(a.degree + c.degree) : WithTop (WithBot ℕ)), (a * c).leadingCoeff)
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    (if a * c = 0 then ⊤ else (↑(a.degree + c.degree) : WithTop (WithBot ℕ)), (a * c).leadingCoeff)

Tactic:
split_ifs with hac
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
pos :
  Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    (⊤, 0)
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    (⊤, (a * c).leadingCoeff)

Tactic:
rw [hac, Polynomial.leadingCoeff_zero]

Premises used: Polynomial.leadingCoeff_zero
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
pos : (↑a.degree : WithTop (WithBot ℕ)) < ⊤
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    (⊤, 0)

Tactic:
apply Prod.Lex.left

Premises used: Prod.Lex.left
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
⊢ (↑a.degree : WithTop (WithBot ℕ)) < ⊤

Tactic:
WithTop.coe_lt_top _

Premises used: WithTop.coe_lt_top
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
⊢ (↑a.degree : WithTop (WithBot ℕ)) < ⊤

Tactic:
exact WithTop.coe_lt_top _

Premises used: WithTop.coe_lt_top
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
⊢ c ≠ 0

Tactic:
have cne0 : c ≠ 0 := right_ne_zero_of_mul hac
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
neg :
  Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    ((↑(a.degree + c.degree) : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    ((↑(a.degree + c.degree) : WithTop (WithBot ℕ)), (a * c).leadingCoeff)

Tactic:
simp only [Polynomial.leadingCoeff_mul]

Premises used: Polynomial.leadingCoeff_mul
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
pos :
  ∀ (hdeg : c.degree = (↑0 : WithBot ℕ)),
    Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit
      ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
      ((↑(a.degree + c.degree) : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)
neg :
  ∀ (hdeg : ¬c.degree = (↑0 : WithBot ℕ)),
    Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit
      ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
      ((↑(a.degree + c.degree) : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    ((↑(a.degree + c.degree) : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)

Tactic:
by_cases hdeg : c.degree = (0 : ℕ)

Premises used: Polynomial.degree, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = (↑0 : WithBot ℕ)
pos :
  Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    ((↑(a.degree + c.degree) : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)

Tactic:
simp only [hdeg, Nat.cast_zero, add_zero]

Premises used: Nat.cast_zero, add_zero
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = (↑0 : WithBot ℕ)
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)

Tactic:
Prod.Lex.right _ ⟨?_, ⟨c.leadingCoeff, fun unit_c => not_unit_c ?_, rfl⟩⟩

Premises used: Polynomial.leadingCoeff, Prod.Lex.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = (↑0 : WithBot ℕ)
pos : a.leadingCoeff ≠ 0
pos₁ : ∀ (unit_c : IsUnit c.leadingCoeff), IsUnit c
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)

Tactic:
refine Prod.Lex.right _ ⟨?_, ⟨c.leadingCoeff, fun unit_c => not_unit_c ?_, rfl⟩⟩

Premises used: Prod.Lex.right
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = (↑0 : WithBot ℕ)
pos : ¬a.leadingCoeff = 0
pos₁ pos₂ pos₃ pos₄ : ¬a = 0
⊢ a.leadingCoeff ≠ 0

Tactic:
rwa [Ne, Polynomial.leadingCoeff_eq_zero]

Premises used: Ne, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = (↑0 : WithBot ℕ)
unit_c : IsUnit c.leadingCoeff
pos : ∃ (r : R), IsUnit r ∧ Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X])
⊢ IsUnit c

Tactic:
rw [Polynomial.isUnit_iff, Polynomial.eq_C_of_degree_eq_zero hdeg]

Premises used: Polynomial.eq_C_of_degree_eq_zero, Polynomial.isUnit_iff
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = (↑0 : WithBot ℕ)
unit_c : IsUnit c.leadingCoeff
right : Eq (α := R[X]) ((C : (a : R) → R[X]) c.leadingCoeff : R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X])
⊢ ∃ (r : R), IsUnit r ∧ Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X])

Tactic:
use c.leadingCoeff, unit_c

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = (↑0 : WithBot ℕ)
unit_c : IsUnit c.leadingCoeff
right : Eq (α := R[X]) ((C : (a : R) → R[X]) (c.coeff c.natDegree) : R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X])
right₁ right₂ : Eq (α := R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X])
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) c.leadingCoeff : R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X])

Tactic:
rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.degree = (↑0 : WithBot ℕ)
neg : (↑a.degree : WithTop (WithBot ℕ)) < (↑(a.degree + c.degree) : WithTop (WithBot ℕ))
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    ((↑(a.degree + c.degree) : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)

Tactic:
apply Prod.Lex.left

Premises used: Prod.Lex.left
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.degree = (↑0 : WithBot ℕ)
neg :
  ∀ (hdeg : ¬Eq (α := WithBot ℕ) (↑c.natDegree : WithBot ℕ) (↑0 : WithBot ℕ)),
    (↑a.degree : WithTop (WithBot ℕ)) < (↑(a.degree + (↑c.natDegree : WithBot ℕ)) : WithTop (WithBot ℕ))
⊢ (↑a.degree : WithTop (WithBot ℕ)) < (↑(a.degree + c.degree) : WithTop (WithBot ℕ))

Tactic:
rw [Polynomial.degree_eq_natDegree cne0] at *

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬Eq (α := WithBot ℕ) (↑c.natDegree : WithBot ℕ) (↑0 : WithBot ℕ)
⊢ ¬c.natDegree = 0

Tactic:
simp only [Nat.cast_inj] at hdeg

Premises used: Nat.cast_inj
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.natDegree = 0
neg : a.natDegree < a.natDegree + c.natDegree
⊢ (↑a.degree : WithTop (WithBot ℕ)) < (↑(a.degree + (↑c.natDegree : WithBot ℕ)) : WithTop (WithBot ℕ))

Tactic:
rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0, ← Nat.cast_add, Nat.cast_lt]

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_add, WithTop.coe_lt_coe, Nat.cast_lt
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.natDegree = 0
⊢ a.natDegree < a.natDegree + c.natDegree

Tactic:
lt_add_of_pos_right _ (Nat.pos_of_ne_zero hdeg)

Premises used: lt_add_of_pos_right, Nat.pos_of_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.natDegree = 0
⊢ a.natDegree < a.natDegree + c.natDegree

Tactic:
exact lt_add_of_pos_right _ (Nat.pos_of_ne_zero hdeg)

Premises used: lt_add_of_pos_right, Nat.pos_of_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f : R[X]
inst_3 : Nontrivial R
hf : 0 < f.degree
⊢ ∃ (g : R[X]), Irreducible g ∧ g ∣ f

Tactic:
WfDvdMonoid.exists_irreducible_factor (fun huf => ne_of_gt hf <| degree_eq_zero_of_isUnit huf)
    fun hf0 => not_lt_of_gt hf <| hf0.symm ▸ (@degree_zero R _).symm ▸ WithBot.bot_lt_coe _

Premises used: Eq.rec, ne_of_gt, WfDvdMonoid.exists_irreducible_factor, Polynomial.degree_zero, Polynomial.degree_eq_zero_of_isUnit, WithBot.bot_lt_coe, not_lt_of_gt, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f : R[X]
inst_3 : Nontrivial R
hf : 0 < f.natDegree
contrapose! : ∀ (hf : f.degree ≤ 0), f.natDegree ≤ 0
⊢ 0 < f.degree

Tactic:
contrapose! hf
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f : R[X]
inst_3 : Nontrivial R
hf : f.degree ≤ 0
⊢ f.natDegree ≤ 0

Tactic:
natDegree_le_of_degree_le hf

Premises used: Polynomial.natDegree_le_of_degree_le
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f : R[X]
inst_3 : Nontrivial R
hf : f.degree ≤ 0
⊢ f.natDegree ≤ 0

Tactic:
exact natDegree_le_of_degree_le hf

Premises used: Polynomial.natDegree_le_of_degree_le
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f : R[X]
inst_3 : Nontrivial R
hf : f.natDegree ≠ 0
⊢ ∃ (g : R[X]), Irreducible g ∧ g ∣ f

Tactic:
exists_irreducible_of_natDegree_pos <| Nat.pos_of_ne_zero hf

Premises used: Nat.pos_of_ne_zero, Polynomial.exists_irreducible_of_natDegree_pos
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
this : NormalizedGCDMonoid D := Classical.arbitrary (NormalizedGCDMonoid D)
⊢ UniqueFactorizationMonoid.{u} D[X]

Tactic:
ufm_of_decomposition_of_wfDvdMonoid

Premises used: ufm_of_decomposition_of_wfDvdMonoid
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
this : NormalizedGCDMonoid D := Classical.arbitrary (NormalizedGCDMonoid D)
⊢ UniqueFactorizationMonoid.{u} D[X]

Tactic:
exact ufm_of_decomposition_of_wfDvdMonoid

Premises used: ufm_of_decomposition_of_wfDvdMonoid
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
set :
  let G := { g : D[X] // g.Monic ∧ g ∣ f };
  Fintype G
⊢ Fintype { g : D[X] // g.Monic ∧ g ∣ f }

Tactic:
set G := { g : D[X] // g.Monic ∧ g ∣ f }
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g : D[X] // g.Monic ∧ g ∣ f }
y : Associates D[X] := Associates.mk f
⊢ y ≠ 0

Tactic:
have hy : y ≠ 0 := Associates.mk_ne_zero.mpr hf
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g : D[X] // g.Monic ∧ g ∣ f }
y : Associates D[X] := Associates.mk f
hy : y ≠ 0
H : Type (max 0 u) := { x : Associates D[X] // x ∣ y }
hfin : Fintype H := fintypeSubtypeDvd y hy
i : G → H := fun (x : G) ↦ Subtype.mk (p := fun (x : Associates D[X]) ↦ x ∣ y) (Associates.mk (↑x : D[X])) ⋯
refine : ∀ (x y : G) (heq : i x = i y), x = y
⊢ Fintype G

Tactic:
refine Fintype.ofInjective i fun x y heq ↦ ?_

Premises used: Fintype.ofInjective
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g : D[X] // g.Monic ∧ g ∣ f }
y_1 : Associates D[X] := Associates.mk f
hy : y_1 ≠ 0
H : Type (max 0 u) := { x : Associates D[X] // x ∣ y_1 }
hfin : Fintype H := fintypeSubtypeDvd y_1 hy
i : G → H := fun (x : G) ↦ Subtype.mk (p := fun (x : Associates D[X]) ↦ x ∣ y_1) (Associates.mk (↑x : D[X])) ⋯
x y : G
heq : i x = i y
rw :
  ∀ (heq : Eq (α := Associates D[X]) (Associates.mk (↑x : D[X])) (Associates.mk (↑y : D[X]))), (↑x : D[X]) = (↑y : D[X])
⊢ x = y

Tactic:
rw [Subtype.mk.injEq] at heq ⊢

Premises used: Subtype.mk.injEq
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g : D[X] // g.Monic ∧ g ∣ f }
y_1 : Associates D[X] := Associates.mk f
hy : y_1 ≠ 0
H : Type (max 0 u) := { x : Associates D[X] // x ∣ y_1 }
hfin : Fintype H := fintypeSubtypeDvd y_1 hy
i : G → H := fun (x : G) ↦ Subtype.mk (p := fun (x : Associates D[X]) ↦ x ∣ y_1) (Associates.mk (↑x : D[X])) ⋯
x y : G
heq : Eq (α := Associates D[X]) (Associates.mk (↑x : D[X])) (Associates.mk (↑y : D[X]))
⊢ (↑x : D[X]) = (↑y : D[X])

Tactic:
eq_of_monic_of_associated x.2.1 y.2.1 (Associates.mk_eq_mk_iff_associated.mp heq)

Premises used: Associates.mk_eq_mk_iff_associated, And.left, Iff.mp, Polynomial.eq_of_monic_of_associated, Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g : D[X] // g.Monic ∧ g ∣ f }
y_1 : Associates D[X] := Associates.mk f
hy : y_1 ≠ 0
H : Type (max 0 u) := { x : Associates D[X] // x ∣ y_1 }
hfin : Fintype H := fintypeSubtypeDvd y_1 hy
i : G → H := fun (x : G) ↦ Subtype.mk (p := fun (x : Associates D[X]) ↦ x ∣ y_1) (Associates.mk (↑x : D[X])) ⋯
x y : G
heq : Eq (α := Associates D[X]) (Associates.mk (↑x : D[X])) (Associates.mk (↑y : D[X]))
⊢ (↑x : D[X]) = (↑y : D[X])

Tactic:
exact eq_of_monic_of_associated x.2.1 y.2.1 (Associates.mk_eq_mk_iff_associated.mp heq)

Premises used: Associates.mk_eq_mk_iff_associated, And.left, Iff.mp, Polynomial.eq_of_monic_of_associated, Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
inst_2 : Finite σ
this : Fintype σ
zero : UniqueFactorizationMonoid D
⊢ UniqueFactorizationMonoid.{u} (MvPolynomial (Fin 0) D)

Tactic:
apply (isEmptyAlgEquiv D (Fin 0)).toMulEquiv.symm.uniqueFactorizationMonoid

Premises used: AlgEquiv.toMulEquiv, MvPolynomial.isEmptyAlgEquiv, MulEquiv.uniqueFactorizationMonoid, OfNat.ofNat, MulEquiv.symm, Fin
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
inst_2 : Finite σ
this : Fintype σ
⊢ UniqueFactorizationMonoid D

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
inst_2 : Finite σ
this : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid.{u} (MvPolynomial (Fin d) D)
succ : UniqueFactorizationMonoid.{u} (MvPolynomial (Fin d) D)[X]
⊢ UniqueFactorizationMonoid.{u} (MvPolynomial (Fin (d + 1)) D)

Tactic:
apply (finSuccEquiv D d).toMulEquiv.symm.uniqueFactorizationMonoid

Premises used: MvPolynomial.finSuccEquiv, AlgEquiv.toMulEquiv, MulEquiv.uniqueFactorizationMonoid, MulEquiv.symm
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
inst_2 : Finite σ
this : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid.{u} (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid.{u} (MvPolynomial (Fin d) D)[X]

Tactic:
Polynomial.uniqueFactorizationMonoid

Premises used: Polynomial.uniqueFactorizationMonoid
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
inst_2 : Finite σ
this : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid.{u} (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid.{u} (MvPolynomial (Fin d) D)[X]

Tactic:
exact Polynomial.uniqueFactorizationMonoid

Premises used: Polynomial.uniqueFactorizationMonoid
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
inst_2 : Finite σ
this : Fintype σ
induction : ∀ (x : ℕ), UniqueFactorizationMonoid.{u} (MvPolynomial (Fin x) D)
⊢ UniqueFactorizationMonoid.{u} (MvPolynomial (Fin (Fintype.card σ)) D)

Tactic:
induction Fintype.card σ with
    | zero =>
      apply (isEmptyAlgEquiv D (Fin 0)).toMulEquiv.symm.uniqueFactorizationMonoid
      infer_instance
    | succ d hd =>
      apply (finSuccEquiv D d).toMulEquiv.symm.uniqueFactorizationMonoid
      exact Polynomial.uniqueFactorizationMonoid

Premises used: Fintype.card, AlgEquiv.toMulEquiv, MvPolynomial.isEmptyAlgEquiv, Polynomial.uniqueFactorizationMonoid, MulEquiv.uniqueFactorizationMonoid, OfNat.ofNat, MulEquiv.symm, Fin
-- Module: Mathlib.RingTheory.Polynomial.UniqueFactorization
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
rw : ∀ (a : MvPolynomial σ D), a ≠ 0 → ∃ (f : Multiset (MvPolynomial σ D)), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
⊢ UniqueFactorizationMonoid (MvPolynomial σ D)

Tactic:
rw [iff_exists_prime_factors]

Premises used: UniqueFactorizationMonoid.iff_exists_prime_factors