no goals
R : Type u_1
S : Type ?u.11886
inst✝ : AddCommMonoid R
s : Multiset (Tropical R)
⊢ ∀ (a : List (Tropical R)),
    untrop (prod (Quotient.mk (List.isSetoid (Tropical R)) a)) =
      sum (map untrop (Quotient.mk (List.isSetoid (Tropical R)) a))
simpa using List.untrop_prod