case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ inf s (untrop ∘ f) = Multiset.inf (Multiset.map untrop (Multiset.map f s.val))
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ untrop (∑ i in s, f i) = inf s (untrop ∘ f)
convert Multiset.untrop_sum (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 → Tropical R
⊢ inf s (untrop ∘ f) = Multiset.inf (Multiset.map (fun x => untrop (f x)) 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 → Tropical R
⊢ inf s (untrop ∘ f) = Multiset.inf (Multiset.map untrop (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 → Tropical R
⊢ inf s (untrop ∘ f) = Multiset.inf (Multiset.map (fun x => untrop (f x)) s.val)
rfl