no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort ?u.248318
ι₂ : Sort ?u.248321
κ : ι → Sort ?u.248326
κ₁ : ι → Sort ?u.248331
κ₂ : ι → Sort ?u.248336
κ' : ι' → Sort ?u.248341
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : ι → Set β
⊢ image2 f s (⋃ (i : ι), t i) = ⋃ (i : ι), image2 f s (t i)
simp only [← image_prod, prod_iUnion, image_iUnion]