case zero
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → ↑sign (f i) = zero
⊢ ↑sign (∑ i in s, f i) = zero

case neg
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → ↑sign (f i) = neg
⊢ ↑sign (∑ i in s, f i) = neg

case pos
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → ↑sign (f i) = pos
⊢ ↑sign (∑ i in s, f i) = pos
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
t : SignType
h : ∀ (i : ι), i ∈ s → ↑sign (f i) = t
⊢ ↑sign (∑ i in s, f i) = t
cases t
case zero
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → f i = 0
⊢ ∑ i in s, f i = 0
case zero
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → ↑sign (f i) = zero
⊢ ↑sign (∑ i in s, f i) = zero
simp_rw [zero_eq_zero, sign_eq_zero_iff] at h⊢
no goals
case zero
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → f i = 0
⊢ ∑ i in s, f i = 0
exact Finset.sum_eq_zero h
case neg
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → f i < 0
⊢ ∑ i in s, f i < 0
case neg
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → ↑sign (f i) = neg
⊢ ↑sign (∑ i in s, f i) = neg
simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h⊢
no goals
case neg
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → f i < 0
⊢ ∑ i in s, f i < 0
exact Finset.sum_neg h hs
case pos
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → 0 < f i
⊢ 0 < ∑ i in s, f i
case pos
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → ↑sign (f i) = pos
⊢ ↑sign (∑ i in s, f i) = pos
simp_rw [pos_eq_one, sign_eq_one_iff] at h⊢
no goals
case pos
α : Type u_2
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_1
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → 0 < f i
⊢ 0 < ∑ i in s, f i
exact Finset.sum_pos h hs