Has Deriv At heat Kernel t

lemma hasDerivAt_heatKernel_t (hα : 0 < α) {t x : ℝ} (ht : 0 < t) :    HasDerivAt (fun τ => heatKernel α x τ)      ((-(1 / (2 * t)) * (1 / Real.sqrt (4 * Real.pi * α * t))) *         Real.exp (-(x^2) / (4 * α * t))       + (1 / Real.sqrt (4 * Real.pi * α * t)) *         ((1 / (4 * α)) * (1 / t^2) * x^2) * Real.exp (-(x^2) / (4 * α * t))) t := by  unfold heatKernel   -- Derivative of the prefactor 1/√(4παt) with respect to t  have h_coef : HasDerivAt (fun τ => 1 / Real.sqrt (4 * Real.pi * α * τ))                            (-(1 / (2 * t)) * (1 / Real.sqrt (4 * Real.pi * α * t))) t := by    have hg : HasDerivAt (fun τ ↦ 4 * Real.pi * α * τ) (4 * Real.pi * α) t := by      simpa using (hasDerivAt_id t).const_mul (4 * Real.pi * α)    have hpos : 4 * Real.pi * α * t > 0 := by positivity    have := (deriv_sqrt_inv hpos).comp t hg    convert this using 1    field_simp [ne_of_gt hpos]   -- Derivative of the exponent -(x²)/(4ατ) with respect to t  have h_inside : HasDerivAt (fun τ => -(x^2) / (4 * α * τ))                              ((1 / (4 * α)) * (1 / t^2) * x^2) t := by    have hexp1 : HasDerivAt (fun τ => τ⁻¹) (-(t^2)⁻¹) t := by      simpa using hasDerivAt_inv (ne_of_gt ht)    convert (hexp1.const_mul (-(x^2) / (4 * α))) using 1    · ext τ; field_simp    · field_simp   -- Apply chain rule through the exponential  have h_exp : HasDerivAt (fun τ => Real.exp (-(x^2) / (4 * α * τ)))                          (((1 / (4 * α)) * (1 / t^2) * x^2) *                           Real.exp (-(x^2) / (4 * α * t))) t := by    simpa [mul_comm, mul_left_comm, mul_assoc] using      (Real.hasDerivAt_exp (x := (-(x^2) / (4 * α * t)))).comp t h_inside   -- Apply product rule to combine the two parts  simpa [mul_comm, mul_left_comm, mul_assoc] using h_coef.mul h_exp