∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι} [inst_2 : DecidableEq ι]
  (i : ι) (f : (j : ι) → i = j → M),
  (s.expect fun j => if h : i = j then f j h else 0) = if i ∈ s then (↑s.card)⁻¹ • f i ⋯ else 0