no goals
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.8713
δ : Type ?u.8716
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : InfSet α
inst✝¹ : InfSet β
inst✝ : sInfHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ ↑f (⨅ (i : ι) (j : κ i), g i j) = ⨅ (i : ι) (j : κ i), ↑f (g i j)
simp_rw [map_iInf]