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