cardinality of disjoint union

Stream: Is there code for X?

[Thomas Browning]

Does this lemma exist in mathlib? (or at least a simpler proof?)

example {α : Type*} (s t : set α) (h : disjoint s t) [hs : fintype s] [ht : fintype t] :
  fintype.card ((s ∪ t) : set α) = fintype.card s + fintype.card t :=
begin
  let x := hs.elems.image (coe : s → α),
  let y := ht.elems.image (coe : t → α),
  have hx : s = ↑x,
  { ext a,
    rw [finset.mem_coe, finset.mem_image],
    split,
    { refine λ ha, ⟨⟨a, ha⟩, _, rfl⟩,
      apply hs.complete },
    { rintros ⟨a, ha, rfl⟩,
      exact a.mem } },
  have hy : t = ↑y,
  { ext a,
    rw [finset.mem_coe, finset.mem_image],
    split,
    { refine λ ha, ⟨⟨a, ha⟩, _, rfl⟩,
      apply ht.complete },
    { rintros ⟨a, ha, rfl⟩,
      exact a.mem } },
  suffices : (x ∪ y).card = x.card + y.card,
  { simp_rw [←fintype.card_coe, finset.coe_union, ←hx, ←hy] at this,
    convert this },
  apply finset.card_disjoint_union,
  rwa [finset.disjoint_iff_disjoint_coe, ←hx, ←hy],
end

[Yakov Pechersky]

Here's a related lemma I prove in my perm.support refactor:

lemma disjoint.card_support_mul (h : disjoint f g) (hf : f.support.finite) (hg : g.support.finite)
  (hfg : (f * g).support.finite) :
  hfg.to_finset.card = hf.to_finset.card + hg.to_finset.card :=
begin
  letI := hf.fintype,
  letI := hg.fintype,
  letI := hfg.fintype,
  simp_rw [finite.card_to_finset, ←to_finset_card],
  classical,
  rw ←finset.card_disjoint_union,
  { congr,
    ext,
    simp [h.support_mul] },
  { simpa using h.disjoint_support }
end

[Yakov Pechersky]

Most of the way there:

example {α : Type*} (s t : set α) (h : _root_.disjoint s t) [fintype s] [fintype t]
  [fintype (s ∪ t : set α)] :
  fintype.card ((s ∪ t) : set α) = fintype.card s + fintype.card t :=
begin
  rw [←to_finset_card, ←to_finset_card, ←to_finset_card],
  classical,
  have : _root_.disjoint s.to_finset t.to_finset := to_finset_disjoint_iff.mpr h,
  convert finset.card_disjoint_union this,
  sorry
end

[Thomas Browning]

Thanks! It seems like it might be best to phrase this in terms of set.finite

[Yakov Pechersky]

example {α : Type*} (s t : set α) (h : _root_.disjoint s t) [fintype s] [fintype t]
  [fintype (s ∪ t : set α)] :
  fintype.card ((s ∪ t) : set α) = fintype.card s + fintype.card t :=
begin
  rw [←to_finset_card, ←to_finset_card, ←to_finset_card],
  classical,
  have : _root_.disjoint s.to_finset t.to_finset := to_finset_disjoint_iff.mpr h,
  convert finset.card_disjoint_union this,
  exact to_finset_union _ _
end

[Thomas Browning]

and here's the set.finite version:

example {α : Type*} (s t : set α) (h : disjoint s t) (hs : s.finite) (ht : t.finite) :
  (set.finite.union hs ht).to_finset.card = hs.to_finset.card + ht.to_finset.card :=
begin
  rw ← finset.card_disjoint_union,
  { apply congr_arg finset.card,
    ext a,
    simp_rw [finset.mem_union, set.finite.mem_to_finset, set.mem_union] },
  { apply set.to_finset_disjoint_iff.mpr,
    exact h },
end

[Yakov Pechersky]

Depends. You can see my #7118 for how I did it in my finset to set refactor. For the cases where you don't know that the underlying type is fintype, I refactored the card lemmas to take set.finite hypotheses. In some sections, I didn't refactor the "underlying type is fintype" and just could infer that fintype s etc.

[Yakov Pechersky]

I'd just use set.finite.card_to_finset for the finite proof, and use the proof we just wrote.