ZetaAppendix.hasDerivAt_deriv_ofReal_cpow_neg

lemma hasDerivAt_deriv_ofReal_cpow_neg (s : ℂ) {x : ℝ} (hx : 0 < x) :    HasDerivAt      (fun y : ℝ ↦ deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y)      (s * (s + 1) * (x : ℂ) ^ (-s - 2)) x := by  have hnear : ∀ᶠ y in 𝓝 x, 0 < y := Ioi_mem_nhds hx  have heq :      (fun y : ℝ ↦ deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y) =ᶠ[𝓝 x]        (fun y : ℝ ↦ -s * (y : ℂ) ^ (-s - 1)) := by    filter_upwards [hnear] with y hy    exact Complex.deriv_ofReal_cpow_neg s hy  by_cases hpow : -s - 1 = 0  · have hconst :        HasDerivAt (fun _y : ℝ ↦ -s * (1 : ℂ)) 0 x := by      simpa using (hasDerivAt_const (x := x) (c := -s * (1 : ℂ)))    have hexp :        (fun y : ℝ ↦ -s * (y : ℂ) ^ (-s - 1)) = fun _y : ℝ ↦ -s * (1 : ℂ) := by      ext y      rw [hpow, cpow_zero]    have htarget : s * (s + 1) * (x : ℂ) ^ (-s - 2) = 0 := by      have hs_add : s + 1 = 0 := by        have hneg : -(s + 1) = 0 := by          simpa [sub_eq_add_neg, neg_add, add_comm, add_left_comm, add_assoc] using hpow        exact neg_eq_zero.mp hneg      simp [hs_add]    rw [htarget]    exact hconst.congr_of_eventuallyEq (heq.trans (Filter.EventuallyEq.of_eq hexp))  · have hbase :        HasDerivAt (fun y : ℝ ↦ (y : ℂ) ^ (-s - 1))          ((-s - 1) * (x : ℂ) ^ ((-s - 1) - 1)) x :=      hasDerivAt_ofReal_cpow_const hx.ne' hpow    have hmul :        HasDerivAt (fun y : ℝ ↦ -s * (y : ℂ) ^ (-s - 1))          ((-s) * ((-s - 1) * (x : ℂ) ^ ((-s - 1) - 1))) x :=      hbase.const_mul (-s)    have htarget :        (-s) * ((-s - 1) * (x : ℂ) ^ ((-s - 1) - 1)) =          s * (s + 1) * (x : ℂ) ^ (-s - 2) := by      rw [show ((-s - 1) - 1 : ℂ) = -s - 2 by ring]      ring    exact (hmul.congr_deriv htarget).congr_of_eventuallyEq heq