Lean4
/-- Uniform distribution taking the same non-zero probability on the nonempty finset `s` -/
def uniformOfFinset (s : Finset α) (hs : s.Nonempty) : PMF α := by
classical
refine ofFinset (fun a => if a ∈ s then s.card⁻¹ else 0) s ?_ ?_
· simp only [Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul]
have : (s.card : ℝ≥0∞) ≠ 0 := by
simpa only [Ne, Nat.cast_eq_zero, Finset.card_eq_zero] using Finset.nonempty_iff_ne_empty.1 hs
exact ENNReal.mul_inv_cancel this <| ENNReal.natCast_ne_top s.card
· exact fun x hx => by simp only [hx, if_false]