case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
⊢ factors a = factors b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
⊢ factors a = factors b
obtain ⟨sa, h_sa⟩ := factors_eq_some_iff_ne_zero.mpr ha
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h_sb : factors b = some sb
⊢ factors a = factors b
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
⊢ factors a = factors b
obtain ⟨sb, h_sb⟩ := factors_eq_some_iff_ne_zero.mpr hb
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
⊢ some sa = some sb
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h_sb : factors b = some sb
⊢ factors a = factors b
rw [h_sa, h_sb] at h⊢
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
⊢ sa = sb
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
⊢ some sa = some sb
rw [Option.some_inj]
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
h_count :
  ∀ (p : Associates α) (hp : Irreducible p),
    Multiset.count { val := p, property := hp } sa = Multiset.count { val := p, property := hp } sb
⊢ sa = sb
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
⊢ sa = sb
have h_count : ∀ (p : Associates α) (hp : Irreducible p),
    sa.count ⟨p, hp⟩ = sb.count ⟨p, hp⟩ := by
  intro p hp
  rw [← count_some, ← count_some, h p hp]
case intro.intro.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
h_count :
  ∀ (p : Associates α) (hp : Irreducible p),
    Multiset.count { val := p, property := hp } sa = Multiset.count { val := p, property := hp } sb
⊢ ↑toFinsupp sa = ↑toFinsupp sb
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
h_count :
  ∀ (p : Associates α) (hp : Irreducible p),
    Multiset.count { val := p, property := hp } sa = Multiset.count { val := p, property := hp } sb
⊢ sa = sb
apply Multiset.toFinsupp.injective
case intro.intro.a.h.mk
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
h_count :
  ∀ (p : Associates α) (hp : Irreducible p),
    Multiset.count { val := p, property := hp } sa = Multiset.count { val := p, property := hp } sb
p : Associates α
hp : Irreducible p
⊢ ↑(↑toFinsupp sa) { val := p, property := hp } = ↑(↑toFinsupp sb) { val := p, property := hp }
case intro.intro.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
h_count :
  ∀ (p : Associates α) (hp : Irreducible p),
    Multiset.count { val := p, property := hp } sa = Multiset.count { val := p, property := hp } sb
⊢ ↑toFinsupp sa = ↑toFinsupp sb
ext ⟨p, hp⟩
no goals
case intro.intro.a.h.mk
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
h_count :
  ∀ (p : Associates α) (hp : Irreducible p),
    Multiset.count { val := p, property := hp } sa = Multiset.count { val := p, property := hp } sb
p : Associates α
hp : Irreducible p
⊢ ↑(↑toFinsupp sa) { val := p, property := hp } = ↑(↑toFinsupp sb) { val := p, property := hp }
rw [Multiset.toFinsupp_apply, Multiset.toFinsupp_apply, h_count p hp]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
p : Associates α
hp : Irreducible p
⊢ Multiset.count { val := p, property := hp } sa = Multiset.count { val := p, property := hp } sb
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
⊢ ∀ (p : Associates α) (hp : Irreducible p),
    Multiset.count { val := p, property := hp } sa = Multiset.count { val := p, property := hp } sb
intro p hp
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ∀ (p : Associates α), Irreducible p → count p (factors a) = count p (factors b)
sa : Multiset { p // Irreducible p }
h_sa : factors a = some sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → count p (some sa) = count p (some sb)
h_sb : factors b = some sb
p : Associates α
hp : Irreducible p
⊢ Multiset.count { val := p, property := hp } sa = Multiset.count { val := p, property := hp } sb
rw [← count_some, ← count_some, h p hp]