no goals
F : Type ?u.451621
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.451633
κ : Type ?u.451636
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : γ → α
g : α → β
s : Finset γ
⊢ (⨅ (x : α) (_ : x ∈ image f s), g x) = ⨅ (y : γ) (_ : y ∈ s), g (f y)
rw [← iInf_coe, coe_image, iInf_image, iInf_coe]