-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
calc : deriv Gamma (1 / 2) = deriv (fun (s : ℝ) ↦ Gamma s * Gamma (s + 1 / 2)) (1 / 2) + √π * γ
calc₁ :
  deriv (fun (s : ℝ) ↦ Gamma s * Gamma (s + 1 / 2)) (1 / 2) + √π * γ =
    deriv (fun (s : ℝ) ↦ Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s) * √π) (1 / 2) + √π * γ
calc₂ :
  deriv (fun (s : ℝ) ↦ Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s) * √π) (1 / 2) + √π * γ =
    √π * (deriv (fun (s : ℝ) ↦ Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2) + γ)
calc₃ :
  √π * (deriv (fun (s : ℝ) ↦ Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2) + γ) =
    √π *
      (HAdd.hAdd (α := ℝ) (deriv (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2))
          (deriv (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)) +
        γ)
calc₄ :
  √π *
      (HAdd.hAdd (α := ℝ) (deriv (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2))
          (deriv (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)) +
        γ) =
    √π * (-2 * γ + deriv (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2) + γ)
calc₅ :
  √π * (-2 * γ + deriv (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2) + γ) = √π * (-2 * γ + -(2 * log 2) + γ)
calc₆ : √π * (-2 * γ + -(2 * log 2) + γ) = -√π * (γ + 2 * log 2)
⊢ deriv Gamma (1 / 2) = -√π * (γ + 2 * log 2)

Tactic:
calc deriv Gamma (1 / 2)
  _ = (deriv (fun s ↦ Gamma s * Gamma (s + 1 / 2)) (1 / 2)) + √π * γ := by
    rw [deriv_fun_mul, Gamma_one_half_eq,
      add_assoc, ← mul_add, deriv_comp_add_const,
      (by norm_num : 1 / 2 + 1 / 2 = (1 : ℝ)), Gamma_one, mul_one,
      eulerMascheroniConstant_eq_neg_deriv, add_neg_cancel, mul_zero, add_zero]
    · apply h_diff; simp -- s = 1
    · exact ((h_diff (by simp)).hasDerivAt.comp_add_const).differentiableAt -- s = 1
  _ = (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2)) + √π * γ := by
    rw [funext Gamma_mul_Gamma_add_half]
  _ = √π * (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ) := by
    rw [mul_comm √π, mul_comm √π, deriv_mul_const, add_mul]
    apply DifferentiableAt.mul
    · exact .comp (g := Gamma) _ (by apply h_diff; simp) -- s = 1
        (differentiableAt_id.const_mul _)
    · exact (differentiableAt_const _).rpow (by fun_prop) two_ne_zero
  _ = √π * (deriv (fun s ↦ Gamma (2 * s)) (1 / 2) +
              deriv (fun s : ℝ ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) := by
    rw [deriv_fun_mul]
    · simp
    · exact h_diff' one_half_pos
    · exact DifferentiableAt.rpow (by fun_prop) (by fun_prop) two_ne_zero
  _ = √π * (-2 * γ + deriv (fun s : ℝ ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) := by
    congr 3
    change deriv (Gamma ∘ fun s ↦ 2 * s) _ = _
    rw [deriv_comp, deriv_const_mul_id, mul_one_div, div_self two_ne_zero]
    · rw [mul_comm, hasDerivAt_Gamma_one.deriv, mul_neg, neg_mul]
    · apply h_diff; simp -- s = 1
    · fun_prop
  _ = √π * (-2 * γ + -(2 * log 2) + γ) := by
    congr 3
    apply HasDerivAt.deriv
    have := HasDerivAt.rpow (hasDerivAt_const (1 / 2 : ℝ) (2 : ℝ))
      (?_ : HasDerivAt (fun s : ℝ ↦ 1 - 2 * s) (-2) (1 / 2)) two_pos
    · simpa
    simp_rw [mul_comm (2 : ℝ) _]
    apply HasDerivAt.const_sub
    exact hasDerivAt_mul_const (2 : ℝ)
  _ = -√π * (γ + 2 * log 2) := by ring

Premises used: Real.pi, HMul.hMul, deriv, HSub.hSub, HDiv.hDiv, Real.log, Real.eulerMascheroniConstant, HPow.hPow, HAdd.hAdd, Real.Gamma, Real.sqrt, OfNat.ofNat, Neg.neg