Cardinality of parts of partitions

• Setoid.IsPartition.ncard_eq_finsum on an ambient finite type, the cardinal of a set is the sum of the cardinalities of its trace on the parts of the partition

theorem Setoid.IsPartition.ncard_eq_finsum {α : Type u_1} {P : Set (Set α)} (hP : IsPartition P) (s : Set α) (hs : s.Finite := by toFinite_tac) : s.ncard = ∑ᶠ (t : ↑P), (s ∩ ↑t).ncard

Given a partition of the ambient type, the cardinal of a finite set is the finsum of the cardinalities of its traces on the parts of the partition