case nil
R : Type u_1
S : Type ?u.18757
inst✝ : LinearOrder R
⊢ trop (minimum []) = sum (map (trop ∘ WithTop.some) [])

case cons
R : Type u_1
S : Type ?u.18757
inst✝ : LinearOrder R
hd : R
tl : List R
IH : trop (minimum tl) = sum (map (trop ∘ WithTop.some) tl)
⊢ trop (minimum (hd :: tl)) = sum (map (trop ∘ WithTop.some) (hd :: tl))
R : Type u_1
S : Type ?u.18757
inst✝ : LinearOrder R
l : List R
⊢ trop (minimum l) = sum (map (trop ∘ WithTop.some) l)
induction' l with hd tl IH
no goals
case nil
R : Type u_1
S : Type ?u.18757
inst✝ : LinearOrder R
⊢ trop (minimum []) = sum (map (trop ∘ WithTop.some) [])
simp
no goals
case cons
R : Type u_1
S : Type ?u.18757
inst✝ : LinearOrder R
hd : R
tl : List R
IH : trop (minimum tl) = sum (map (trop ∘ WithTop.some) tl)
⊢ trop (minimum (hd :: tl)) = sum (map (trop ∘ WithTop.some) (hd :: tl))
simp [List.minimum_cons, ← IH]