α : Type ?u.479911
inst✝⁷ : CancelCommMonoidWithZero α
inst✝⁶ : DecidableEq α
inst✝⁵ : NormalizationMonoid α
inst✝⁴ : UniqueFactorizationMonoid α
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : DecidableEq M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Unique Mˣ
x : M
⊢ factors x = Multiset.map (↑normalize) (factors x)
α : Type ?u.479911
inst✝⁷ : CancelCommMonoidWithZero α
inst✝⁶ : DecidableEq α
inst✝⁵ : NormalizationMonoid α
inst✝⁴ : UniqueFactorizationMonoid α
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : DecidableEq M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Unique Mˣ
x : M
⊢ factors x = normalizedFactors x
unfold normalizedFactors
case h.e'_3.a.h.e
α : Type ?u.479911
inst✝⁷ : CancelCommMonoidWithZero α
inst✝⁶ : DecidableEq α
inst✝⁵ : NormalizationMonoid α
inst✝⁴ : UniqueFactorizationMonoid α
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : DecidableEq M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Unique Mˣ
x x✝ : M
a✝ : x✝ ∈ factors x
⊢ ↑normalize = id
α : Type ?u.479911
inst✝⁷ : CancelCommMonoidWithZero α
inst✝⁶ : DecidableEq α
inst✝⁵ : NormalizationMonoid α
inst✝⁴ : UniqueFactorizationMonoid α
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : DecidableEq M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Unique Mˣ
x : M
⊢ factors x = Multiset.map (↑normalize) (factors x)
convert (Multiset.map_id (factors x)).symm
case h.e'_3.a.h.e.h
α : Type ?u.479911
inst✝⁷ : CancelCommMonoidWithZero α
inst✝⁶ : DecidableEq α
inst✝⁵ : NormalizationMonoid α
inst✝⁴ : UniqueFactorizationMonoid α
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : DecidableEq M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Unique Mˣ
x x✝ : M
a✝ : x✝ ∈ factors x
p : M
⊢ ↑normalize p = id p
case h.e'_3.a.h.e
α : Type ?u.479911
inst✝⁷ : CancelCommMonoidWithZero α
inst✝⁶ : DecidableEq α
inst✝⁵ : NormalizationMonoid α
inst✝⁴ : UniqueFactorizationMonoid α
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : DecidableEq M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Unique Mˣ
x x✝ : M
a✝ : x✝ ∈ factors x
⊢ ↑normalize = id
ext p
no goals
case h.e'_3.a.h.e.h
α : Type ?u.479911
inst✝⁷ : CancelCommMonoidWithZero α
inst✝⁶ : DecidableEq α
inst✝⁵ : NormalizationMonoid α
inst✝⁴ : UniqueFactorizationMonoid α
M : Type u_1
inst✝³ : CancelCommMonoidWithZero M
inst✝² : DecidableEq M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Unique Mˣ
x x✝ : M
a✝ : x✝ ∈ factors x
p : M
⊢ ↑normalize p = id p
exact normalize_eq p