no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort ?u.256231
ι' : Sort ?u.256234
ι₂ : Sort ?u.256237
κ : ι → Sort ?u.256242
κ₁ : ι → Sort ?u.256247
κ₂ : ι → Sort ?u.256252
κ' : ι' → Sort ?u.256257
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : Set β
⊢ image2 f s t = ⋃ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), {f i j}
simp_rw [← image_eq_iUnion, iUnion_image_left]