awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
q : R
hq : q ∈ normalizedFactors a
hqprime : Prime q
h1 : emultiplicity q a = (↑(Multiset.count ((normalize : (a : R) → R) q) (normalizedFactors a)) : ℕ∞)
h2 : emultiplicity q b = (↑(Multiset.count ((normalize : (a : R) → R) q) (normalizedFactors b)) : ℕ∞)
⊢ emultiplicity q a = (↑(Multiset.count q (normalizedFactors a)) : ℕ∞)

Tactic:
rw [normalize_normalized_factor q hq] at h1 h2

Premises used: UniqueFactorizationMonoid.normalize_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
q : R
hq : q ∈ normalizedFactors a
hqprime : Prime q
h1 : emultiplicity q a = (↑(Multiset.count ((normalize : (a : R) → R) q) (normalizedFactors a)) : ℕ∞)
h2 : emultiplicity q b = (↑(Multiset.count ((normalize : (a : R) → R) q) (normalizedFactors b)) : ℕ∞)
h1₁ : emultiplicity q a = (↑(Multiset.count q (normalizedFactors a)) : ℕ∞)
⊢ emultiplicity q b = (↑(Multiset.count q (normalizedFactors b)) : ℕ∞)

Tactic:
rw [normalize_normalized_factor q hq] at h1 h2

Premises used: UniqueFactorizationMonoid.normalize_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
q : R
hq : q ∈ normalizedFactors a
hqprime : Prime q
h1 : emultiplicity q a = (↑(Multiset.count q (normalizedFactors a)) : ℕ∞)
h2 : emultiplicity q b = (↑(Multiset.count q (normalizedFactors b)) : ℕ∞)
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)

Tactic:
simpa [h1, h2] using h q hqprime
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
q : R
hq : q ∉ normalizedFactors a
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)

Tactic:
simp [Multiset.count_eq_zero_of_notMem hq]

Premises used: Multiset.count_eq_zero_of_notMem
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
refine : ∀ (h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b), a ∣ b
pos : ∀ (h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b) (hb : b = 0), a ∣ b
neg neg₁ : ∀ (h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b) (hb : ¬b = 0), a ∣ b
neg₂ : ∀ (h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b) (hb : ¬b = 0), a ∣ b
neg₃ neg₄ :
  ∀ (h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b) (hb : ¬b = 0),
    let this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid;
    ∀ (q : R), Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)
pos₁ :
  ∀ (h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b) (hb : ¬b = 0),
    let this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid;
    ∀ (q : R) (hq : q ∈ normalizedFactors a),
      Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)
neg₅ neg₆ :
  ∀ (h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b) (hb : ¬b = 0),
    let this : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid;
    ∀ (q : R) (hq : q ∉ normalizedFactors a),
      Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)
⊢ a ∣ b ↔ ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b

Tactic:
classical
  refine ⟨fun h _ _ ↦ emultiplicity_le_emultiplicity_of_dvd_right h, fun h ↦ ?_⟩
  by_cases hb : b = 0
  · simp_all
  letI : NormalizationMonoid R := UniqueFactorizationMonoid.normalizationMonoid
  rw [dvd_iff_normalizedFactors_le_normalizedFactors ha hb, Multiset.le_iff_count]
  intro q
  by_cases hq : q ∈ normalizedFactors a
  · have hqprime : Prime q := prime_of_normalized_factor q hq
    have h1 := emultiplicity_eq_count_normalizedFactors hqprime.irreducible ha
    have h2 := emultiplicity_eq_count_normalizedFactors hqprime.irreducible hb
    rw [normalize_normalized_factor q hq] at h1 h2
    simpa [h1, h2] using h q hqprime
  · simp [Multiset.count_eq_zero_of_notMem hq]

Premises used: Multiset.le_iff_count
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
pos : ∀ (ha : a = 0), a ^ n ∣ b ^ n ↔ a ∣ b
neg : ∀ (ha : ¬a = 0), a ^ n ∣ b ^ n ↔ a ∣ b
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : a = 0
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

Tactic:
simp [ha, hn]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : ¬a = 0
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

Tactic:
⟨?_, fun h ↦ pow_dvd_pow_of_dvd h n⟩

Premises used: pow_dvd_pow_of_dvd, Iff.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : ¬a = 0
neg : a ^ n ∣ b ^ n → a ∣ b
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

Tactic:
refine ⟨?_, fun h ↦ pow_dvd_pow_of_dvd h n⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : ¬a = 0
neg :
  (∀ (p : R), Prime p → emultiplicity p (a ^ n) ≤ emultiplicity p (b ^ n)) →
    ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
⊢ a ^ n ∣ b ^ n → a ∣ b

Tactic:
rw [dvd_iff_emultiplicity_le (pow_ne_zero n ha), dvd_iff_emultiplicity_le ha]

Premises used: pow_ne_zero, UniqueFactorizationMonoid.dvd_iff_emultiplicity_le
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : ¬a = 0
H : ∀ (p : R), Prime p → emultiplicity p (a ^ n) ≤ emultiplicity p (b ^ n)
p : R
hp : Prime p
⊢ emultiplicity p (a ^ n) ≤ emultiplicity p (b ^ n)

Tactic:
have := H p hp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : ¬a = 0
H : ∀ (p : R), Prime p → emultiplicity p (a ^ n) ≤ emultiplicity p (b ^ n)
p : R
hp : Prime p
this : (↑n : ℕ∞) * emultiplicity p a ≤ (↑n : ℕ∞) * emultiplicity p b
⊢ Ne (α := ℕ∞) (↑n : ℕ∞) 0

Tactic:
exact_mod_cast hn
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
n : ℕ
hn : n ≠ 0
ha : ¬a = 0
H : ∀ (p : R), Prime p → emultiplicity p (a ^ n) ≤ emultiplicity p (b ^ n)
p : R
hp : Prime p
this : emultiplicity p (a ^ n) ≤ emultiplicity p (b ^ n)
neg : ∀ (this : (↑n : ℕ∞) * emultiplicity p a ≤ emultiplicity p (b ^ n)), emultiplicity p a ≤ emultiplicity p b
neg₁ : ∀ (this : (↑n : ℕ∞) * emultiplicity p a ≤ (↑n : ℕ∞) * emultiplicity p b), emultiplicity p a ≤ emultiplicity p b
neg₂ neg₃ neg₄ neg₅ : ∀ (this : emultiplicity p a ≤ emultiplicity p b), emultiplicity p a ≤ emultiplicity p b
⊢ emultiplicity p a ≤ emultiplicity p b

Tactic:
rwa [emultiplicity_pow hp, emultiplicity_pow hp,
    ENat.mul_le_mul_left_iff (by exact_mod_cast hn) (ENat.coe_ne_top _)] at this

Premises used: ENat.coe_ne_top, emultiplicity_pow, ENat.mul_le_mul_left_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
α : Type u_3
M : Type u_4
inst_2 : CommMonoid M
inst_3 : Subsingleton.{u_2 + 1} Rˣ
f : α → M
g : α → R
hgi : Function.Injective g
hg : ∀ (s : α), Irreducible (g s)
r : R
hr : r ≠ 0
simp : Function.HasFiniteMulSupport.{u_3, u_4} (M := M) fun (s : α) ↦ f s ^ Multiset.count (g s) (normalizedFactors r)
⊢ Function.HasFiniteMulSupport.{u_3, u_4} (M := M) fun (s : α) ↦ f s ^ multiplicity (g s) r

Tactic:
simp only [multiplicity_eq_count_normalizedFactors (hg _) hr, normalize_eq]

Premises used: UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors, normalize_eq
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
α : Type u_3
M : Type u_4
inst_2 : CommMonoid M
inst_3 : Subsingleton.{u_2 + 1} Rˣ
f : α → M
g : α → R
hgi : Function.Injective g
hg : ∀ (s : α), Irreducible (g s)
r : R
hr : r ≠ 0
funProp : Function.Injective.{u_3 + 1, u_2 + 1} (β := R) fun (a : α) ↦ g a
⊢ Function.HasFiniteMulSupport.{u_3, u_4} (M := M) fun (s : α) ↦ f s ^ Multiset.count (g s) (normalizedFactors r)

Tactic:
fun_prop
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
α : Type u_3
M : Type u_4
inst_2 : CommMonoid M
inst_3 : Subsingleton.{u_2 + 1} Rˣ
f : α → M
g : α → R
hgi : Function.Injective g
hg : ∀ (s : α), Irreducible (g s)
r : R
hr : r ≠ 0
simp : Function.HasFiniteMulSupport.{u_3, u_4} (M := M) fun (s : α) ↦ f s ^ Multiset.count (g s) (normalizedFactors r)
⊢ Function.HasFiniteMulSupport.{u_3, u_4} (M := M) fun (s : α) ↦ f s ^ multiplicity (g s) r

Tactic:
classical
  simp only [multiplicity_eq_count_normalizedFactors (hg _) hr, normalize_eq]
  fun_prop

Premises used: normalize_eq
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
⊢ WellFounded (α := ℕ) DvdNotUnit

Tactic:
RelHomClass.wellFounded
      (⟨fun x : ℕ => if x = 0 then (⊤ : ℕ∞) else x, ?_⟩ : DvdNotUnit →r (· < ·)) wellFounded_lt

Premises used: RelHomClass.wellFounded, Nat.cast, wellFounded_lt, RelHom.mk, Top.top, OfNat.ofNat, Eq, ite
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
refine :
  ∀ {a b : ℕ},
    DvdNotUnit a b →
      LT.lt (α := ℕ∞) ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) a)
        ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) b)
⊢ WellFounded (α := ℕ) DvdNotUnit

Tactic:
refine RelHomClass.wellFounded
      (⟨fun x : ℕ => if x = 0 then (⊤ : ℕ∞) else x, ?_⟩ : DvdNotUnit →r (· < ·)) wellFounded_lt

Premises used: RelHomClass.wellFounded, Nat.cast, wellFounded_lt, RelHom.mk, Top.top, OfNat.ofNat, Eq, ite
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
a b : ℕ
h : DvdNotUnit a b
zero :
  ∀ (h : DvdNotUnit 0 b),
    LT.lt (α := ℕ∞) ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) 0)
      ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) b)
succ :
  ∀ (a : ℕ) (h : DvdNotUnit (a + 1) b),
    LT.lt (α := ℕ∞) ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) (a + 1))
      ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) b)
⊢ LT.lt (α := ℕ∞) ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) a)
    ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) b)

Tactic:
rcases a with - | a
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
b : ℕ
h : DvdNotUnit 0 b
zero : False
⊢ LT.lt (α := ℕ∞) ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) 0)
    ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) b)

Tactic:
exfalso
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
b : ℕ
h : DvdNotUnit 0 b
zero : ∀ (h : DvdNotUnit 0 b), False
⊢ False

Tactic:
revert h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
b : ℕ
⊢ ∀ (h : DvdNotUnit 0 b), False

Tactic:
simp [DvdNotUnit]

Premises used: DvdNotUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
b a : ℕ
h : DvdNotUnit (a + 1) b
succ :
  ∀ (h : DvdNotUnit (a + 1) 0),
    LT.lt (α := ℕ∞) ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) (a + 1))
      ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) 0)
succ₁ :
  ∀ (n : ℕ) (h : DvdNotUnit (a + 1) (n + 1)),
    LT.lt (α := ℕ∞) ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) (a + 1))
      ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) (n + 1))
⊢ LT.lt (α := ℕ∞) ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) (a + 1))
    ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) b)

Tactic:
cases b
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
a : ℕ
h : DvdNotUnit (a + 1) 0
⊢ LT.lt (α := ℕ∞) ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) (a + 1))
    ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
a n : ℕ
h : DvdNotUnit (a + 1) (n + 1)
⊢ a + 1 ∣ n + 1

Tactic:
obtain ⟨h1, h2⟩ := dvd_and_not_dvd_iff.2 h

Premises used: Iff.mpr, dvd_and_not_dvd_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
a n : ℕ
h : DvdNotUnit (a + 1) (n + 1)
h1 : a + 1 ∣ n + 1
⊢ ¬n + 1 ∣ a + 1

Tactic:
obtain ⟨h1, h2⟩ := dvd_and_not_dvd_iff.2 h

Premises used: Iff.mpr, dvd_and_not_dvd_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
a n : ℕ
h : DvdNotUnit (a + 1) (n + 1)
h1 : a + 1 ∣ n + 1
h2 : ¬n + 1 ∣ a + 1
succ : a + 1 < n + 1
⊢ LT.lt (α := ℕ∞) ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) (a + 1))
    ((fun (x : ℕ) ↦ (if x = 0 then ⊤ else (↑x : ℕ∞) : ℕ∞)) (n + 1))

Tactic:
simp only [succ_ne_zero, cast_lt, if_false]

Premises used: if_false, Nat.succ_ne_zero, Nat.cast_lt
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
a n : ℕ
h : DvdNotUnit (a + 1) (n + 1)
h1 : a + 1 ∣ n + 1
h2 : ¬n + 1 ∣ a + 1
⊢ a + 1 < n + 1

Tactic:
lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h1) fun con => h2 ?_

Premises used: Nat.succ_pos, Nat.le_of_dvd, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
a n : ℕ
h : DvdNotUnit (a + 1) (n + 1)
h1 : a + 1 ∣ n + 1
h2 : ¬n + 1 ∣ a + 1
succ : ∀ (con : a + 1 = n + 1), n + 1 ∣ a + 1
⊢ a + 1 < n + 1

Tactic:
refine lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h1) fun con => h2 ?_

Premises used: Nat.succ_pos, Nat.le_of_dvd, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
a n : ℕ
h : DvdNotUnit (a + 1) (n + 1)
h1 : a + 1 ∣ n + 1
h2 : ¬n + 1 ∣ a + 1
con : a + 1 = n + 1
succ succ₁ : n + 1 ∣ n + 1
⊢ n + 1 ∣ a + 1

Tactic:
rw [con]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
⊢ normalizedFactors 0 = (↑(primeFactorsList 0) : Multiset ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
n : ℕ
rw :
  Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) (normalizedFactors (n + 1)) (↑(n + 1).primeFactorsList : Multiset ℕ)
⊢ normalizedFactors (n + 1) = (↑(n + 1).primeFactorsList : Multiset ℕ)

Tactic:
rw [← Multiset.rel_eq, ← associated_eq_eq]

Premises used: associated_eq_eq, Multiset.rel_eq
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
n : ℕ
apply : Associated (normalizedFactors (n + 1)).prod (↑(n + 1).primeFactorsList : Multiset ℕ).prod
apply₁ : ∀ x ∈ (↑(n + 1).primeFactorsList : Multiset ℕ), Irreducible x
⊢ Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) (normalizedFactors (n + 1)) (↑(n + 1).primeFactorsList : Multiset ℕ)

Tactic:
apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _

Premises used: UniqueFactorizationMonoid.factors_unique, UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
n : ℕ
rw : Associated (normalizedFactors (n + 1)).prod n.succ
⊢ Associated (normalizedFactors (n + 1)).prod (↑(n + 1).primeFactorsList : Multiset ℕ).prod

Tactic:
rw [Multiset.prod_coe, Nat.prod_primeFactorsList n.succ_ne_zero]

Premises used: Nat.succ_ne_zero, Multiset.prod_coe, Nat.prod_primeFactorsList
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod n.succ

Tactic:
prod_normalizedFactors n.succ_ne_zero

Premises used: Nat.succ_ne_zero, UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod n.succ

Tactic:
exact prod_normalizedFactors n.succ_ne_zero

Premises used: Nat.succ_ne_zero, UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
n x : ℕ
hx : x ∈ (↑(n + 1).primeFactorsList : Multiset ℕ)
⊢ Prime x

Tactic:
Nat.prime_of_mem_primeFactorsList hx

Premises used: Nat.prime_of_mem_primeFactorsList
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
n x : ℕ
hx : x ∈ (↑(n + 1).primeFactorsList : Multiset ℕ)
⊢ Prime x

Tactic:
exact Nat.prime_of_mem_primeFactorsList hx

Premises used: Nat.prime_of_mem_primeFactorsList
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
rw : Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) (normalizedFactors s.prod) s
⊢ normalizedFactors s.prod = s

Tactic:
rw [← Multiset.rel_eq, ← associated_eq_eq]

Premises used: associated_eq_eq, Multiset.rel_eq
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
apply : s.prod ≠ 0
⊢ Multiset.Rel (fun (x1 x2 : ℕ) ↦ Associated x1 x2) (normalizedFactors s.prod) s

Tactic:
apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor h
    (prod_normalizedFactors _)

Premises used: UniqueFactorizationMonoid.factors_unique, UniqueFactorizationMonoid.prod_normalizedFactors, UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
rw : 0 ∉ s
⊢ s.prod ≠ 0

Tactic:
rw [Ne, Multiset.prod_eq_zero_iff]

Premises used: Multiset.prod_eq_zero_iff, Ne
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ 0 ∉ s

Tactic:
fun con ↦ not_irreducible_zero (h 0 con)

Premises used: not_irreducible_zero, OfNat.ofNat, Not
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Goal:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ 0 ∉ s

Tactic:
exact fun con ↦ not_irreducible_zero (h 0 con)

Premises used: not_irreducible_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Subsingleton.{u_2 + 1} Mˣ
x : M
⊢ factors x = Multiset.map id (factors x)

Tactic:
(Multiset.map_id (factors x)).symm

Premises used: Multiset.map_id, UniqueFactorizationMonoid.factors, Eq.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Subsingleton.{u_2 + 1} Mˣ
x : M
h : ∀ x_1 ∈ factors x, Eq.{u_2 + 1} (α := (a : M) → M) (⇑normalize : (a : M) → M) id
⊢ factors x = Multiset.map (⇑normalize : (a : M) → M) (factors x)

Tactic:
convert! (Multiset.map_id (factors x)).symm

Premises used: Multiset.map_id, UniqueFactorizationMonoid.factors, Eq.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Subsingleton.{u_2 + 1} Mˣ
x x_1 : M
h_1 : x_1 ∈ factors x
h : ∀ (p : M), (normalize : (a : M) → M) p = id p
⊢ Eq.{u_2 + 1} (α := (a : M) → M) (⇑normalize : (a : M) → M) id

Tactic:
ext p
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Subsingleton.{u_2 + 1} Mˣ
x x_1 : M
h : x_1 ∈ factors x
p : M
⊢ (normalize : (a : M) → M) p = id p

Tactic:
normalize_eq p

Premises used: normalize_eq
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Subsingleton.{u_2 + 1} Mˣ
x x_1 : M
h : x_1 ∈ factors x
p : M
⊢ (normalize : (a : M) → M) p = id p

Tactic:
exact normalize_eq p

Premises used: normalize_eq
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
rw :
  Multiset.prod
      (Multiset.map (⇑normalize : (a : α) → α)
        (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯)) ~ᵤ
    a
⊢ (normalizedFactors a).prod ~ᵤ a

Tactic:
rw [normalizedFactors, factors, dif_neg ane0]

Premises used: UniqueFactorizationMonoid.normalizedFactors, UniqueFactorizationMonoid.factors, dif_neg
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Multiset.prod
      (Multiset.map (⇑normalize : (a : α) → α)
        (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯)) ~ᵤ
    a

Tactic:
Associated.trans ?_ (Classical.choose_spec (exists_prime_factors a ane0)).2

Premises used: UniqueFactorizationMonoid.exists_prime_factors, Associated.trans, Classical.choose_spec, And.right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
refine :
  Multiset.prod
      (Multiset.map (⇑normalize : (a : α) → α)
        (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯)) ~ᵤ
    (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).prod
⊢ Multiset.prod
      (Multiset.map (⇑normalize : (a : α) → α)
        (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯)) ~ᵤ
    a

Tactic:
refine Associated.trans ?_ (Classical.choose_spec (exists_prime_factors a ane0)).2

Premises used: UniqueFactorizationMonoid.exists_prime_factors, Associated.trans, Classical.choose_spec, And.right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
rw :
  Eq (α := Associates α)
    (Multiset.prod
      (Multiset.map (Associates.mk ∘ (⇑normalize : (a : α) → α))
        (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯)))
    (Multiset.prod
      (Multiset.map Associates.mk (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯)))
⊢ Multiset.prod
      (Multiset.map (⇑normalize : (a : α) → α)
        (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯)) ~ᵤ
    (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).prod

Tactic:
rw [← Associates.mk_eq_mk_iff_associated, ← Associates.prod_mk, ← Associates.prod_mk,
    Multiset.map_map]

Premises used: Associates.mk_eq_mk_iff_associated, Associates.prod_mk, Multiset.map_map