case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : f x ≤ 0
⊢ 0 ≤ -1 * f x

case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : ¬f x ≤ 0
⊢ 0 ≤ 1 * f x
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
⊢ 0 ≤ (if f x ≤ 0 then -1 else 1) * f x
split_ifs with hx
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : 0 < f x
⊢ 0 ≤ f x
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : ¬f x ≤ 0
⊢ 0 ≤ 1 * f x
simp at hx ⊢
no goals
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : 0 < f x
⊢ 0 ≤ f x
exact le_of_lt hx
no goals
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : f x ≤ 0
⊢ 0 ≤ -1 * f x
simp [hx]
no goals
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
⊢ ∏ x in s, (if f x ≤ 0 then -1 else 1) * f x = ∏ x in s, f x
rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one,
  Finset.prod_const, neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]