α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : DecidableEq (Associates α)
p : Associates α
hp : Irreducible p
s : Multiset { a // Irreducible a }
⊢ dite (Irreducible p) (fun hp => bcount { val := p, property := hp }) (fun hp => 0) (some s) =
    Multiset.count { val := p, property := hp } s
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : DecidableEq (Associates α)
p : Associates α
hp : Irreducible p
s : Multiset { a // Irreducible a }
⊢ count p (some s) = Multiset.count { val := p, property := hp } s
dsimp only [count]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : DecidableEq (Associates α)
p : Associates α
hp : Irreducible p
s : Multiset { a // Irreducible a }
⊢ bcount { val := p, property := hp } (some s) = Multiset.count { val := p, property := hp } s
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : DecidableEq (Associates α)
p : Associates α
hp : Irreducible p
s : Multiset { a // Irreducible a }
⊢ dite (Irreducible p) (fun hp => bcount { val := p, property := hp }) (fun hp => 0) (some s) =
    Multiset.count { val := p, property := hp } s
split_ifs
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : DecidableEq (Associates α)
p : Associates α
hp : Irreducible p
s : Multiset { a // Irreducible a }
⊢ bcount { val := p, property := hp } (some s) = Multiset.count { val := p, property := hp } s
rfl