[GOAL]
R : Type u_1
S : Type u_2
inst✝ : AddMonoid R
l : List R
⊢ trop (sum l) = prod (map trop l)
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
R : Type u_1
S : Type u_2
inst✝ : AddMonoid R
⊢ trop (sum []) = prod (map trop [])
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u_1
S : Type u_2
inst✝ : AddMonoid R
hd : R
tl : List R
IH : trop (sum tl) = prod (map trop tl)
⊢ trop (sum (hd :: tl)) = prod (map trop (hd :: tl))
[PROOFSTEP]
simp [← IH]
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Multiset R
⊢ ∀ (a : List R), trop (sum (Quotient.mk (List.isSetoid R) a)) = prod (map trop (Quotient.mk (List.isSetoid R) a))
[PROOFSTEP]
simpa using List.trop_sum
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ trop (∑ i in s, f i) = ∏ i in s, trop (f i)
[PROOFSTEP]
convert Multiset.trop_sum (s.val.map f)
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ ∏ i in s, trop (f i) = Multiset.prod (Multiset.map trop (Multiset.map f s.val))
[PROOFSTEP]
simp only [Multiset.map_map, Function.comp_apply]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ ∏ i in s, trop (f i) = Multiset.prod (Multiset.map (fun i => trop (f i)) s.val)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : AddMonoid R
l : List (Tropical R)
⊢ untrop (prod l) = sum (map untrop l)
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
R : Type u_1
S : Type u_2
inst✝ : AddMonoid R
⊢ untrop (prod []) = sum (map untrop [])
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u_1
S : Type u_2
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))
[PROOFSTEP]
simp [← IH]
[GOAL]
R : Type u_1
S : Type u_2
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))
[PROOFSTEP]
simpa using List.untrop_prod
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ untrop (∏ i in s, f i) = ∑ i in s, untrop (f i)
[PROOFSTEP]
convert Multiset.untrop_prod (s.val.map f)
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ ∑ i in s, untrop (f i) = Multiset.sum (Multiset.map untrop (Multiset.map f s.val))
[PROOFSTEP]
simp only [Multiset.map_map, Function.comp_apply]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ ∑ i in s, untrop (f i) = Multiset.sum (Multiset.map (fun i => untrop (f i)) s.val)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : LinearOrder R
l : List R
⊢ trop (minimum l) = sum (map (trop ∘ WithTop.some) l)
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
R : Type u_1
S : Type u_2
inst✝ : LinearOrder R
⊢ trop (minimum []) = sum (map (trop ∘ WithTop.some) [])
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u_1
S : Type u_2
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))
[PROOFSTEP]
simp [List.minimum_cons, ← IH]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Multiset R
⊢ trop (inf s) = sum (map trop s)
[PROOFSTEP]
induction' s using Multiset.induction with s x IH
[GOAL]
case empty
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ trop (inf 0) = sum (map trop 0)
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u_1
S : Type u_2
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))
[PROOFSTEP]
simp [← IH]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ trop (inf s f) = ∑ i in s, trop (f i)
[PROOFSTEP]
convert Multiset.trop_inf (s.val.map f)
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i in s, trop (f i) = Multiset.sum (Multiset.map trop (Multiset.map f s.val))
[PROOFSTEP]
simp only [Multiset.map_map, Function.comp_apply]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i in s, trop (f i) = Multiset.sum (Multiset.map (fun i => trop (f i)) s.val)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
⊢ trop (sInf (f '' ↑s)) = ∑ i in s, trop (f i)
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | h)
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → WithTop R
⊢ trop (sInf (f '' ↑∅)) = ∑ i in ∅, trop (f i)
[PROOFSTEP]
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, trop_top]
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : Finset.Nonempty s
⊢ trop (sInf (f '' ↑s)) = ∑ i in s, trop (f i)
[PROOFSTEP]
rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, s.trop_inf]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → WithTop R
⊢ trop (⨅ (i : S), f i) = ∑ i : S, trop (f i)
[PROOFSTEP]
rw [iInf, ← Set.image_univ, ← coe_univ, trop_sInf_image]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Multiset (Tropical R)
⊢ untrop (sum s) = inf (map untrop s)
[PROOFSTEP]
induction' s using Multiset.induction with s x IH
[GOAL]
case empty
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
⊢ untrop (sum 0) = inf (map untrop 0)
[PROOFSTEP]
simp
[GOAL]
case cons
R : Type u_1
S : Type u_2
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))
[PROOFSTEP]
simp only [sum_cons, ge_iff_le, untrop_add, untrop_le_iff, map_cons, inf_cons, ← IH]
[GOAL]
case cons
R : Type u_1
S : Type u_2
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)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ untrop (∑ i in s, f i) = inf s (untrop ∘ f)
[PROOFSTEP]
convert Multiset.untrop_sum (s.val.map f)
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ inf s (untrop ∘ f) = Multiset.inf (Multiset.map untrop (Multiset.map f s.val))
[PROOFSTEP]
simp only [Multiset.map_map, Function.comp_apply]
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Finset S
f : S → Tropical R
⊢ inf s (untrop ∘ f) = Multiset.inf (Multiset.map (fun x => untrop (f x)) s.val)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i in s, f i) = sInf (untrop ∘ f '' ↑s)
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | h)
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → Tropical (WithTop R)
⊢ untrop (∑ i in ∅, f i) = sInf (untrop ∘ f '' ↑∅)
[PROOFSTEP]
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, untrop_zero]
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : Finset.Nonempty s
⊢ untrop (∑ i in s, f i) = sInf (untrop ∘ f '' ↑s)
[PROOFSTEP]
rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i : S, f i) = ⨅ (i : S), untrop (f i)
[PROOFSTEP]
rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ sInf ((untrop ∘ fun i => f i) '' ↑univ) = sInf ((fun i => untrop (f i)) '' ↑univ)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i in s, f i) = ⨅ (i : { x // x ∈ s }), untrop (f ↑i)
[PROOFSTEP]
simpa [← _root_.untrop_sum] using sum_attach.symm
