no goals
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ 0 ≤ ↑f' y
simpa using h.hasFDerivWithinAt_nonpos hf hy'