case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ count p (factors (a * b)) = count p (factors a) + count p (factors b)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
⊢ count p (factors (a * b)) = count p (factors a) + count p (factors b)
obtain ⟨a0, nza, ha'⟩ := exists_non_zero_rep ha
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
b0 : α
nzb : b0 ≠ 0
hb' : Associates.mk b0 = b
⊢ count p (factors (a * b)) = count p (factors a) + count p (factors b)
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ count p (factors (a * b)) = count p (factors a) + count p (factors b)
obtain ⟨b0, nzb, hb'⟩ := exists_non_zero_rep hb
no goals
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
b0 : α
nzb : b0 ≠ 0
hb' : Associates.mk b0 = b
⊢ count p (factors (a * b)) = count p (factors a) + count p (factors b)
rw [factors_mul, ← ha', ← hb', factors_mk a0 nza, factors_mk b0 nzb, ← FactorSet.coe_add, ←
  WithTop.some_eq_coe, ← WithTop.some_eq_coe, ← WithTop.some_eq_coe, count_some hp,
  Multiset.count_add, count_some hp, count_some hp]