Finset.biUnion over union

Stream: Is there code for X?

[Terence Tao]

For some reason I couldn't find this lemma in Mathlib.Data.Finset.Union:

lemma Finset.biUnion_union {α : Type*} {β : Type*} {s s' : Finset α} {t : α → Finset β} [DecidableEq β] [DecidableEq α]  :
(s ∪ s').biUnion t = (s.biUnion t) ∪ (s'.biUnion t) := by
  ext _
  simp only [Finset.mem_biUnion, Finset.mem_union]
  aesop

There is docs#Finset.set_biUnion_union, but that isn't the same thing because it uses Set's union operation rather than Finset.biUnion (which makes me confused as to the naming convention here).

[Yaël Dillies]

@loogle Finset.biUnion, _ ∪ _

[loogle]

:search: Finset.biUnion_insert, SimpleGraph.unreduced_edges_subset

[Yaël Dillies]

shows that it is indeed missing

[Eric Wieser]

@loogle Finset.disjiUnion, Finest.disjUnion

[loogle]

:exclamation: unknown identifier 'Finest.disjUnion'
Did you mean Finset.disjiUnion, "Finest.disjUnion"?

[Eric Wieser]

@loogle Finset.disjiUnion, Finset.disjUnion

[loogle]

:search: Finset.disjiUnion_cons

[Eric Wieser]

Also missing, it seems

[Eric Wieser]

docs#Multiset.add_bind exists at least