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

case cons
R : Type u_1
S : Type ?u.37156
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Tropical R
x : Multiset (Tropical R)
IH : untrop (sum x) = inf (map untrop x)
⊢ untrop (sum (s ::ₘ x)) = inf (map untrop (s ::ₘ x))
R : Type u_1
S : Type ?u.37156
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Multiset (Tropical R)
⊢ untrop (sum s) = inf (map untrop s)
induction' s using Multiset.induction with s x IH
no goals
case empty
R : Type u_1
S : Type ?u.37156
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ untrop (sum 0) = inf (map untrop 0)
simp
case cons
R : Type u_1
S : Type ?u.37156
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Tropical R
x : Multiset (Tropical R)
IH : untrop (sum x) = inf (map untrop x)
⊢ min (untrop s) (untrop (sum x)) = untrop s ⊓ untrop (sum x)
case cons
R : Type u_1
S : Type ?u.37156
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Tropical R
x : Multiset (Tropical R)
IH : untrop (sum x) = inf (map untrop x)
⊢ untrop (sum (s ::ₘ x)) = inf (map untrop (s ::ₘ x))
simp only [sum_cons, ge_iff_le, untrop_add, untrop_le_iff, map_cons, inf_cons, ← IH]
no goals
case cons
R : Type u_1
S : Type ?u.37156
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Tropical R
x : Multiset (Tropical R)
IH : untrop (sum x) = inf (map untrop x)
⊢ min (untrop s) (untrop (sum x)) = untrop s ⊓ untrop (sum x)
rfl