Deriv ne zero implies isolated zero

theorem deriv_ne_zero_implies_isolated_zero {f : ℝ → ℝ} {x : ℝ} {c : ℝ}    (hf : HasDerivAt f c x) (hfx : f x = 0) (hc : c ≠ 0) :    ∃ δ > 0, ∀ h, 0 < |h| → |h| < δ → f (x + h) ≠ 0 := by  rw [hasDerivAt_iff_isLittleO_nhds_zero] at hf  have hc_pos : 0 < |c| := abs_pos.mpr hc  rw [Asymptotics.isLittleO_iff] at hf  have hfilt := hf (half_pos hc_pos)  rw [Filter.eventually_iff_exists_mem] at hfilt  obtain ⟨S, hS_mem, hS⟩ := hfilt  obtain ⟨δ, hδ_pos, hδ_sub⟩ := Metric.mem_nhds_iff.mp hS_mem  refine ⟨δ, hδ_pos, fun h hh_pos hh_lt hf_eq => ?_⟩  have hh_in : h ∈ S := hδ_sub (by simp; exact hh_lt)  have h1 := hS h hh_in  simp only [hfx, sub_zero, Real.norm_eq_abs, smul_eq_mul] at h1  rw [hf_eq, zero_sub, abs_neg, abs_mul] at h1  nlinarith