no goals
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x (x + y) ⊆ s
⊢ y ∈ posTangentConeAt s x
simpa only [add_sub_cancel'] using mem_posTangentConeAt_of_segment_subset h