no goals
α : Type u_1
β : Type ?u.183679
γ : Type ?u.183682
s : Multiset α
hs : s ≠ 0
a : α
ha : ¬a ∈ s
⊢ ↑(ofMultiset s hs) a = 0
simpa only [ofMultiset_apply, ENNReal.div_eq_zero_iff, Nat.cast_eq_zero, Multiset.count_eq_zero,
  ENNReal.nat_ne_top, or_false_iff] using ha