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