Sigma qexp deriv bound generic

lemma sigma_qexp_deriv_bound_generic (k : ℕ) :    ∀ K : Set ℂ, K ⊆ {w : ℂ | 0 < w.im} → IsCompact K →      ∃ u : ℕ+ → ℝ, Summable u ∧ ∀ (n : ℕ+) (z : K),        ‖(ArithmeticFunction.sigma k n : ℂ) * (2 * Real.pi * Complex.I * n) *          Complex.exp (2 * Real.pi * Complex.I * n * z.1)‖ ≤ u n := by  intro K hK hKc  obtain ⟨u₀, hu₀_sum, hu₀_bound⟩ := iter_deriv_comp_bound3 K hK hKc (k + 2)  refine ⟨fun n => u₀ n, hu₀_sum.subtype _, fun n z => ?_⟩  have hpow : (2 * π * n) ^ (k + 2) * ‖Complex.exp (2 * π * Complex.I * n * z.1)‖ ≤ u₀ n := by    simpa [abs_of_pos Real.pi_pos] using hu₀_bound n z  calc ‖(ArithmeticFunction.sigma k n : ℂ) * (2 * π * Complex.I * n) *          Complex.exp (2 * π * Complex.I * n * z.1)‖      = ‖(ArithmeticFunction.sigma k n : ℂ)‖ * ‖(2 * π * Complex.I * n : ℂ)‖ *          ‖Complex.exp (2 * π * Complex.I * n * z.1)‖ := by rw [norm_mul, norm_mul]    _ ≤ (n : ℝ) ^ (k + 1) * (2 * π * n) * ‖Complex.exp (2 * π * Complex.I * n * z.1)‖ := by        apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)        have hs : ‖(ArithmeticFunction.sigma k n : ℂ)‖ ≤ (n : ℝ) ^ (k + 1) := by          simpa using mod_cast ArithmeticFunction.sigma_le_pow_succ k n        have hn : ‖(2 * π * Complex.I * n : ℂ)‖ = 2 * π * n := by          simp [abs_of_pos Real.pi_pos]        rw [hn]; exact mul_le_mul hs le_rfl (by positivity) (by positivity)    _ ≤ (2 * π * n) ^ (k + 2) * ‖Complex.exp (2 * π * Complex.I * n * z.1)‖ := by        apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)        calc (n : ℝ) ^ (k + 1) * (2 * π * ↑↑n) = (2 * π) * (n : ℝ) ^ (k + 2) := by ring          _ ≤ (2 * π) ^ (k + 2) * (n : ℝ) ^ (k + 2) := by              apply mul_le_mul_of_nonneg_right _ (by positivity)              calc (2 * π) = (2 * π) ^ 1 := (pow_one _).symm                _ ≤ (2 * π) ^ (k + 2) :=                    pow_le_pow_right₀ (by linarith [Real.two_le_pi]) (by omega)          _ = (2 * π * ↑↑n) ^ (k + 2) := by ring    _ ≤ u₀ n := hpow