-- 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
rwa₈ :
  ∀
    (this :
      HasDerivAt ((fun (s : ℂ) ↦ 2 * (2 * (↑π : ℂ)) ^ (-s)) * Gamma) ((-log (2 * (↑π : ℂ)) + -(↑γ : ℂ)) / (↑π : ℂ)) 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