-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
lemma hasDerivAt_Gammaℂ_one : HasDerivAt Gammaℂ (-(γ + log (2 * π)) / π) 1

Proof state:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
this : HasDerivAt (fun x => (2 * ↑π) ^ (-x)) ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) 1
⊢ HasDerivAt (fun s => 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1

Tactic:
refine (this.const_mul 2).congr_deriv ?_

Result:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
this : HasDerivAt (fun x => (2 * ↑π) ^ (-x)) ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) 1
⊢ 2 * ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) = -log (2 * ↑π) / ↑π

Proof state:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Tactic:
have : HasDerivAt (fun s : ℂ ↦ 2 * (2 * π : ℂ) ^ (-s)) (-log (2 * π) / π) 1 := by
  have := (hasDerivAt_neg' (1 : ℂ)).const_cpow (c := 2 * π)
    (Or.inl (by exact_mod_cast Real.two_pi_pos.ne'))
  refine (this.const_mul 2).congr_deriv ?_
  rw [mul_neg_one, mul_neg, cpow_neg_one, ← div_eq_inv_mul, ← mul_div_assoc,
    mul_div_mul_left _ _ two_ne_zero, neg_div]

Result:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
this : HasDerivAt (fun s => 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Proof state:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
this : HasDerivAt (fun x => (2 * ↑π) ^ (-x)) ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) 1
⊢ 2 * ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) = -log (2 * ↑π) / ↑π

Tactic:
rw [mul_neg_one, mul_neg, cpow_neg_one, ← div_eq_inv_mul, ← mul_div_assoc,
  mul_div_mul_left _ _ two_ne_zero, neg_div]

Result:
no goals

Proof state:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
this✝ : HasDerivAt (fun s => 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1
this : HasDerivAt (fun y => 2 * (2 * ↑π) ^ (-y) * Gamma y) (-log (2 * ↑π) / ↑π * Gamma 1 + 2 * (2 * ↑π) ^ (-1) * -↑γ) 1
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Tactic:
rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
  mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this

Result:
no goals

Proof state:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
this : HasDerivAt (fun s => 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Tactic:
have := this.mul hasDerivAt_Gamma_one

Result:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
this✝ : HasDerivAt (fun s => 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1
this : HasDerivAt (fun y => 2 * (2 * ↑π) ^ (-y) * Gamma y) (-log (2 * ↑π) / ↑π * Gamma 1 + 2 * (2 * ↑π) ^ (-1) * -↑γ) 1
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Proof state:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
⊢ 2 * ↑π ≠ 0

Tactic:
exact_mod_cast Real.two_pi_pos.ne'

Result:
no goals

Proof state:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
⊢ HasDerivAt (fun s => 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1

Tactic:
have := (hasDerivAt_neg' (1 : ℂ)).const_cpow (c := 2 * π)
  (Or.inl (by exact_mod_cast Real.two_pi_pos.ne'))

Result:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
this : HasDerivAt (fun x => (2 * ↑π) ^ (-x)) ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) 1
⊢ HasDerivAt (fun s => 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1

Proof state:
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Tactic:
let f (s : ℂ) : ℂ := 2 * (2 * π) ^ (-s)

Result:
f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1