no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort ?u.247553
ι₂ : Sort ?u.247556
κ : ι → Sort ?u.247561
κ₁ : ι → Sort ?u.247566
κ₂ : ι → Sort ?u.247571
κ' : ι' → Sort ?u.247576
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : ι → Set α
t : Set β
⊢ image2 f (⋃ (i : ι), s i) t = ⋃ (i : ι), image2 f (s i) t
simp only [← image_prod, iUnion_prod_const, image_iUnion]