α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y
have h : (normalize : α → α) = Associates.out ∘ Associates.mk := by
  ext
  rw [Function.comp_apply, Associates.out_mk]
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y)) =
    Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y)))
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y
rw [← Multiset.map_id' (normalizedFactors (x * y)), ← Multiset.map_id' (normalizedFactors x), ←
  Multiset.map_id' (normalizedFactors y), ← Multiset.map_congr rfl normalize_normalized_factor, ←
  Multiset.map_congr rfl normalize_normalized_factor, ←
  Multiset.map_congr rfl normalize_normalized_factor, ← Multiset.map_add, h, ←
  Multiset.map_map Associates.out, eq_comm, ← Multiset.map_map Associates.out]
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y) =
    Multiset.map Associates.mk (normalizedFactors (x * y))
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y)) =
    Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y)))
refine' congr rfl _
case hst
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.Rel Setoid.r (normalizedFactors x + normalizedFactors y) (normalizedFactors (x * y))
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y) =
    Multiset.map Associates.mk (normalizedFactors (x * y))
apply Multiset.map_mk_eq_map_mk_of_rel
case hst.hf
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ ∀ (x_1 : α), x_1 ∈ normalizedFactors x + normalizedFactors y → Irreducible x_1

case hst.hg
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ ∀ (x_1 : α), x_1 ∈ normalizedFactors (x * y) → Irreducible x_1

case hst.h
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.prod (normalizedFactors x + normalizedFactors y) ~ᵤ Multiset.prod (normalizedFactors (x * y))
case hst
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.Rel Setoid.r (normalizedFactors x + normalizedFactors y) (normalizedFactors (x * y))
apply factors_unique
case h
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
x✝ : α
⊢ ↑normalize x✝ = (Associates.out ∘ Associates.mk) x✝
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑normalize = Associates.out ∘ Associates.mk
ext
no goals
case h
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
x✝ : α
⊢ ↑normalize x✝ = (Associates.out ∘ Associates.mk) x✝
rw [Function.comp_apply, Associates.out_mk]
case hst.hf
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x✝ y : α
hx✝ : x✝ ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
x : α
hx : x ∈ normalizedFactors x✝ + normalizedFactors y
⊢ Irreducible x
case hst.hf
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ ∀ (x_1 : α), x_1 ∈ normalizedFactors x + normalizedFactors y → Irreducible x_1
intro x hx
no goals
case hst.hf
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x✝ y : α
hx✝ : x✝ ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
x : α
hx : x ∈ normalizedFactors x✝ + normalizedFactors y
⊢ Irreducible x
rcases Multiset.mem_add.1 hx with (hx | hx) <;> exact irreducible_of_normalized_factor x hx
no goals
case hst.hg
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ ∀ (x_1 : α), x_1 ∈ normalizedFactors (x * y) → Irreducible x_1
exact irreducible_of_normalized_factor
case hst.h
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.prod (normalizedFactors x) * Multiset.prod (normalizedFactors y) ~ᵤ Multiset.prod (normalizedFactors (x * y))
case hst.h
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.prod (normalizedFactors x + normalizedFactors y) ~ᵤ Multiset.prod (normalizedFactors (x * y))
rw [Multiset.prod_add]
no goals
case hst.h
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : ↑normalize = Associates.out ∘ Associates.mk
⊢ Multiset.prod (normalizedFactors x) * Multiset.prod (normalizedFactors y) ~ᵤ Multiset.prod (normalizedFactors (x * y))
exact
  ((normalizedFactors_prod hx).mul_mul (normalizedFactors_prod hy)).trans
    (normalizedFactors_prod (mul_ne_zero hx hy)).symm