no goals
α : Type u_1
β : Type ?u.7626
γ : Type ?u.7629
a a' : α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
h : MeasurableSingletonClass α
⊢ Measure.toPmf (Measure.dirac a) = pure a
rw [toPmf_eq_iff_toMeasure_eq, toMeasure_pure]