case nil
R : Type u_1
S : Type ?u.9353
inst✝ : AddMonoid R
⊢ untrop (prod []) = sum (map untrop [])

case cons
R : Type u_1
S : Type ?u.9353
inst✝ : AddMonoid R
hd : Tropical R
tl : List (Tropical R)
IH : untrop (prod tl) = sum (map untrop tl)
⊢ untrop (prod (hd :: tl)) = sum (map untrop (hd :: tl))
R : Type u_1
S : Type ?u.9353
inst✝ : AddMonoid R
l : List (Tropical R)
⊢ untrop (prod l) = sum (map untrop l)
induction' l with hd tl IH
no goals
case nil
R : Type u_1
S : Type ?u.9353
inst✝ : AddMonoid R
⊢ untrop (prod []) = sum (map untrop [])
simp
no goals
case cons
R : Type u_1
S : Type ?u.9353
inst✝ : AddMonoid R
hd : Tropical R
tl : List (Tropical R)
IH : untrop (prod tl) = sum (map untrop tl)
⊢ untrop (prod (hd :: tl)) = sum (map untrop (hd :: tl))
simp [← IH]