case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i in s, trop (f i) = Multiset.sum (Multiset.map trop (Multiset.map f s.val))
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ trop (inf s f) = ∑ i in s, trop (f i)
convert Multiset.trop_inf (s.val.map f)
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i in s, trop (f i) = Multiset.sum (Multiset.map (fun i => trop (f i)) s.val)
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i in s, trop (f i) = Multiset.sum (Multiset.map trop (Multiset.map f s.val))
simp only [Multiset.map_map, Function.comp_apply]
no goals
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i in s, trop (f i) = Multiset.sum (Multiset.map (fun i => trop (f i)) s.val)
rfl