-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
lemma hasDerivAt_Gamma_one_half : HasDerivAt Gamma (-√π * (γ + 2 * log 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
⊢ 1 / 2 + 1 / 2 = 1

Tactic:
norm_num

Result:
no goals

Proof state:
case 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 => 2 ^ (1 - 2 * s)) (1 / 2)

Tactic:
exact DifferentiableAt.rpow (by fun_prop) (by fun_prop) two_ne_zero

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 => Gamma (2 * s)) (1 / 2) = -2 * γ

Tactic:
change deriv (Gamma ∘ fun s ↦ 2 * s) _ = _

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 ∘ fun s => 2 * s) (1 / 2) = -2 * γ

Proof state:
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)

Tactic:
norm_num

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
⊢ √π * (-2 * γ + deriv (fun s => 2 ^ (1 - 2 * s)) (1 / 2) + γ) = √π * (-2 * γ + -(2 * log 2) + γ)

Tactic:
congr 3

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 (fun s => 2 ^ (1 - 2 * s)) (1 / 2) = -(2 * log 2)

Proof state:
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)

Tactic:
apply h_diff

Result:
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

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)) (1 / 2) + deriv (fun s => 2 ^ (1 - 2 * s)) (1 / 2) + γ) =
    √π * (-2 * γ + deriv (fun s => 2 ^ (1 - 2 * s)) (1 / 2) + γ)

Tactic:
congr 3

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 (fun s => Gamma (2 * s)) (1 / 2) = -2 * γ

Proof state:
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)

Tactic:
exact ((h_diff (by norm_num)).hasDerivAt.comp_add_const).differentiableAt

Result:
no goals

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

Tactic:
have h_diff {s : ℝ} (hs : 0 < s) : DifferentiableAt ℝ Gamma s :=
  differentiableAt_Gamma fun m ↦ ((neg_nonpos.mpr m.cast_nonneg).trans_lt hs).ne'

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

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) * 2 ^ (1 - 2 * s)) (1 / 2) =
    deriv (fun s => Gamma (2 * s)) (1 / 2) + deriv (fun s => 2 ^ (1 - 2 * s)) (1 / 2)

Tactic:
rw [deriv_mul]

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)) (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)

case e_a.e_a.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)) (1 / 2)

case 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 => 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
⊢ DifferentiableAt ℝ (fun y => 1 - 2 * y) (1 / 2)

Tactic:
fun_prop

Result:
no goals

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 ℝ (fun s => 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
⊢ DifferentiableAt ℝ Gamma (2 * (1 / 2))

Tactic:
apply h_diff

Result:
case 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:
case hc.ha
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun y => Gamma (2 * y)) (1 / 2)

Tactic:
exact .comp (g := Gamma) _ (by apply h_diff; norm_num) (differentiableAt_id.const_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
⊢ DifferentiableAt ℝ (fun s => 2) (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
⊢ √π * (-2 * γ + -(2 * log 2) + γ) = -√π * (γ + 2 * log 2)

Tactic:
ring

Result:
no goals

Proof state:
case e_a.e_a.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)) (1 / 2)

Tactic:
exact h_diff' one_half_pos

Result:
no goals

Proof state:
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)

Tactic:
apply DifferentiableAt.mul

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

case hc.hb
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun y => 2 ^ (1 - 2 * y)) (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 - 2 * s) (-2) (1 / 2)

Tactic:
simp_rw [mul_comm (2 : ℝ) _]

Result:
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)

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

Tactic:
exact (differentiableAt_const _).rpow (by fun_prop) two_ne_zero

Result:
no goals