@[simp]

theorem Finset.sum_indicator_one {α : Type u_1} {R : Type u_2} [Fintype α] [Semiring R] (s : Finset α) : ∑ x : α, (↑s).indicator (fun (x : α) => 1) x = ↑s.card

theorem Finset.card_eq_sum_indicator_one {α : Type u_1} [Fintype α] (s : Finset α) : s.card = ∑ x : α, (↑s).indicator (fun (x : α) => 1) x