feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267

)

From discussion in #21172

Mathlib/Data/Set/Lattice.lean

@@ -439,13 +439,20 @@ theorem inter_iInter [Nonempty ι] (s : Set β) (t : ι → Set β) : (s ∩ ⋂
 theorem iInter_inter [Nonempty ι] (s : Set β) (t : ι → Set β) : (⋂ i, t i) ∩ s = ⋂ i, t i ∩ s :=
   iInf_inf
 
+theorem insert_iUnion [Nonempty ι] (x : β) (t : ι → Set β) :
+    insert x (⋃ i, t i) = ⋃ i, insert x (t i) := by
+  simp_rw [← union_singleton, iUnion_union]
+
 -- classical
 theorem union_iInter (s : Set β) (t : ι → Set β) : (s ∪ ⋂ i, t i) = ⋂ i, s ∪ t i :=
   sup_iInf_eq _ _
 
 theorem iInter_union (s : ι → Set β) (t : Set β) : (⋂ i, s i) ∪ t = ⋂ i, s i ∪ t :=
   iInf_sup_eq _ _
 
+theorem insert_iInter (x : β) (t : ι → Set β) : insert x (⋂ i, t i) = ⋂ i, insert x (t i) := by
+  simp_rw [← union_singleton, iInter_union]
+
 theorem iUnion_diff (s : Set β) (t : ι → Set β) : (⋃ i, t i) \ s = ⋃ i, t i \ s :=
   iUnion_inter _ _