awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw :
  √π *
      (deriv (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2) * HPow.hPow (α := ℝ) 2 (1 - 2 * (1 / 2)) +
          Gamma (2 * (1 / 2)) * deriv (fun (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)) +
        γ)
hc : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2)
hd : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)
⊢ √π * (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:
rw [deriv_fun_mul]

Premises used: deriv_fun_mul
-- 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
⊢ √π *
      (deriv (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2) * HPow.hPow (α := ℝ) 2 (1 - 2 * (1 / 2)) +
          Gamma (2 * (1 / 2)) * deriv (fun (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:
simp
-- 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
⊢ DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2)

Tactic:
h_diff' one_half_pos

Premises used: one_half_pos
-- 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
⊢ DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2)

Tactic:
exact h_diff' one_half_pos

Premises used: one_half_pos
-- 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
⊢ DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ 2) (1 / 2)

Tactic:
fun_prop
-- 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
⊢ DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)

Tactic:
exact DifferentiableAt.rpow (by fun_prop) (by fun_prop) two_ne_zero
-- 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
e_a : deriv (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2) = -2 * γ
⊢ √π *
      (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:
congr 3
-- 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
e_a : deriv Gamma 1 * 2 = -2 * γ
e_a₁ : DifferentiableAt ℝ Gamma (2 * (1 / 2))
e_a₂ : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ 2 * s) (1 / 2)
⊢ deriv (Gamma ∘ fun (s : ℝ) ↦ 2 * s) (1 / 2) = -2 * γ

Tactic:
rw [deriv_comp, deriv_const_mul_id, mul_one_div, div_self two_ne_zero]

Premises used: deriv_comp, deriv_const_mul_id, two_ne_zero, mul_one_div, div_self
-- 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
e_a : 2 * deriv Gamma 1 = -2 * γ
e_a₁ : 2 * -γ = -2 * γ
e_a₂ : -(2 * γ) = -2 * γ
e_a₃ e_a₄ : -(2 * γ) = -(2 * γ)
⊢ deriv Gamma 1 * 2 = -2 * γ

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

Premises used: HasDerivAt.deriv, Real.hasDerivAt_Gamma_one, mul_comm, neg_mul, mul_neg
-- 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
e_a : 0 < 2 * (1 / 2)
⊢ DifferentiableAt ℝ Gamma (2 * (1 / 2))

Tactic:
apply h_diff
-- 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
⊢ DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ 2 * s) (1 / 2)

Tactic:
fun_prop
-- 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
e_a : deriv (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2) = -(2 * log 2)
⊢ √π * (-2 * γ + deriv (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2) + γ) = √π * (-2 * γ + -(2 * log 2) + γ)

Tactic:
congr 3
-- 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
e_a : HasDerivAt (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (-(2 * log 2)) (1 / 2)
⊢ deriv (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2) = -(2 * log 2)

Tactic:
apply HasDerivAt.deriv

Premises used: HasDerivAt.deriv
-- 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
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)
e_a₁ : HasDerivAt (F := ℝ) (fun (s : ℝ) ↦ 1 - 2 * s) (-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
-- 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
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:
simpa
-- 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
e_a : HasDerivAt (F := ℝ) (fun (s : ℝ) ↦ 1 - s * 2) (-2) (1 / 2)
⊢ HasDerivAt (F := ℝ) (fun (s : ℝ) ↦ 1 - 2 * s) (-2) (1 / 2)

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

Premises used: mul_comm, OfNat.ofNat
-- 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
e_a : HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ x * 2) 2 (1 / 2)
⊢ HasDerivAt (F := ℝ) (fun (s : ℝ) ↦ 1 - s * 2) (-2) (1 / 2)

Tactic:
apply HasDerivAt.const_sub

Premises used: HasDerivAt.const_sub
-- 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
⊢ HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ x * 2) 2 (1 / 2)

Tactic:
hasDerivAt_mul_const (2 : ℝ)

Premises used: hasDerivAt_mul_const, OfNat.ofNat
-- 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
⊢ HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ x * 2) 2 (1 / 2)

Tactic:
exact hasDerivAt_mul_const (2 : ℝ)

Premises used: hasDerivAt_mul_const, OfNat.ofNat
-- 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
⊢ √π * (-2 * γ + -(2 * log 2) + γ) = -√π * (γ + 2 * log 2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f (↑s : ℂ)
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f (↑s : ℂ) = (↑(g s) : ℂ)
⊢ HasDerivAt f (↑g' : ℂ) (↑s : ℂ)

Tactic:
HasDerivAt.congr_deriv hf.hasDerivAt ?_

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.congr_deriv
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f (↑s : ℂ)
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f (↑s : ℂ) = (↑(g s) : ℂ)
refine : deriv f (↑s : ℂ) = (↑g' : ℂ)
⊢ HasDerivAt f (↑g' : ℂ) (↑s : ℂ)

Tactic:
refine HasDerivAt.congr_deriv hf.hasDerivAt ?_

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.congr_deriv
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f (↑s : ℂ)
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f (↑s : ℂ) = (↑(g s) : ℂ)
rw : deriv (fun (x : ℝ) ↦ (↑(g x) : ℂ)) s = (↑g' : ℂ)
⊢ deriv f (↑s : ℂ) = (↑g' : ℂ)

Tactic:
rw [← (funext hfg ▸ hf.hasDerivAt.comp_ofReal.deriv :)]
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f (↑s : ℂ)
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f (↑s : ℂ) = (↑(g s) : ℂ)
⊢ deriv (fun (x : ℝ) ↦ (↑(g x) : ℂ)) s = (↑g' : ℂ)

Tactic:
hg.ofReal_comp.deriv

Premises used: HasDerivAt.deriv, HasDerivAt.ofReal_comp
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f (↑s : ℂ)
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f (↑s : ℂ) = (↑(g s) : ℂ)
⊢ deriv (fun (x : ℝ) ↦ (↑(g x) : ℂ)) s = (↑g' : ℂ)

Tactic:
exact hg.ofReal_comp.deriv

Premises used: HasDerivAt.deriv, HasDerivAt.ofReal_comp
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n : ℕ
⊢ DifferentiableAt ℂ Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)

Tactic:
differentiableAt_Gamma _ (fun m ↦ ?_)

Premises used: Complex.differentiableAt_Gamma
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n : ℕ
refine : ∀ (m : ℕ), HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ -(↑m : ℂ)
⊢ DifferentiableAt ℂ Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)

Tactic:
refine differentiableAt_Gamma _ (fun m ↦ ?_)

Premises used: Complex.differentiableAt_Gamma
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n m : ℕ
simp : ¬HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + (↑m : ℝ) = 0
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ -(↑m : ℂ)

Tactic:
simp only [Ne, ← ofReal_natCast, ← ofReal_one, ← ofReal_add, ← ofReal_neg, ofReal_inj,
    eq_neg_iff_add_eq_zero]

Premises used: Complex.ofReal_neg, Complex.ofReal_add, Complex.ofReal_one, Ne, Complex.ofReal_natCast, Complex.ofReal_inj, eq_neg_iff_add_eq_zero
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n m : ℕ
⊢ ¬HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + (↑m : ℝ) = 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n : ℕ
⊢ DifferentiableAt ℂ Gamma (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)

Tactic:
exact_mod_cast differentiableAt_Gamma_nat_add_one n

Premises used: Complex.differentiableAt_Gamma_nat_add_one
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n : ℕ
⊢ HasDerivAt Gamma ((↑n ! : ℂ) * (-(↑γ : ℂ) + (↑(harmonic n) : ℂ))) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)

Tactic:
exact_mod_cast HasDerivAt.complex_of_real
    (by exact_mod_cast differentiableAt_Gamma_nat_add_one n)
    (Real.hasDerivAt_Gamma_nat n) Gamma_ofReal

Premises used: _private.0.Complex.HasDerivAt.complex_of_real, Real.hasDerivAt_Gamma_nat, Complex.Gamma_ofReal
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n : ℕ
⊢ deriv Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) = (↑n ! : ℂ) * (-(↑γ : ℂ) + (↑(harmonic n) : ℂ))

Tactic:
(hasDerivAt_Gamma_nat n).deriv

Premises used: HasDerivAt.deriv, Complex.hasDerivAt_Gamma_nat
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
⊢ HasDerivAt Gamma (-(↑γ : ℂ)) 1

Tactic:
simpa only [factorial_zero, cast_one, harmonic_zero, Rat.cast_zero, add_zero, mul_neg, one_mul,
    cast_zero, zero_add] using hasDerivAt_Gamma_nat 0

Premises used: harmonic_zero, zero_add, Rat.cast_zero, Nat.factorial_zero, Nat.cast_zero, add_zero, OfNat.ofNat, Nat.cast_one, one_mul, mul_neg, Complex.hasDerivAt_Gamma_nat
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
refine_2 :
  ∀ (this : HasDerivAt Gamma (↑(-√π * (γ + 2 * Real.log 2)) : ℂ) (↑(1 / 2) : ℂ)),
    HasDerivAt Gamma (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2)) (1 / 2)
refine_1 : ∀ (m : ℕ), (↑(1 / 2) : ℂ) ≠ -(↑m : ℂ)
⊢ HasDerivAt Gamma (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2)) (1 / 2)

Tactic:
have := HasDerivAt.complex_of_real
    (differentiableAt_Gamma _ ?_) Real.hasDerivAt_Gamma_one_half Gamma_ofReal
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
this : HasDerivAt Gamma (↑(-√π * (γ + 2 * Real.log 2)) : ℂ) (↑(1 / 2) : ℂ)
⊢ HasDerivAt Gamma (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2)) (1 / 2)

Tactic:
simpa only [neg_mul, one_div, ofReal_neg, ofReal_mul, ofReal_add, ofReal_ofNat, ofNat_log,
      ofReal_inv] using this

Premises used: Complex.ofNat_log, Complex.ofReal_neg, Complex.ofReal_add, one_div, neg_mul, Complex.ofReal_ofNat, Complex.ofReal_inv, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
m : ℕ
refine_1 : ¬1 / 2 = -(↑m : ℝ)
⊢ (↑(1 / 2) : ℂ) ≠ -(↑m : ℂ)

Tactic:
rw [← ofReal_natCast, ← ofReal_neg, ne_eq, ofReal_inj]

Premises used: Complex.ofReal_neg, ne_eq, Complex.ofReal_natCast, Complex.ofReal_inj
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
m : ℕ
⊢ ¬1 / 2 = -(↑m : ℝ)

Tactic:
((neg_nonpos.mpr m.cast_nonneg).trans_lt one_half_pos).ne'

Premises used: Iff.mpr, neg_nonpos, LT.lt.ne', LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
m : ℕ
⊢ ¬1 / 2 = -(↑m : ℝ)

Tactic:
exact ((neg_nonpos.mpr m.cast_nonneg).trans_lt one_half_pos).ne'

Premises used: Iff.mpr, neg_nonpos, LT.lt.ne', LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
⊢ 2 * (↑π : ℂ) ≠ 0

Tactic:
exact_mod_cast Real.two_pi_pos.ne'

Premises used: Real.two_pi_pos, LT.lt.ne'
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
⊢ 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'))
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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

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

Premises used: HasDerivAt.const_mul, OfNat.ofNat, HasDerivAt.congr_deriv
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this :
  HasDerivAt (fun (x : ℂ) ↦ (2 * (↑π : ℂ)) ^ (-x)) (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) 1
refine : 2 * (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
⊢ HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1

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

Premises used: HasDerivAt.const_mul, OfNat.ofNat, HasDerivAt.congr_deriv
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 * (↑π : ℂ)) / (↑π : ℂ)
rw₂ : -(2 * ((2 * (↑π : ℂ))⁻¹ * log (2 * (↑π : ℂ)))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
rw₃ : -(2 * (log (2 * (↑π : ℂ)) / (2 * (↑π : ℂ)))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
rw₄ : -(2 * log (2 * (↑π : ℂ)) / (2 * (↑π : ℂ))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
rw₅ : -(log (2 * (↑π : ℂ)) / (↑π : ℂ)) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
rw₆ rw₇ : -(log (2 * (↑π : ℂ)) / (↑π : ℂ)) = -(log (2 * (↑π : ℂ)) / (↑π : ℂ))
⊢ 2 * (HPow.hPow (β := ℂ) (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]

Premises used: neg_div, Complex.cpow_neg_one, mul_div_assoc, two_ne_zero, mul_div_mul_left, mul_neg_one, div_eq_inv_mul, mul_neg
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
⊢ HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-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]
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this : HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
⊢ HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
    (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * Gamma 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1

Tactic:
have := this.mul hasDerivAt_Gamma_one
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
rw : (↑π : ℂ) ^ (1 / 2) = (↑(π ^ (1 / 2)) : ℂ)
rw₁ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ (↑(1 / 2) : ℂ)
rw₂ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ ((↑1 : ℂ) / (↑2 : ℂ))
rw₃ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ (1 / (↑2 : ℂ))
rw₄ rw₅ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ HDiv.hDiv (α := ℂ) 1 2
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)

Tactic:
rw [Real.sqrt_eq_rpow, ofReal_cpow Real.pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]

Premises used: Complex.ofReal_cpow, Real.pi_pos, LT.lt.le, Complex.ofReal_one, Complex.ofReal_div, Complex.ofReal_ofNat, Real.sqrt_eq_rpow
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)

Tactic:
have aux : (π : ℂ) ^ (1 / 2 : ℂ) = ↑√π := by
    rw [Real.sqrt_eq_rpow, ofReal_cpow Real.pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
rw : √π ≠ 0
⊢ (↑√π : ℂ) ≠ 0

Tactic:
rw [ofReal_ne_zero]

Premises used: Complex.ofReal_ne_zero
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
⊢ √π ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
⊢ (↑√π : ℂ) ≠ 0

Tactic:
have aux2 : (√π : ℂ) ≠ 0 := by rw [ofReal_ne_zero]; positivity
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
⊢ -1 / 2 ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
⊢ HasDerivAt (fun (x : ℂ) ↦ (↑π : ℂ) ^ (-x / 2)) ((↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2)) 1

Tactic:
have := ((hasDerivAt_neg (1 : ℂ)).div_const 2).const_cpow (c := π) (Or.inr (by simp))
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
this : HasDerivAt (fun (x : ℂ) ↦ (↑π : ℂ) ^ (-x / 2)) ((↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2)) 1
⊢ HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1

Tactic:
this.congr_deriv ?_

Premises used: HasDerivAt.congr_deriv
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
this : HasDerivAt (fun (x : ℂ) ↦ (↑π : ℂ) ^ (-x / 2)) ((↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2)) 1
refine : (↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
⊢ HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1

Tactic:
refine this.congr_deriv ?_

Premises used: HasDerivAt.congr_deriv
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
this : HasDerivAt (fun (x : ℂ) ↦ (↑π : ℂ) ^ (-x / 2)) ((↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2)) 1
rw : (↑π : ℂ) ^ (-1 / 2) * (log (↑π : ℂ) * (-1 / 2)) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
rw₁ : (↑π : ℂ) ^ (-1 / 2) * (log (↑π : ℂ) * -1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
rw₂ : (↑π : ℂ) ^ (-1 / 2) * (-log (↑π : ℂ) / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
rw₃ : (↑π : ℂ) ^ (-(1 / 2)) * (-log (↑π : ℂ) / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
rw₄ : ((↑π : ℂ) ^ (1 / 2))⁻¹ * (-log (↑π : ℂ) / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
rw₅ : -log (↑π : ℂ) / 2 / (↑π : ℂ) ^ (1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
rw₆ rw₇ : -log (↑π : ℂ) / 2 / (↑√π : ℂ) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
⊢ (↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)

Tactic:
rw [mul_assoc, ← mul_div_assoc, mul_neg_one, neg_div, cpow_neg, ← div_eq_inv_mul, aux]

Premises used: neg_div, mul_assoc, mul_div_assoc, Complex.cpow_neg, mul_neg_one, div_eq_inv_mul
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
⊢ HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1

Tactic:
have hf : HasDerivAt f (-log π / 2 / √π) 1 := by
    have := ((hasDerivAt_neg (1 : ℂ)).div_const 2).const_cpow (c := π) (Or.inr (by simp))
    refine this.congr_deriv ?_
    rw [mul_assoc, ← mul_div_assoc, mul_neg_one, neg_div, cpow_neg, ← div_eq_inv_mul, aux]