awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
e_a : 2 * deriv Gamma 1 = -2 * γ
⊢ deriv Gamma 1 * 2 = -2 * γ
have e_a₁ : 2 * -γ = -2 * γ
Tactic: rw [mul_comm, hasDerivAt_Gamma_one.deriv, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
e_a : 2 * deriv Gamma 1 = -2 * γ
e_a₁ : 2 * -γ = -2 * γ
⊢ deriv Gamma 1 * 2 = -2 * γ
have e_a₂ : -(2 * γ) = -2 * γ
Tactic: rw [mul_comm, hasDerivAt_Gamma_one.deriv, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
e_a : 2 * deriv Gamma 1 = -2 * γ
e_a₁ : 2 * -γ = -2 * γ
e_a₂ : -(2 * γ) = -2 * γ
⊢ deriv Gamma 1 * 2 = -2 * γ
have e_a₃ : -(2 * γ) = -(2 * γ)
Tactic: rw [mul_comm, hasDerivAt_Gamma_one.deriv, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (2 * (1 / 2))
have e_a : 0 < 2 * (1 / 2)
Tactic: apply h_diff
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
⊢ √π * (-2 * γ + deriv (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2) + γ) = √π * (-2 * γ + -(2 * log 2) + γ)
have e_a : deriv (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2) = -(2 * log 2)
Tactic: congr 3
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
⊢ deriv (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2) = -(2 * log 2)
have e_a : HasDerivAt (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (-(2 * log 2)) (1 / 2)
Tactic: apply HasDerivAt.deriv
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
⊢ HasDerivAt (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (-(2 * log 2)) (1 / 2)
have e_a : ∀
  (this :
    HasDerivAt (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * x))
      (0 * (1 - 2 * (1 / 2)) * HPow.hPow (α := ℝ) 2 (1 - 2 * (1 / 2) - 1) +
        -2 * HPow.hPow (α := ℝ) 2 (1 - 2 * (1 / 2)) * log 2)
      (1 / 2)),
  HasDerivAt (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (-(2 * log 2)) (1 / 2)
Tactic: have := HasDerivAt.rpow (hasDerivAt_const (1 / 2 : ℝ) (2 : ℝ))
      (?_ : HasDerivAt (fun s : ℝ ↦ 1 - 2 * s) (-2) (1 / 2)) two_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
e_a :
  ∀
    (this :
      HasDerivAt (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * x))
        (0 * (1 - 2 * (1 / 2)) * HPow.hPow (α := ℝ) 2 (1 - 2 * (1 / 2) - 1) +
          -2 * HPow.hPow (α := ℝ) 2 (1 - 2 * (1 / 2)) * log 2)
        (1 / 2)),
    HasDerivAt (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (-(2 * log 2)) (1 / 2)
⊢ HasDerivAt (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (-(2 * log 2)) (1 / 2)
have e_a₁ : HasDerivAt (F := ℝ) (fun (s : ℝ) ↦ 1 - 2 * s) (-2) (1 / 2)
Tactic: have := HasDerivAt.rpow (hasDerivAt_const (1 / 2 : ℝ) (2 : ℝ))
      (?_ : HasDerivAt (fun s : ℝ ↦ 1 - 2 * s) (-2) (1 / 2)) two_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
⊢ HasDerivAt (F := ℝ) (fun (s : ℝ) ↦ 1 - 2 * s) (-2) (1 / 2)
have e_a : HasDerivAt (F := ℝ) (fun (s : ℝ) ↦ 1 - s * 2) (-2) (1 / 2)
Tactic: simp_rw [mul_comm (2 : ℝ) _]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
⊢ HasDerivAt (F := ℝ) (fun (s : ℝ) ↦ 1 - s * 2) (-2) (1 / 2)
have e_a : HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ x * 2) 2 (1 / 2)
Tactic: apply HasDerivAt.const_sub
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
⊢ deriv Gamma (1 / 2) = -√π * (γ + 2 * log 2)
have calc : deriv Gamma (1 / 2) = deriv (fun (s : ℝ) ↦ Gamma s * Gamma (s + 1 / 2)) (1 / 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
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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) + √π * γ
⊢ deriv Gamma (1 / 2) = -√π * (γ + 2 * log 2)
have 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) + √π * γ
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
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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) + √π * γ
⊢ deriv Gamma (1 / 2) = -√π * (γ + 2 * log 2)
have 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) + γ)
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
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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) + γ)
⊢ deriv Gamma (1 / 2) = -√π * (γ + 2 * log 2)
have 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)) +
      γ)
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
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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)) +
        γ)
⊢ deriv Gamma (1 / 2) = -√π * (γ + 2 * log 2)
have 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) + γ)
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
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f (↑s : ℂ)
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f (↑s : ℂ) = (↑(g s) : ℂ)
⊢ HasDerivAt f (↑g' : ℂ) (↑s : ℂ)
have refine : deriv f (↑s : ℂ) = (↑g' : ℂ)
Tactic: refine HasDerivAt.congr_deriv hf.hasDerivAt ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f (↑s : ℂ)
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f (↑s : ℂ) = (↑(g s) : ℂ)
⊢ deriv f (↑s : ℂ) = (↑g' : ℂ)
have rw : deriv (fun (x : ℝ) ↦ (↑(g x) : ℂ)) s = (↑g' : ℂ)
Tactic: rw [← (funext hfg ▸ hf.hasDerivAt.comp_ofReal.deriv :)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
⊢ DifferentiableAt ℂ Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
have refine : ∀ (m : ℕ), HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ -(↑m : ℂ)
Tactic: refine differentiableAt_Gamma _ (fun m ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n m : ℕ
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ -(↑m : ℂ)
have simp : ¬HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + (↑m : ℝ) = 0
Tactic: simp only [Ne, ← ofReal_natCast, ← ofReal_one, ← ofReal_add, ← ofReal_neg, ofReal_inj,
    eq_neg_iff_add_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
⊢ HasDerivAt Gamma (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2)) (1 / 2)
have refine_2 : ∀ (this : HasDerivAt Gamma (↑(-√π * (γ + 2 * Real.log 2)) : ℂ) (↑(1 / 2) : ℂ)),
  HasDerivAt Gamma (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2)) (1 / 2)
Tactic: have := HasDerivAt.complex_of_real
    (differentiableAt_Gamma _ ?_) Real.hasDerivAt_Gamma_one_half Gamma_ofReal
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
refine_2 :
  ∀ (this : HasDerivAt Gamma (↑(-√π * (γ + 2 * Real.log 2)) : ℂ) (↑(1 / 2) : ℂ)),
    HasDerivAt Gamma (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2)) (1 / 2)
⊢ HasDerivAt Gamma (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2)) (1 / 2)
have refine_1 : ∀ (m : ℕ), (↑(1 / 2) : ℂ) ≠ -(↑m : ℂ)
Tactic: have := HasDerivAt.complex_of_real
    (differentiableAt_Gamma _ ?_) Real.hasDerivAt_Gamma_one_half Gamma_ofReal
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
m : ℕ
⊢ (↑(1 / 2) : ℂ) ≠ -(↑m : ℂ)
have refine_1 : ¬1 / 2 = -(↑m : ℝ)
Tactic: rw [← ofReal_natCast, ← ofReal_neg, ne_eq, ofReal_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
⊢ HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
have this : HasDerivAt (fun (x : ℂ) ↦ (2 * (↑π : ℂ)) ^ (-x)) (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) 1
Tactic: have := (hasDerivAt_neg' (1 : ℂ)).const_cpow (c := 2 * π)
      (Or.inl (by exact_mod_cast Real.two_pi_pos.ne'))
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this :
  HasDerivAt (fun (x : ℂ) ↦ (2 * (↑π : ℂ)) ^ (-x)) (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) 1
⊢ HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
have refine : 2 * (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
Tactic: refine (this.const_mul 2).congr_deriv ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this :
  HasDerivAt (fun (x : ℂ) ↦ (2 * (↑π : ℂ)) ^ (-x)) (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) 1
⊢ 2 * (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
have rw : 2 * -(HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ))) = -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]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this :
  HasDerivAt (fun (x : ℂ) ↦ (2 * (↑π : ℂ)) ^ (-x)) (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) 1
rw : 2 * -(HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
⊢ 2 * (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
have rw₁ : -(2 * (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)))) = -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]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this :
  HasDerivAt (fun (x : ℂ) ↦ (2 * (↑π : ℂ)) ^ (-x)) (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) 1
rw : 2 * -(HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
rw₁ : -(2 * (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
⊢ 2 * (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
have rw₂ : -(2 * ((2 * (↑π : ℂ))⁻¹ * log (2 * (↑π : ℂ)))) = -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]