no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort ?u.249089
ι₂ : Sort ?u.249092
κ : ι → Sort u_5
κ₁ : ι → Sort ?u.249102
κ₂ : ι → Sort ?u.249107
κ' : ι' → Sort ?u.249112
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋃ (i : ι) (j : κ i), s i j) t = ⋃ (i : ι) (j : κ i), image2 f (s i j) t
simp_rw [image2_iUnion_left]