theorem ENat.tsum_const {α : Type u_1} (c : ℕ∞) : ∑' (x : α), c = card α * c

theorem ENat.tsum_set_const {α : Type u_1} (s : Set α) (c : ℕ∞) : ∑' (x : ↑s), c = s.encard * c

theorem ENat.tsum_one {α : Type u_1} : ∑' (x : α), 1 = card α

theorem ENat.tsum_set_one {α : Type u_1} (s : Set α) : ∑' (x : ↑s), 1 = s.encard