awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 * (↑π : ℂ)) / (↑π : ℂ)
rw₂ : -(2 * ((2 * (↑π : ℂ))⁻¹ * log (2 * (↑π : ℂ)))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
⊢ 2 * (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
have rw₃ : -(2 * (log (2 * (↑π : ℂ)) / (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 * (↑π : ℂ)) / (↑π : ℂ)
rw₂ : -(2 * ((2 * (↑π : ℂ))⁻¹ * log (2 * (↑π : ℂ)))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
rw₃ : -(2 * (log (2 * (↑π : ℂ)) / (2 * (↑π : ℂ)))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
⊢ 2 * (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
have rw₄ : -(2 * log (2 * (↑π : ℂ)) / (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 * (↑π : ℂ)) / (↑π : ℂ)
rw₂ : -(2 * ((2 * (↑π : ℂ))⁻¹ * log (2 * (↑π : ℂ)))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
rw₃ : -(2 * (log (2 * (↑π : ℂ)) / (2 * (↑π : ℂ)))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
rw₄ : -(2 * log (2 * (↑π : ℂ)) / (2 * (↑π : ℂ))) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
⊢ 2 * (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
have rw₅ : -(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 * (↑π : ℂ)) / (↑π : ℂ)
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 * (↑π : ℂ)) / (↑π : ℂ)
⊢ 2 * (HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * log (2 * (↑π : ℂ)) * -1) = -log (2 * (↑π : ℂ)) / (↑π : ℂ)
have rw₆ : -(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 (hypothesis)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
⊢ HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
have this : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this : HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
⊢ HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
have this₁ : HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
  (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * Gamma 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1
Tactic: have := this.mul hasDerivAt_Gamma_one
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this_1 : HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
this :
  HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
    (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * Gamma 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1
⊢ HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
have rwa : ∀
  (this :
    HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
      (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
  HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
Tactic: rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
    mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this_1 : HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
this :
  HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
    (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * Gamma 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1
rwa :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
⊢ HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
have rwa₁ : ∀
  (this :
    HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
      (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
  HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
Tactic: rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
    mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this_1 : HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
this :
  HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
    (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * Gamma 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1
rwa :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₁ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
⊢ HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
have rwa₂ : ∀
  (this :
    HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
      (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * (2 * (↑π : ℂ))⁻¹ * -(↑γ : ℂ)) 1),
  HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
Tactic: rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
    mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this_1 : HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
this :
  HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
    (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * Gamma 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1
rwa :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₁ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₂ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * (2 * (↑π : ℂ))⁻¹ * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
⊢ HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
have rwa₃ : ∀
  (this :
    HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
      (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 / (2 * (↑π : ℂ)) * -(↑γ : ℂ)) 1),
  HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
Tactic: rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
    mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this_1 : HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
this :
  HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
    (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * Gamma 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1
rwa :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₁ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₂ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * (2 * (↑π : ℂ))⁻¹ * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₃ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 / (2 * (↑π : ℂ)) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
⊢ HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
have rwa₄ : ∀
  (this :
    HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
      (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 / 2 / (↑π : ℂ) * -(↑γ : ℂ)) 1),
  HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
Tactic: rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
    mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this_1 : HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
this :
  HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
    (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * Gamma 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1
rwa :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₁ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₂ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * (2 * (↑π : ℂ))⁻¹ * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₃ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 / (2 * (↑π : ℂ)) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₄ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 / 2 / (↑π : ℂ) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
⊢ HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
have rwa₅ : ∀
  (this :
    HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
      (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 1 / (↑π : ℂ) * -(↑γ : ℂ)) 1),
  HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
Tactic: rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
    mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this_1 : HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
this :
  HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
    (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * Gamma 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1
rwa :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₁ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₂ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * (2 * (↑π : ℂ))⁻¹ * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₃ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 / (2 * (↑π : ℂ)) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₄ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 / 2 / (↑π : ℂ) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₅ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 1 / (↑π : ℂ) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
⊢ HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
have rwa₆ : ∀
  (this :
    HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
      (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + -(↑γ : ℂ) * (1 / (↑π : ℂ))) 1),
  HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
Tactic: rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
    mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this_1 : HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
this :
  HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
    (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * Gamma 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1
rwa :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₁ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₂ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * (2 * (↑π : ℂ))⁻¹ * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₃ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 / (2 * (↑π : ℂ)) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₄ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 / 2 / (↑π : ℂ) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₅ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 1 / (↑π : ℂ) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₆ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + -(↑γ : ℂ) * (1 / (↑π : ℂ))) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
⊢ HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
have rwa₇ : ∀
  (this :
    HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
      (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + -(↑γ : ℂ) / (↑π : ℂ)) 1),
  HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
Tactic: rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
    mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)
this_1 : HasDerivAt (fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) (-log (2 * (↑π : ℂ)) / (↑π : ℂ)) 1
this :
  HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
    (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * Gamma 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1
rwa :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) * 1 + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₁ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * HPow.hPow (β := ℂ) (2 * (↑π : ℂ)) (-1) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₂ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 * (2 * (↑π : ℂ))⁻¹ * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₃ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 / (2 * (↑π : ℂ)) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₄ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 2 / 2 / (↑π : ℂ) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₅ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + 1 / (↑π : ℂ) * -(↑γ : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₆ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + -(↑γ : ℂ) * (1 / (↑π : ℂ))) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
rwa₇ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma)
        (-log (2 * (↑π : ℂ)) / (↑π : ℂ) + -(↑γ : ℂ) / (↑π : ℂ)) 1),
    HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
⊢ HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
have rwa₈ : ∀
  (this :
    HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma) ((-log (2 * (↑π : ℂ)) + -(↑γ : ℂ)) / (↑π : ℂ)) 1),
  HasDerivAt Gammaℂ (-((↑γ : ℂ) + log (2 * (↑π : ℂ))) / (↑π : ℂ)) 1
Tactic: rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
    mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this
Cleared hypotheses: this