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

case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : Finset.Nonempty s
⊢ trop (sInf (f '' ↑s)) = ∑ i in s, trop (f i)
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
⊢ trop (sInf (f '' ↑s)) = ∑ i in s, trop (f i)
rcases s.eq_empty_or_nonempty with (rfl | h)
no goals
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : Finset.Nonempty s
⊢ trop (sInf (f '' ↑s)) = ∑ i in s, trop (f i)
rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, s.trop_inf]
no goals
case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → WithTop R
⊢ trop (sInf (f '' ↑∅)) = ∑ i in ∅, trop (f i)
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, trop_top]