awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
have rw₁ : Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
    ((algebraMap A B : (a : A) → B) 0 : B) ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
rw₁ :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
      ((algebraMap A B : (a : A) → B) 0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) (((aeval ((algebraMap A B : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
have rw₂ : Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A) ↔
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
Tactic: rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp :
  Eq (α := A[X]) (((mapAlg R A : AlgHom.{u_1, u_1, u_2} R R[X] A[X]) : (a : R[X]) → A[X]) p : A[X])
    (Multiset.prod
        (Multiset.map (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) s) :
      A[X])
⊢ Eq.{u_2 + 1} (α := A) ((aeval x : (a : R[X]) → A) p : A) (0 : A)
have rw : Membership.mem (γ := Multiset A)
  (Multiset.map (α := A[X]) (⇑(aeval x) : (a : A[X]) → A)
    (Multiset.map (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) s))
  0
Tactic: rw [← aeval_map_algebraMap A, ← mapAlg_eq_map, hp, map_multiset_prod, Multiset.prod_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp :
  Eq (α := A[X]) (((mapAlg R A : AlgHom.{u_1, u_1, u_2} R R[X] A[X]) : (a : R[X]) → A[X]) p : A[X])
    (Multiset.prod
        (Multiset.map (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) s) :
      A[X])
⊢ Membership.mem (γ := Multiset A)
    (Multiset.map (α := A[X]) (⇑(aeval x) : (a : A[X]) → A)
      (Multiset.map (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) s))
    0
have rw : ∃ a ∈ s,
  Eq (α := A)
    (Function.comp (β := A[X]) (⇑(aeval x) : (a : A[X]) → A)
      (fun (x : A) ↦ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) x : A[X])) a)
    0
Tactic: rw [Multiset.map_map, Multiset.mem_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f : R[X]
⊢ WellFounded.{u_1 + 1} (α := R[X]) DvdNotUnit
have 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)
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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ 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)
have 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)
Tactic: rw [Polynomial.degree_mul, if_neg ane0]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ 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)
have pos : ∀ (hac : a * c = 0),
  Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    (⊤, (a * c).leadingCoeff)
Tactic: split_ifs with hac
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with hac
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    (⊤, (a * c).leadingCoeff)
have pos : Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
  (⊤, 0)
Tactic: rw [hac, Polynomial.leadingCoeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    (⊤, 0)
have pos : (↑a.degree : WithTop (WithBot ℕ)) < ⊤
Tactic: apply Prod.Lex.left
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (hypothesis)
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
⊢ 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)
have cne0 : c ≠ 0
Tactic: have cne0 : c ≠ 0 := right_ne_zero_of_mul hac
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ 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)
have 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)
Tactic: simp only [Polynomial.leadingCoeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ 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)
have 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)
Tactic: by_cases hdeg : c.degree = (0 : ℕ)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hdeg : c.degree = (0 : ℕ)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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 + c.degree) : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)
have 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)
Tactic: simp only [hdeg, Nat.cast_zero, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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)
have pos : a.leadingCoeff ≠ 0
Tactic: refine Prod.Lex.right _ ⟨?_, ⟨c.leadingCoeff, fun unit_c => not_unit_c ?_, rfl⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ Prod.Lex (fun (x1 x2 : WithTop (WithBot ℕ)) ↦ x1 < x2) DvdNotUnit ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff)
    ((↑a.degree : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)
have pos₁ : ∀ (unit_c : IsUnit c.leadingCoeff), IsUnit c
Tactic: refine Prod.Lex.right _ ⟨?_, ⟨c.leadingCoeff, fun unit_c => not_unit_c ?_, rfl⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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 ℕ)
⊢ a.leadingCoeff ≠ 0
have pos : ¬a.leadingCoeff = 0
Tactic: rwa [Ne, Polynomial.leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ a.leadingCoeff ≠ 0
have pos₁ : ¬a = 0
Tactic: rwa [Ne, Polynomial.leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ IsUnit c
have 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])
Tactic: rw [Polynomial.isUnit_iff, Polynomial.eq_C_of_degree_eq_zero hdeg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ ∃ (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])
have right : Eq (α := R[X]) ((C : (a : R) → R[X]) c.leadingCoeff : R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X])
Tactic: use c.leadingCoeff, unit_c
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) c.leadingCoeff : R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X])
have 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])
Tactic: rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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])
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) c.leadingCoeff : R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X])
have right₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X]) ((C : (a : R) → R[X]) (c.coeff 0) : R[X])
Tactic: rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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 + c.degree) : WithTop (WithBot ℕ)), a.leadingCoeff * c.leadingCoeff)
have neg : (↑a.degree : WithTop (WithBot ℕ)) < (↑(a.degree + c.degree) : WithTop (WithBot ℕ))
Tactic: apply Prod.Lex.left
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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 ℕ)
⊢ (↑a.degree : WithTop (WithBot ℕ)) < (↑(a.degree + c.degree) : WithTop (WithBot ℕ))
have neg : ∀ (hdeg : ¬Eq (α := WithBot ℕ) (↑c.natDegree : WithBot ℕ) (↑0 : WithBot ℕ)),
  (↑a.degree : WithTop (WithBot ℕ)) < (↑(a.degree + (↑c.natDegree : WithBot ℕ)) : WithTop (WithBot ℕ))
Tactic: rw [Polynomial.degree_eq_natDegree cne0] at *
Cleared hypotheses: hdeg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (hypothesis)
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 ℕ)
⊢ (↑a.degree : WithTop (WithBot ℕ)) < (↑(a.degree + (↑c.natDegree : WithBot ℕ)) : WithTop (WithBot ℕ))
have hdeg₁ : ¬c.natDegree = 0
Tactic: simp only [Nat.cast_inj] at hdeg
Cleared hypotheses: hdeg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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.degree : WithTop (WithBot ℕ)) < (↑(a.degree + (↑c.natDegree : WithBot ℕ)) : WithTop (WithBot ℕ))
have neg : a.natDegree < a.natDegree + c.natDegree
Tactic: rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0, ← Nat.cast_add, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : WfDvdMonoid R
f : R[X]
⊢ WellFounded.{u_1 + 1} (α := R[X]) DvdNotUnit
have 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)
Tactic: classical
      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)
      rintro a b ⟨ane0, ⟨c, ⟨not_unit_c, rfl⟩⟩⟩
      dsimp
      rw [Polynomial.degree_mul, if_neg ane0]
      split_ifs with hac
      · rw [hac, Polynomial.leadingCoeff_zero]
        apply Prod.Lex.left
        exact WithTop.coe_lt_top _
      have cne0 : c ≠ 0 := right_ne_zero_of_mul hac
      simp only [Polynomial.leadingCoeff_mul]
      by_cases hdeg : c.degree = (0 : ℕ)
      · simp only [hdeg, Nat.cast_zero, add_zero]
        refine Prod.Lex.right _ ⟨?_, ⟨c.leadingCoeff, fun unit_c => not_unit_c ?_, rfl⟩⟩
        · rwa [Ne, Polynomial.leadingCoeff_eq_zero]
        rw [Polynomial.isUnit_iff, Polynomial.eq_C_of_degree_eq_zero hdeg]
        use c.leadingCoeff, unit_c
        rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]
      · apply Prod.Lex.left
        rw [Polynomial.degree_eq_natDegree cne0] at *
        simp only [Nat.cast_inj] at hdeg
        rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0, ← Nat.cast_add, Nat.cast_lt]
        exact lt_add_of_pos_right _ (Nat.pos_of_ne_zero hdeg)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
have p₁ : ∀ {a : R[X]} (ane0 : a ≠ 0) (c : R[X]) (not_unit_c : ¬IsUnit c),
  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)) (a * c))
Tactic: classical
      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)
      rintro a b ⟨ane0, ⟨c, ⟨not_unit_c, rfl⟩⟩⟩
      dsimp
      rw [Polynomial.degree_mul, if_neg ane0]
      split_ifs with hac
      · rw [hac, Polynomial.leadingCoeff_zero]
        apply Prod.Lex.left
        exact WithTop.coe_lt_top _
      have cne0 : c ≠ 0 := right_ne_zero_of_mul hac
      simp only [Polynomial.leadingCoeff_mul]
      by_cases hdeg : c.degree = (0 : ℕ)
      · simp only [hdeg, Nat.cast_zero, add_zero]
        refine Prod.Lex.right _ ⟨?_, ⟨c.leadingCoeff, fun unit_c => not_unit_c ?_, rfl⟩⟩
        · rwa [Ne, Polynomial.leadingCoeff_eq_zero]
        rw [Polynomial.isUnit_iff, Polynomial.eq_C_of_degree_eq_zero hdeg]
        use c.leadingCoeff, unit_c
        rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]
      · apply Prod.Lex.left
        rw [Polynomial.degree_eq_natDegree cne0] at *
        simp only [Nat.cast_inj] at hdeg
        rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0, ← Nat.cast_add, Nat.cast_lt]
        exact lt_add_of_pos_right _ (Nat.pos_of_ne_zero hdeg)