Pos of deriv neg at zeros

lemma pos_of_deriv_neg_at_zeros {g : ℝ → ℝ}    (hcont : ContinuousOn g (Set.Ioi 0))    {t₀ : ℝ} (_ht₀ : 0 < t₀)    (hpos : ∀ t, t₀ ≤ t → 0 < g t)    (hderiv : ∀ t, 0 < t → t < t₀ → g t = 0 → deriv g t < 0) :    ∀ t, 0 < t → 0 < g t := by  intro t ht  by_cases htge : t₀ ≤ t  · exact hpos t htge  by_contra hle  push Not at hle  let S := Set.Icc t t₀ ∩ g ⁻¹' Set.Iic 0  have hIcc_sub : Set.Icc t t₀ ⊆ Set.Ioi 0 := fun s hs => lt_of_lt_of_le ht hs.1  have hS_closed : IsClosed S :=    (hcont.mono hIcc_sub).preimage_isClosed_of_isClosed isClosed_Icc isClosed_Iic  have hS_bdd : BddAbove S := ⟨t₀, fun s hs => hs.1.2⟩  have hS_ne : S.Nonempty := ⟨t, ⟨⟨le_refl _, le_of_lt (not_le.mp htge)⟩, hle⟩⟩  let T := sSup S  obtain ⟨⟨hT_ge_t, h_sSup⟩, hT_le⟩ := hS_closed.csSup_mem hS_ne hS_bdd  have hT_lt : T < t₀ := by    rcases eq_or_lt_of_le h_sSup with h | h    · exact absurd (h ▸ hT_le) (not_le.mpr (hpos t₀ le_rfl))    · exact h  have hT_pos : 0 < T := lt_of_lt_of_le ht hT_ge_t  have hgT_eq : g T = 0 := by    by_contra hne    have hlt' : g T < 0 := lt_of_le_of_ne hT_le hne    have hcT : ContinuousAt g T :=      (hcont T (Set.mem_Ioi.mpr hT_pos)).continuousAt (isOpen_Ioi.mem_nhds hT_pos)    obtain ⟨ε, hε, hball_neg⟩ := show ∃ ε > 0, ball T ε ⊆ {x | g x < 0} by      simpa [← Metric.mem_nhds_iff, Filter.Eventually] using Tendsto.eventually_lt_const hlt' hcT    have hd : 0 < min ε (t₀ - T) / 2 := half_pos (lt_min hε (sub_pos.mpr hT_lt))    have : T + min ε (t₀ - T) / 2 ∈ S :=      ⟨⟨by linarith, by linarith [min_le_right ε (t₀ - T)]⟩,       Set.mem_preimage.mpr (Set.mem_Iic.mpr (le_of_lt (hball_neg (by        rw [Metric.mem_ball, Real.dist_eq]        have : T + min ε (t₀ - T) / 2 - T = min ε (t₀ - T) / 2 := by ring        rw [this, abs_of_pos hd]; linarith [min_le_left ε (t₀ - T)]))))⟩    linarith [le_csSup hS_bdd this]  obtain ⟨δ, hδ, hneg⟩ := neg_after_zero_of_deriv_neg hgT_eq (hderiv T hT_pos hT_lt hgT_eq)  have hmin_pos : 0 < min δ (t₀ - T) := lt_min hδ (sub_pos.mpr hT_lt)  have : T + min δ (t₀ - T) / 2 ∈ S :=    ⟨⟨by linarith, by linarith [min_le_right δ (t₀ - T)]⟩,     Set.mem_preimage.mpr (Set.mem_Iic.mpr (le_of_lt (hneg _ (by linarith)       (by linarith [min_le_left δ (t₀ - T)]))))⟩  linarith [le_csSup hS_bdd this]