-- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
theorem Finset.prod_nonneg_of_card_nonpos_even {α β : Type*} [LinearOrderedCommRing β] {f : α → β}
    [DecidablePred fun x => f x ≤ 0] {s : Finset α} (h0 : Even (s.filter fun x => f x ≤ 0).card) :
    0 ≤ ∏ x ∈ s, f x :=
  calc
    0 ≤ ∏ x ∈ s, (if f x ≤ 0 then (-1 : β) else 1) * f x :=
      Finset.prod_nonneg fun x _ => by
        split_ifs with hx
        · simp [hx]
        simp? at hx ⊢ says simp only [not_le, one_mul] at hx ⊢
        exact le_of_lt hx
    _ = _

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even #(filter (fun x => f x ≤ 0) s)
⊢ ∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x = ∏ x ∈ s, f x

Tactic:
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]

Result:
no goals

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

Tactic:
simp [hx]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even #(filter (fun x => f x ≤ 0) s)
x : α
x✝ : x ∈ s
⊢ 0 ≤ (if f x ≤ 0 then -1 else 1) * f x

Tactic:
split_ifs with hx

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

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

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even #(filter (fun x => f x ≤ 0) s)
x : α
x✝ : x ∈ s
hx : 0 < f x
⊢ 0 ≤ f x

Tactic:
exact le_of_lt hx

Result:
no goals

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

Tactic:
simp only [not_le, one_mul] at hx ⊢

Result:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even #(filter (fun x => f x ≤ 0) s)
x : α
x✝ : x ∈ s
hx : 0 < f x
⊢ 0 ≤ f x

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

Tactic:
simp? at hx ⊢ says simp only [not_le, one_mul] at hx ⊢

Result:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even #(filter (fun x => f x ≤ 0) s)
x : α
x✝ : x ∈ s
hx : 0 < f x
⊢ 0 ≤ f x