FKS2.deriv_dawson

lemma deriv_dawson : ∀ x, deriv dawson x = 1 - 2 * x * dawson x := by  intro x  unfold dawson  have h_exp_cont : Continuous (fun t : ℝ ↦ exp (t ^ 2)) := by fun_prop  rw [deriv_fun_mul (by fun_prop) ((intervalIntegral.differentiable_integral_of_continuous h_exp_cont) x),    deriv_exp (by fun_prop), Continuous.deriv_integral _ h_exp_cont 0 x,    show deriv (fun y ↦ -y ^ 2) x = -2 * x by rw [deriv.fun_neg, deriv_pow_field 2]; norm_num,    ← exp_add, neg_add_cancel, exp_zero]  ring