no goals
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → WithTop R
⊢ trop (⨅ (i : S), f i) = ∑ i : S, trop (f i)
rw [iInf, ← Set.image_univ, ← coe_univ, trop_sInf_image]