case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → Tropical (WithTop R)
⊢ untrop (∑ i in ∅, f i) = sInf (untrop ∘ f '' ↑∅)

case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : Finset.Nonempty s
⊢ untrop (∑ i in s, f i) = sInf (untrop ∘ f '' ↑s)
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) = sInf (untrop ∘ f '' ↑s)
rcases s.eq_empty_or_nonempty with (rfl | h)
no goals
case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → Tropical (WithTop R)
⊢ untrop (∑ i in ∅, f i) = sInf (untrop ∘ f '' ↑∅)
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, untrop_zero]
no goals
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : Finset.Nonempty s
⊢ untrop (∑ i in s, f i) = sInf (untrop ∘ f '' ↑s)
rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']