no goals
α : Type u_1
β : Type u_2
γ : Type ?u.191070
ι : Sort u_3
ι' : Sort ?u.191076
ι₂ : Sort ?u.191079
κ : ι → Sort u_4
κ₁ : ι → Sort ?u.191089
κ₂ : ι → Sort ?u.191094
κ' : ι' → Sort ?u.191099
f : α → β
hf : Bijective f
s : (i : ι) → κ i → Set α
⊢ (f '' ⋂ (i : ι) (j : κ i), s i j) = ⋂ (i : ι) (j : κ i), f '' s i j
simp_rw [image_iInter hf]