no goals
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.6894
δ : Type ?u.6897
ι : Sort u_4
κ : ι → Sort ?u.6905
inst✝² : InfSet α
inst✝¹ : InfSet β
inst✝ : sInfHomClass F α β
f : F
g : ι → α
⊢ ↑f (⨅ (i : ι), g i) = ⨅ (i : ι), ↑f (g i)
simp [iInf, ← Set.range_comp, Function.comp]