∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E} {f' : ℝ},
  IsExtrOn f s a → HasLineDerivAt ℝ f f' a b → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → f' = 0