no goals
ι : Type u_1
ι' : Type ?u.10187
α : ι → Type u_2
β : ι → Type ?u.10197
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a✝ : α i
a : (i : ι) → α i
⊢ (Set.Sigma s fun i => insert (a i) (t i)) = (fun i => { fst := i, snd := a i }) '' s ∪ Set.Sigma s t
simp_rw [insert_eq, sigma_union, sigma_singleton]