union distributes over nonempty bUnion

Stream: Is there code for X?

[Rémi Bottinelli]

Hey, I'm looking for this:

example {α β : Type*} (s : set α) (S : set β) (hS : S.nonempty) (f : β → set α) :
  s ∪ (⋃ t ∈ S, f t) = ⋃ t ∈ S, s ∪ (f t) := by library_search [hS]

What's the cleanest way to get it? Thanks!

[Eric Wieser]

lemma set.union_bUnion {α β : Type*} (s : set α) (S : set β) (hS : S.nonempty) (f : β → set α) :
  s ∪ (⋃ t ∈ S, f t) = ⋃ t ∈ S, s ∪ (f t) :=
begin
  letI := hS.coe_sort,
  simpa only [set.Union_coe_set, subtype.coe_mk] using set.union_Union s (λ x : S, f x),
end

[Rémi Bottinelli]

Thanks, I hadn't found union_Union! Would union_bUnion belong in data.set.lattice ?