## Stream: new members

### Topic: Counting cardinalities in presence of partitions

#### Antoine Chambert-Loir (Mar 08 2022 at 13:08):

The following MWE is arguably ugly, but I couldn't do better, in the presence of a docs#setoid.is_partition of a set which is known to be finite , to say that the cardinality of the ambient set is the sum of the cardinalities of its parts.
I struggled against coercions between finset (finset α) and set (set α).
Any advice or golfing is welcome !

In particular :

• Is there a better way to switch between close types, especially in the presence of finset.sum.

• On line 29, the suffices… is made to have Lean automatically insert the correct type; can one do better?

import data.setoid.partition
/-  {α : Type u_1} (c : set (set α)) :
setoid.is_partition c =
(∅ ∉ c ∧ ∀ (a : α), ∃! (b : set α) (H : b ∈ c), a ∈ b)
-/
import algebra.big_operators.order

variables {α : Type*}

open_locale big_operators classical

/-- The cardinal of ambient fintype equal the sum of cardinals of the parts of a partition (finset style)-/
lemma card_of_partition' [fintype α] {c : finset (finset α)} (hc : setoid.is_partition ({ s : set α | ∃ (t : finset α), s.to_finset = t ∧ t ∈ c } : set (set α))) :
∑ (s : finset α) in c, s.card = fintype.card α :=
begin
rw ← mul_one (fintype.card α),
rw ← finset.sum_card,
intro a,
rw finset.card_eq_one,
obtain ⟨s, hs, hs'⟩ := hc.right a,
simp only [exists_unique_iff_exists, exists_prop, and_imp, exists_eq_left', set.mem_set_of_eq] at hs hs',
have hs'2 : ∀ (z : finset α), z ∈ c → a ∈ z → z = s.to_finset,
{ intros z hz ha,
rw ← finset.coe_inj, simp,
refine  hs' z _ (finset.mem_coe.mpr ha),
-- To get the correct type automatically and perform the rewrite
suffices : ∀ {u v : finset α}, v ∈ c → u = v → u ∈ c,
{ refine this hz _,
rw [← finset.coe_inj, set.coe_to_finset], },
{ intros u v hu huv, rw huv, exact hu, },
},
use s.to_finset,
ext t,
simp only [finset.mem_filter, finset.mem_singleton],
split,
{ rintro ⟨ht,ha⟩,
exact hs'2 t ht ha, },
{ intro ht,
rw ← ht at hs, apply and.intro hs.left,
rw ht, simp only [set.mem_to_finset],  exact hs.right,}
end

/-- The cardinal of ambient fintype equal the sum of cardinals of the parts of a partition (set style)-/
lemma card_of_partition [fintype α] {c : set (set α)} (hc : setoid.is_partition c) :
∑ (s : set α) in c.to_finset, s.to_finset.card = fintype.card α :=
begin
let c' : finset (finset α) := { s : finset (α) | (s : set α) ∈ c }.to_finset,
have hcc' : c = { s : set α | ∃ (t : finset α), s.to_finset = t ∧ t ∈ c' },
{ simp only [set.mem_to_finset, set.mem_set_of_eq, exists_eq_left', set.coe_to_finset, set.set_of_mem_eq] },
rw hcc' at hc,
rw ← card_of_partition'  hc,
have hi : ∀ (a : set α) (ha : a ∈ c.to_finset), a.to_finset ∈ c',
{ intros a ha,
simp only [set.mem_to_finset, set.mem_set_of_eq, set.coe_to_finset],
simpa only [set.mem_to_finset] using ha,  },
have hj : ∀ (a : finset α) (ha : a ∈ c'), (a : set α) ∈ c.to_finset,
{ intros a ha,
simpa only [set.mem_to_finset] using ha, },
rw finset.sum_bij' _ hi _ _ hj,
{ intros a ha, simp only [set.coe_to_finset],  },
{ intros a ha,
rw [← finset.coe_inj, set.coe_to_finset], },
{ intros a ha, refl, },
end


#### Anatole Dedecker (Mar 08 2022 at 14:18):

I’m not a big user of the finite cardinals API in Lean, but when working on the Burnside formula (docs#mul_action.sum_card_fixed_by_eq_card_orbits_mul_card_group) I found it really convenient to construct an equiv in calc mode and then just deduce the corresponding cardinal result

#### Anatole Dedecker (Mar 08 2022 at 14:25):

In particular I would definitely try using docs#finset.card_sigma in this case.

#### Anatole Dedecker (Mar 08 2022 at 14:26):

About the suffices I’m not sure if I understand your problem correctly, but do you know about docs#tactic.interactive.change ?

#### Eric Wieser (Mar 08 2022 at 14:38):

If you're working with finset.card, it should be much easier to use finpartition:

import algebra.big_operators.basic
import order.partition.finpartition

open_locale big_operators

/-- The cardinal of ambient fintype equal the sum of cardinals of the parts of a partition (set style)-/
example {α : Type*} [decidable_eq α] {x : finset α} (p : finpartition x) :
∑ s in p.parts, s.card = x.card :=
begin
conv_rhs {rw ←p.sup_parts},
rw [finset.sup_eq_bUnion, finset.card_bUnion p.sup_indep.pairwise_disjoint],
refl
end


#### Antoine Chambert-Loir (Mar 08 2022 at 14:41):

… and using the ongoing PR to convert is_partition to finpartition? ;-)

#### Eric Wieser (Mar 08 2022 at 14:41):

Or maximally golfed:

example {α : Type*} [decidable_eq α] {x : finset α} (p : finpartition x) :
∑ s in p.parts, s.card = x.card :=
(finset.card_bUnion p.sup_indep.pairwise_disjoint).symm.trans $congr_arg _$
(finset.sup_eq_bUnion _ _).symm.trans p.sup_parts


#### Antoine Chambert-Loir (Mar 08 2022 at 15:44):

Shouldn't such a function belong to mathlib?

#### Johan Commelin (Mar 08 2022 at 16:11):

I think it should

#### Antoine Chambert-Loir (Mar 08 2022 at 16:29):

Actually, it exists… docs#finpartition.sum_card_parts

#### Antoine Chambert-Loir (Mar 08 2022 at 16:30):

(I even had forgotten that PR #12459 was the very reason to be able to use it.)

#### Antoine Chambert-Loir (Mar 08 2022 at 16:32):

That leaves one of my initial questions still open. Maybe, PR #12459 should not only produce a finpartitionof set αbut also produce one of finset α when possible.

#### Eric Wieser (Mar 08 2022 at 19:19):

Can you post the statement you're thinking of here?

#### Antoine Chambert-Loir (Mar 15 2022 at 02:14):

Sure. And finally, I could prove it myself., but I did not succeed using finpartition.

import data.setoid.partition
import algebra.big_operators.order

open_locale big_operators classical

section partition

variables {α : Type*}

-- TODO : remove the finiteness assumption on α and put it on s
/-- Given a partition of the ambient finite type,
the cardinal of a set is the sum of the cardinalities of its trace on the parts of the partition -/
lemma setoid.is_partition.card_set_eq_sum_parts {α : Type*} [fintype α] {s : set α} {P : set (set α)}
(hP : setoid.is_partition P) :
s.to_finset.card =
finset.sum P.to_finset (λ (t : set α), (s ∩ t).to_finset.card) :=
begin
rw ← finset.card_bUnion,
apply congr_arg,
{ rw ← finset.coe_inj, simp only [set.coe_to_finset, finset.coe_bUnion],
rw [set.bUnion_eq_Union, ← set.inter_Union, ← set.sUnion_eq_Union],
rw setoid.is_partition.sUnion_eq_univ hP,
exact (set.inter_univ s).symm },
{ intros t ht u hu htu,
simp only [set.mem_to_finset] at ht hu,
simp only [set.to_finset_disjoint_iff],
exact set.disjoint_of_subset (set.inter_subset_right s t) (set.inter_subset_right s u)
(setoid.is_partition.pairwise_disjoint hP ht hu htu) }
end

/-- The cardinality of a finite type is
the sum of the cardinalities of the parts of any partition -/
lemma setoid.is_partition.card_eq_sum_parts {α : Type*} [fintype α] {P : set (set α)}
(hP : setoid.is_partition P) :
fintype.card α =
finset.sum P.to_finset (λ (t : set α), t.to_finset.card) :=
begin
change finset.univ.card = _,
have : (finset.univ : finset α) = (set.univ : set α).to_finset :=
by rw [← finset.coe_inj, set.to_finset_univ],
rw this,
have h : ∀ (t : set α) (ht : t ∈ P.to_finset), t.to_finset.card = (set.univ ∩ t).to_finset.card,
{ intros t ht, apply congr_arg,
rw set.to_finset_inj, exact (set.univ_inter t).symm,  },
simp_rw finset.sum_congr rfl h,
let z := @setoid.is_partition.card_set_eq_sum_parts _ _ (set.univ) P hP,
simpa only [set.to_finset_univ, set.to_finset_card, fintype.card_of_finset]
using z,
end

end partition


#### Antoine Chambert-Loir (Mar 15 2022 at 08:37):

(By the way, should I PR these two lemmas to somewhere after the definition of docs#setoid.is_partition ?)

Last updated: Dec 20 2023 at 11:08 UTC