feat(Data/Set/Lattice): iUnion + insertion (#21322)

Another distributivity lemma with iUnion and insertions, needed for #21172. 

This could maybe be `@[simp]`

Mathlib/Data/Set/Lattice.lean

@@ -1125,10 +1125,14 @@ theorem iUnion_subset_iUnion_const {s : Set α} (h : ι → ι₂) : ⋃ _ : ι,
   iSup_const_mono (α := Set α) h
 
 @[simp]
-theorem iUnion_singleton_eq_range {α β : Type*} (f : α → β) : ⋃ x : α, {f x} = range f := by
+theorem iUnion_singleton_eq_range (f : α → β) : ⋃ x : α, {f x} = range f := by
   ext x
   simp [@eq_comm _ x]
 
+theorem iUnion_insert_eq_range_union_iUnion {ι : Type*} (x : ι → β) (t : ι → Set β) :
+    ⋃ i, insert (x i) (t i) = range x ∪ ⋃ i, t i := by
+  simp_rw [← union_singleton, iUnion_union_distrib, union_comm, iUnion_singleton_eq_range]
+
 theorem iUnion_of_singleton (α : Type*) : (⋃ x, {x} : Set α) = univ := by simp [Set.ext_iff]
 
 theorem iUnion_of_singleton_coe (s : Set α) : ⋃ i : s, ({(i : α)} : Set α) = s := by simp