Neg after zero of deriv neg

lemma neg_after_zero_of_deriv_neg {g : ℝ → ℝ} {t₀ : ℝ}    (hg0 : g t₀ = 0) (hd : deriv g t₀ < 0) :    ∃ δ > 0, ∀ s, t₀ < s → s < t₀ + δ → g s < 0 := by  have hdiff : DifferentiableAt ℝ g t₀ := by    by_contra h; simp [deriv_zero_of_not_differentiableAt h] at hd  have hda : HasDerivAt g (deriv g t₀) t₀ := hdiff.hasDerivAt  rw [hasDerivAt_iff_isLittleO_nhds_zero] at hda  have hε : (0 : ℝ) < -deriv g t₀ / 2 := by linarith  have hio := hda.def hε  rw [Filter.Eventually, Metric.mem_nhds_iff] at hio  obtain ⟨δ, hδ, hball⟩ := hio  refine ⟨δ, hδ, fun s hs1 hs2 => ?_⟩  have hh_pos : 0 < s - t₀ := sub_pos.mpr hs1  have hmem : s - t₀ ∈ Metric.ball (0 : ℝ) δ := by    simpa [Metric.mem_ball, dist_zero_right, Real.norm_eq_abs,           abs_of_pos hh_pos] using sub_left_lt_of_lt_add hs2  have hest := hball hmem  simp only [Set.mem_setOf_eq, hg0, sub_zero, smul_eq_mul, norm_eq_abs, abs_of_pos hh_pos] at hest  have := (abs_le.mp hest).2  rw [show s = t₀ + (s - t₀) by ring]  linarith [div_neg_of_neg_of_pos (mul_neg_of_pos_of_neg hh_pos hd) (by norm_num : (0 : ℝ) < 2)]