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

Proof state:
case e_a.e_a.e_a.h.refine_1
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ HasDerivAt (fun s => 1 - s * 2) (-2) (1 / 2)

Tactic:
apply HasDerivAt.const_sub

Result:
case e_a.e_a.e_a.h.refine_1.hf
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ HasDerivAt (fun x => x * 2) 2 (1 / 2)

Proof state:
case hc.hs
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ 0 < 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
case e_a.e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ deriv (fun s => 2 ^ (1 - 2 * s)) (1 / 2) = -(2 * log 2)

Tactic:
apply HasDerivAt.deriv

Result:
case e_a.e_a.e_a.h
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ HasDerivAt (fun s => 2 ^ (1 - 2 * s)) (-(2 * log 2)) (1 / 2)

Proof state:
case e_a.e_a.e_a.hh₂
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (2 * (1 / 2))

Tactic:
apply h_diff

Result:
case e_a.e_a.e_a.hh₂.hs
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ 0 < 2 * (1 / 2)

Proof state:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ deriv (fun s => Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2) + √π * γ =
    √π * (deriv (fun s => Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ)

Tactic:
rw [mul_comm √π, mul_comm √π, deriv_mul_const, add_mul]

Result:
case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s => Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2)

Proof state:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ deriv Gamma (1 / 2) = deriv (fun s => Gamma s * Gamma (s + 1 / 2)) (1 / 2) + √π * γ

Tactic:
rw [deriv_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]

Result:
case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (1 / 2)

case hd
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s => Gamma (s + 1 / 2)) (1 / 2)

Proof state:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s => 1 - 2 * s) (1 / 2)

Tactic:
fun_prop

Result:
no goals

Proof state:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ 0 < 1 / 2 + 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
case e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ deriv (fun s => Gamma (2 * s)) (1 / 2) * 2 ^ (1 - 2 * (1 / 2)) +
      Gamma (2 * (1 / 2)) * deriv (fun s => 2 ^ (1 - 2 * s)) (1 / 2) =
    deriv (fun s => Gamma (2 * s)) (1 / 2) + deriv (fun s => 2 ^ (1 - 2 * s)) (1 / 2)

Tactic:
congr 1 <;> norm_num

Result:
no goals

Proof state:
case e_a.e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ deriv Gamma 1 * (2 * 1) = -2 * γ

Tactic:
rw [mul_one, mul_comm, hasDerivAt_Gamma_one.deriv, mul_neg, neg_mul]

Result:
no goals

Proof state:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ deriv (fun s => Gamma s * Gamma (s + 1 / 2)) (1 / 2) + √π * γ =
    deriv (fun s => Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2) + √π * γ

Tactic:
rw [funext Gamma_mul_Gamma_add_half]

Result:
no goals

Proof state:
case e_a.e_a.e_a.h.refine_1.hf
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ HasDerivAt (fun x => x * 2) 2 (1 / 2)

Tactic:
exact hasDerivAt_mul_const (2 : ℝ)

Result:
no goals

Proof state:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ √π * (deriv (fun s => Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ) =
    √π * (deriv (fun s => Gamma (2 * s)) (1 / 2) + deriv (fun s => 2 ^ (1 - 2 * s)) (1 / 2) + γ)

Tactic:
congr 2

Result:
case e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ deriv (fun s => Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) =
    deriv (fun s => Gamma (2 * s)) (1 / 2) + deriv (fun s => 2 ^ (1 - 2 * s)) (1 / 2)

Proof state:
case e_a.e_a.e_a.h.refine_2
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
this :
  HasDerivAt (fun x => 2 ^ (1 - 2 * x))
    (0 * (1 - 2 * (1 / 2)) * 2 ^ (1 - 2 * (1 / 2) - 1) + -2 * 2 ^ (1 - 2 * (1 / 2)) * log 2) (1 / 2)
⊢ HasDerivAt (fun s => 2 ^ (1 - 2 * s)) (-(2 * log 2)) (1 / 2)

Tactic:
norm_num at this

Result:
case e_a.e_a.e_a.h.refine_2
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
this : HasDerivAt (fun x => 2 ^ (1 - 2 * x)) (-(2 * log 2)) (1 / 2)
⊢ HasDerivAt (fun s => 2 ^ (1 - 2 * s)) (-(2 * log 2)) (1 / 2)

Proof state:
case e_a.e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ deriv (Gamma ∘ fun s => 2 * s) (1 / 2) = -2 * γ

Tactic:
rw [deriv_comp, deriv_const_mul, mul_one_div, div_self two_ne_zero, deriv_id''] <;>
dsimp only

Result:
case e_a.e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ deriv Gamma 1 * (2 * 1) = -2 * γ

case e_a.e_a.e_a.hd
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s => s) (1 / 2)

case e_a.e_a.e_a.hh₂
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (2 * (1 / 2))

case e_a.e_a.e_a.hh
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s => 2 * s) (1 / 2)

Proof state:
case e_a.e_a.e_a.hd
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s => s) (1 / 2)

Tactic:
fun_prop

Result:
no goals

Proof state:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)

Tactic:
refine (h_diff one_half_pos).hasDerivAt.congr_deriv ?_

Result:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ deriv Gamma (1 / 2) = -√π * (γ + 2 * log 2)