no goals
𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.366356
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.366451
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s✝ t : Set E
L L₁ L₂ : Filter E
s : Set E
x₀ : E
n : ℕ
h : f =O[𝓝[s] x₀] fun x => ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
⊢ HasFDerivWithinAt f 0 s x₀
simp_rw [HasFDerivWithinAt, HasFDerivAtFilter,
  h.eq_zero_of_norm_pow_within hx₀ <| zero_lt_one.trans hn, zero_apply, sub_zero,
  h.trans_isLittleO ((isLittleO_pow_sub_sub x₀ hn).mono nhdsWithin_le_nhds)]