theorem expect_indicator_one {α : Type u_1} {R : Type u_2} [Fintype α] [Semiring R] [Module ℚ≥0 R] (s : Finset α) : (Finset.univ.expect fun (x : α) => (↑s).indicator (fun (x : α) => 1) x) = (↑(Fintype.card α))⁻¹ • ↑s.card