-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Ne (α := Associates α) (Associates.mk a0) 0
b0 : α
nzb : b0 ≠ 0
hb : Ne (α := Associates α) (Associates.mk b0) 0
rw :
  p.count (HAdd.hAdd (α := FactorSet α) (factors (Associates.mk a0)) (factors (Associates.mk b0))) =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
rw₁ :
  p.count
      (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
        (factors (Associates.mk b0))) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (factors (Associates.mk b0))
rw₂ :
  p.count
      (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
        (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₃ :
  p.count
      (↑(HAdd.hAdd (α := Multiset { a : Associates α // Irreducible a }) (factors' a0) (factors' b0)) :
        WithTop (Multiset { a : Associates α // Irreducible a })) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₄ :
  Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp)
      (HAdd.hAdd (α := Multiset { a : Associates α // Irreducible a }) (factors' a0) (factors' b0)) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₅ :
  Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' a0) +
      Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' b0) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₆ :
  Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' a0) +
      Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' b0) =
    Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' a0) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₇ rw₈ :
  Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' a0) +
      Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' b0) =
    Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' a0) +
      Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' b0)
⊢ p.count (HMul.hMul (α := Associates α) (Associates.mk a0) (Associates.mk b0)).factors =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))

Tactic:
rw [factors_mul, factors_mk a0 nza, factors_mk b0 nzb, ← FactorSet.coe_add, count_some hp,
    Multiset.count_add, count_some hp, count_some hp]

Premises used: Associates.factors_mul, Associates.count_some, Associates.factors_mk, Multiset.count_add, Associates.FactorSet.coe_add