awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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))
p₂ :
  ∀ {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)
⊢ 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 (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: 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)
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))
p₂ :
  ∀ {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)
p₃ :
  ∀ {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)
⊢ WellFounded.{u_1 + 1} (α := R[X]) DvdNotUnit
have pos : ∀ {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)
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]
inst_3 : Nontrivial R
hf : 0 < f.natDegree
⊢ 0 < f.degree
have contrapose! : ∀ (hf : f.degree ≤ 0), f.natDegree ≤ 0
Tactic: contrapose! hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (hypothesis)
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
⊢ Fintype G
have hy : y ≠ 0
Tactic: have hy : y ≠ 0 := Associates.mk_ne_zero.mpr hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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])) ⋯
⊢ Fintype G
have refine : ∀ (x y : G) (heq : i x = i y), x = y
Tactic: refine Fintype.ofInjective i fun x y heq ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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
⊢ x = y
have rw : ∀ (heq : Eq (α := Associates D[X]) (Associates.mk (↑x : D[X])) (Associates.mk (↑y : D[X]))), (↑x : D[X]) = (↑y : D[X])
Tactic: rw [Subtype.mk.injEq] at heq ⊢
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
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 + 1)) D)
have succ : UniqueFactorizationMonoid.{u} (MvPolynomial (Fin d) D)[X]
Tactic: apply (finSuccEquiv D d).toMulEquiv.symm.uniqueFactorizationMonoid
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
inst_2 : Finite σ
this : Fintype σ
⊢ UniqueFactorizationMonoid.{u} (MvPolynomial (Fin (Fintype.card σ)) D)
have induction : ∀ (x : ℕ), UniqueFactorizationMonoid.{u} (MvPolynomial (Fin x) 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
⊢ UniqueFactorizationMonoid (MvPolynomial σ D)
have rw : ∀ (a : MvPolynomial σ D), a ≠ 0 → ∃ (f : Multiset (MvPolynomial σ D)), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Tactic: rw [iff_exists_prime_factors]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
a : MvPolynomial σ D
ha : a ≠ 0
⊢ ∃ (f : Multiset (MvPolynomial σ D)), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
have obtain : ∀ (s : Finset σ) (a' : MvPolynomial.{v, u} (↥s) D)
  (ha :
    Ne (α := MvPolynomial σ D)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
        MvPolynomial σ D)
      (0 : MvPolynomial σ D)),
  ∃ (f : Multiset (MvPolynomial σ D)),
    (∀ b ∈ f, Prime b) ∧
      Associated f.prod
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a')
Tactic: obtain ⟨s, a', rfl⟩ := exists_finset_rename a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial.{v, u} (↥s) D
ha :
  Ne (α := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
    (0 : MvPolynomial σ D)
⊢ ∃ (f : Multiset (MvPolynomial σ D)),
    (∀ b ∈ f, Prime b) ∧
      Associated f.prod
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a')
have obtain : ∀ (w : Multiset (MvPolynomial.{v, u} (↥s) D)) (h : ∀ b ∈ w, Prime b) (u : (MvPolynomial.{v, u} (↥s) D)ˣ)
  (hw : w.prod * (↑u : MvPolynomial (↥s) D) = a'),
  ∃ (f : Multiset (MvPolynomial σ D)),
    (∀ b ∈ f, Prime b) ∧
      Associated f.prod
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a')
Tactic: obtain ⟨w, h, u, hw⟩ :=
    iff_exists_prime_factors.1 (uniqueFactorizationMonoid_of_fintype s) a' fun h =>
      ha <| by simp [h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial.{v, u} (↥s) D
ha :
  Ne (α := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
    (0 : MvPolynomial σ D)
w : Multiset (MvPolynomial.{v, u} (↥s) D)
h : ∀ b ∈ w, Prime b
u : (MvPolynomial.{v, u} (↥s) D)ˣ
hw : w.prod * (↑u : MvPolynomial (↥s) D) = a'
⊢ HMul.hMul (α := MvPolynomial σ D)
      (Multiset.prod
        (Multiset.map
          (⇑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w))
      (↑((Units.map
                (↑(AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))) :
                  MvPolynomial (↥s) D →* MvPolynomial σ D) :
              (a : (MvPolynomial (↥s) D)ˣ) → (MvPolynomial σ D)ˣ)
            u) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
have rw : HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
      MvPolynomial σ D)
    ((↑((Units.map
                (↑(AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))) :
                  MvPolynomial (↥s) D →* MvPolynomial σ D) :
              (a : (MvPolynomial (↥s) D)ˣ) → (MvPolynomial σ D)ˣ)
            u) :
        MvPolynomial σ D) :
      MvPolynomial σ D) =
  (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
Tactic: rw [Multiset.prod_hom, Units.coe_map, AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe,
        AlgHom.toRingHom_toMonoidHom, MonoidHom.coe_coe, ← map_mul, hw]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial.{v, u} (↥s) D
ha :
  Ne (α := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
    (0 : MvPolynomial σ D)
w : Multiset (MvPolynomial.{v, u} (↥s) D)
h : ∀ b ∈ w, Prime b
u : (MvPolynomial.{v, u} (↥s) D)ˣ
hw : w.prod * (↑u : MvPolynomial (↥s) D) = a'
rw :
  HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
        MvPolynomial σ D)
      ((↑((Units.map
                  (↑(AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))) :
                    MvPolynomial (↥s) D →* MvPolynomial σ D) :
                (a : (MvPolynomial (↥s) D)ˣ) → (MvPolynomial σ D)ˣ)
              u) :
          MvPolynomial σ D) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
⊢ HMul.hMul (α := MvPolynomial σ D)
      (Multiset.prod
        (Multiset.map
          (⇑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w))
      (↑((Units.map
                (↑(AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))) :
                  MvPolynomial (↥s) D →* MvPolynomial σ D) :
              (a : (MvPolynomial (↥s) D)ˣ) → (MvPolynomial σ D)ˣ)
            u) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
have rw₁ : HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
      MvPolynomial σ D)
    (((↑(AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))) :
            MvPolynomial (↥s) D →* MvPolynomial σ D) :
          (a : MvPolynomial (↥s) D) → MvPolynomial σ D)
        (↑u : MvPolynomial (↥s) D) :
      MvPolynomial σ D) =
  (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
Tactic: rw [Multiset.prod_hom, Units.coe_map, AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe,
        AlgHom.toRingHom_toMonoidHom, MonoidHom.coe_coe, ← map_mul, hw]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
σ : Type v
D : Type u
inst : CommRing D
inst_1 : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial.{v, u} (↥s) D
ha :
  Ne (α := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a' :
      MvPolynomial σ D)
    (0 : MvPolynomial σ D)
w : Multiset (MvPolynomial.{v, u} (↥s) D)
h : ∀ b ∈ w, Prime b
u : (MvPolynomial.{v, u} (↥s) D)ˣ
hw : w.prod * (↑u : MvPolynomial (↥s) D) = a'
rw :
  HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
        MvPolynomial σ D)
      ((↑((Units.map
                  (↑(AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))) :
                    MvPolynomial (↥s) D →* MvPolynomial σ D) :
                (a : (MvPolynomial (↥s) D)ˣ) → (MvPolynomial σ D)ˣ)
              u) :
          MvPolynomial σ D) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
rw₁ :
  HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
        MvPolynomial σ D)
      (((↑(AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))) :
              MvPolynomial (↥s) D →* MvPolynomial σ D) :
            (a : MvPolynomial (↥s) D) → MvPolynomial σ D)
          (↑u : MvPolynomial (↥s) D) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
⊢ HMul.hMul (α := MvPolynomial σ D)
      (Multiset.prod
        (Multiset.map
          (⇑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w))
      (↑((Units.map
                (↑(AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))) :
                  MvPolynomial (↥s) D →* MvPolynomial σ D) :
              (a : (MvPolynomial (↥s) D)ˣ) → (MvPolynomial σ D)ˣ)
            u) :
        MvPolynomial σ D) =
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
have rw₂ : HMul.hMul (α := MvPolynomial σ D) (β := MvPolynomial σ D)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) w.prod :
      MvPolynomial σ D)
    (((↑(↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) : MvPolynomial (↥s) D →+* MvPolynomial σ D) :
            MvPolynomial (↥s) D →* MvPolynomial σ D) :
          (a : MvPolynomial (↥s) D) → MvPolynomial σ D)
        (↑u : MvPolynomial (↥s) D) :
      MvPolynomial σ D) =
  (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) D) → MvPolynomial σ D) a'
Tactic: rw [Multiset.prod_hom, Units.coe_map, AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe,
        AlgHom.toRingHom_toMonoidHom, MonoidHom.coe_coe, ← map_mul, hw]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
F : Type u_1
inst : Field F
f : F[X]
hu : ¬IsUnit f
⊢ ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f
have pos : ∀ (hf : f = 0), ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
F : Type u_1
inst : Field F
f : F[X]
hu : ¬IsUnit f
pos : ∀ (hf : f = 0), ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f
⊢ ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f
have neg : ∀ (hf : ¬f = 0), ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (goal)
Goal:
F : Type u_1
inst : Field F
f : F[X]
hu : ¬IsUnit f
hf : ¬f = 0
⊢ ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f
have neg : ∀ (g : F[X]) (hi : Irreducible g) (hf : g ∣ f), ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f
Tactic: obtain ⟨g, hi, hf⟩ := WfDvdMonoid.exists_irreducible_factor hu hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniqueFactorization (hypothesis)
Goal:
F : Type u_1
inst : Field F
f : F[X]
hu : ¬IsUnit f
hf_1 : ¬f = 0
g : F[X]
hi : Irreducible g
hf : g ∣ f
⊢ ∃ (g : F[X]), g.Monic ∧ Irreducible g ∧ g ∣ f
have ha : Associated g (HMul.hMul (β := F[X]) g ((C : (a : F) → F[X]) g.leadingCoeff⁻¹ : F[X]))
Tactic: have ha : Associated g (g * C g.leadingCoeff⁻¹) := associated_mul_unit_right _ _ <|
    isUnit_C.2 (leadingCoeff_ne_zero.2 hi.ne_zero).isUnit.inv
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
⊢ Eq (α := MvPolynomial (Fin n) R) (coeff (freeMonic R n) k)
    (if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0)
have simp : HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
    (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
  if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
Tactic: simp only [freeMonic, Polynomial.coeff_add, Polynomial.coeff_X_pow, Polynomial.finsetSum_coeff,
    Polynomial.coeff_C_mul, mul_ite, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
⊢ HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
      (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
have pos : ∀ (h : k < n),
  HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
      (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
Tactic: by_cases h : k < n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
pos :
  ∀ (h : k < n),
    HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
        (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
      if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
⊢ HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
      (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
have neg : ∀ (h : ¬k < n),
  HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
      (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
Tactic: by_cases h : k < n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
h : ¬k < n
x : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ x
⊢ ¬k = (↑x : ℕ)
have mk : ∀ (val : ℕ) (isLt : val < n),
  Membership.mem (γ := Finset (Fin n)) Finset.univ (⟨val, isLt⟩ : Fin n) → ¬k = (↑(⟨val, isLt⟩ : Fin n) : ℕ)
Tactic: cases x
Cleared hypotheses: x, h_1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
h : ¬k < n
⊢ HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
      (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
have neg : HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0) 0 =
  if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
Tactic: rw [Finset.sum_eq_zero fun x _ ↦ if_neg (by cases x; lia), add_zero, dif_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.UniversalFactorizationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
h : ¬k < n
neg :
  HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0) 0 =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
⊢ HAdd.hAdd (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
      (∑ x : Fin n, if k = (↑x : ℕ) then MvPolynomial.X x else 0) =
    if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0
have neg₁ : Eq.{u_1 + 1} (α := MvPolynomial (Fin n) R) (if k = n then 1 else 0)
  (if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0)
Tactic: rw [Finset.sum_eq_zero fun x _ ↦ if_neg (by cases x; lia), add_zero, dif_neg h]