α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Multiset.prod
      (Multiset.map (↑normalize) (Classical.choose (_ : ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a))) ~ᵤ
    a
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Multiset.prod (normalizedFactors a) ~ᵤ a
rw [normalizedFactors, factors, dif_neg ane0]
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Multiset.prod
      (Multiset.map (↑normalize) (Classical.choose (_ : ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a))) ~ᵤ
    Multiset.prod (Classical.choose (_ : ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a))
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Multiset.prod
      (Multiset.map (↑normalize) (Classical.choose (_ : ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a))) ~ᵤ
    a
refine' Associated.trans _ (Classical.choose_spec (exists_prime_factors a ane0)).2
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Multiset.prod
      (Multiset.map (Associates.mk ∘ ↑normalize)
        (Classical.choose (_ : ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a))) =
    Multiset.prod
      (Multiset.map Associates.mk (Classical.choose (_ : ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a)))
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Multiset.prod
      (Multiset.map (↑normalize) (Classical.choose (_ : ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a))) ~ᵤ
    Multiset.prod (Classical.choose (_ : ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a))
rw [← Associates.mk_eq_mk_iff_associated, ← Associates.prod_mk, ← Associates.prod_mk,
  Multiset.map_map]
case e_a.e_f
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Associates.mk ∘ ↑normalize = Associates.mk
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Multiset.prod
      (Multiset.map (Associates.mk ∘ ↑normalize)
        (Classical.choose (_ : ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a))) =
    Multiset.prod
      (Multiset.map Associates.mk (Classical.choose (_ : ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a)))
congr 2
case e_a.e_f.h
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
x✝ : α
⊢ (Associates.mk ∘ ↑normalize) x✝ = Associates.mk x✝
case e_a.e_f
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Associates.mk ∘ ↑normalize = Associates.mk
ext
no goals
case e_a.e_f.h
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
x✝ : α
⊢ (Associates.mk ∘ ↑normalize) x✝ = Associates.mk x✝
rw [Function.comp_apply, Associates.mk_normalize]