feat(Data/Finset/Union): two easy lemmas relating union and biUnion (#34004)

The lemma names are picked to mimic biUnion_image and image_biUnion a little earlier

Author: b-mehta

Mathlib/Data/Finset/Union.lean

@@ -254,6 +254,11 @@ theorem image_biUnion_filter_eq [DecidableEq α] (s : Finset β) (g : β → α)
     ((s.image g).biUnion fun a => s.filter fun c => g c = a) = s :=
   biUnion_filter_eq_of_maps_to fun _ => mem_image_of_mem g
 
+lemma union_biUnion [DecidableEq α] : (s₁ ∪ s₂).biUnion t = s₁.biUnion t ∪ s₂.biUnion t := by
+  grind
+
+lemma biUnion_union : s.biUnion (fun x ↦ t₁ x ∪ t₂ x) = s.biUnion t₁ ∪ s.biUnion t₂ := by grind
+
 theorem biUnion_singleton {f : α → β} : (s.biUnion fun a => {f a}) = s.image f := by grind
 
 end BUnion