simp_rw [← singleton_union, biUnion_eq_iUnion, ← iUnion_union, iUnion_singleton_eq_range,
  Subtype.range_coe_subtype, setOf_mem_eq]
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
X : Set α
hX : X.Nonempty
Y : Set α
this : Nonempty ↑X
⊢ ⋃ x ∈ X, insert x Y = X ∪ Y
no goals