ZetaAppendix.hasDerivAt_bernoulli2_primitive_of_mem_Ioo

lemma hasDerivAt_bernoulli2_primitive_of_mem_Ioo (m : ℕ) {x : ℝ}    (hx : x ∈ Set.Ioo (m : ℝ) (m + 1 : ℝ)) :    HasDerivAt      (fun y : ℝ ↦        (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ))      (((-B1 x) : ℝ) : ℂ) x := by  have hnear : ∀ᶠ y in 𝓝 x, y ∈ Set.Ioo (m : ℝ) (m + 1 : ℝ) :=    isOpen_Ioo.mem_nhds hx  have heq :      (fun y : ℝ ↦        (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ))        =ᶠ[𝓝 x]      (fun y : ℝ ↦        (((-(((y - (m : ℝ)) ^ 2 - (y - (m : ℝ)) + 1 / 6) / 2)) : ℝ) : ℂ)) := by    filter_upwards [hnear] with y hy    rw [fract_eq_sub_nat_of_mem_Ioo m hy]    ring_nf  have hbase : HasDerivAt (fun y : ℝ ↦ y - (m : ℝ)) 1 x := by    simpa using (hasDerivAt_id x).sub_const (m : ℝ)  have hreal :      HasDerivAt        (fun y : ℝ ↦ -(((y - (m : ℝ)) ^ 2 - (y - (m : ℝ)) + 1 / 6) / 2))        (-(2 * (x - (m : ℝ)) - 1) / 2) x := by    have hpoly := (((hbase.pow 2).sub hbase).add_const (1 / 6)).div_const 2 |>.neg    convert! hpoly using 1    · ring_nf  have htarget :      (((-(2 * (x - (m : ℝ)) - 1) / 2) : ℝ) : ℂ) =        (((-B1 x) : ℝ) : ℂ) := by    rw [B1_eq_sub_nat_sub_half_of_mem_Ioo m hx]    norm_num    ring_nf  exact (hreal.ofReal_comp.congr_deriv htarget).congr_of_eventuallyEq heq