case empty
R : Type u_1
S : Type ?u.25149
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ trop (inf 0) = sum (map trop 0)

case cons
R : Type u_1
S : Type ?u.25149
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : R
x : Multiset R
IH : trop (inf x) = sum (map trop x)
⊢ trop (inf (s ::ₘ x)) = sum (map trop (s ::ₘ x))
R : Type u_1
S : Type ?u.25149
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Multiset R
⊢ trop (inf s) = sum (map trop s)
induction' s using Multiset.induction with s x IH
no goals
case empty
R : Type u_1
S : Type ?u.25149
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ trop (inf 0) = sum (map trop 0)
simp
no goals
case cons
R : Type u_1
S : Type ?u.25149
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : R
x : Multiset R
IH : trop (inf x) = sum (map trop x)
⊢ trop (inf (s ::ₘ x)) = sum (map trop (s ::ₘ x))
simp [← IH]