no goals
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i in s, f i) = ⨅ (i : { x // x ∈ s }), untrop (f ↑i)
simpa [← _root_.untrop_sum] using sum_attach.symm