hh_deriv

lemma hh_deriv (a : ℝ) {t : ℝ} (ht : t ≠ 0) : HasDerivAt (hh a) (hh' a t) t := by  have e1 : t * (1 + (a * log t) ^ 2) ≠ 0 := mul_ne_zero ht (_root_.ne_of_lt (by positivity)).symm  have l5 : HasDerivAt (fun t : ℝ => log t) t⁻¹ t := Real.hasDerivAt_log ht  have l4 : HasDerivAt (fun t : ℝ => a * log t) (a * t⁻¹) t := l5.const_mul _  have l3 : HasDerivAt (fun t : ℝ => (a * log t) ^ 2) (2 * a ^ 2 * t⁻¹ * log t) t := by    convert! l4.pow 2 using 1 ; ring  have l2 : HasDerivAt (fun t : ℝ => 1 + (a * log t) ^ 2) (2 * a ^ 2 * t⁻¹ * log t) t :=    l3.const_add _  have l1 : HasDerivAt (fun t : ℝ => t * (1 + (a * log t) ^ 2))      (1 + 2 * a ^ 2 * log t + a ^ 2 * log t ^ 2) t := by    convert! (hasDerivAt_id' t).mul l2 using 1; field_simp; ring  convert! l1.inv e1 using 1; simp only [hh', pp, hh]; field_simp; ring