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_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
⊢ 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 : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
have rw : (↑π : ℂ) ^ (1 / 2) = (↑(π ^ (1 / 2)) : ℂ)
Tactic: rw [Real.sqrt_eq_rpow, ofReal_cpow Real.pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
rw : (↑π : ℂ) ^ (1 / 2) = (↑(π ^ (1 / 2)) : ℂ)
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
have rw₁ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ (↑(1 / 2) : ℂ)
Tactic: rw [Real.sqrt_eq_rpow, ofReal_cpow Real.pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
rw : (↑π : ℂ) ^ (1 / 2) = (↑(π ^ (1 / 2)) : ℂ)
rw₁ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ (↑(1 / 2) : ℂ)
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
have rw₂ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ ((↑1 : ℂ) / (↑2 : ℂ))
Tactic: rw [Real.sqrt_eq_rpow, ofReal_cpow Real.pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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 : ℂ))
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
have rw₃ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ (1 / (↑2 : ℂ))
Tactic: rw [Real.sqrt_eq_rpow, ofReal_cpow Real.pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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 : ℂ))
⊢ (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
have rw₄ : (↑π : ℂ) ^ (1 / 2) = (↑π : ℂ) ^ HDiv.hDiv (α := ℂ) 1 2
Tactic: rw [Real.sqrt_eq_rpow, ofReal_cpow Real.pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
⊢ HasDerivAt Gammaℝ (-((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2) 1
have aux : (↑π : ℂ) ^ (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]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
⊢ (↑√π : ℂ) ≠ 0
have rw : √π ≠ 0
Tactic: rw [ofReal_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
⊢ HasDerivAt Gammaℝ (-((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2) 1
have aux2 : (↑√π : ℂ) ≠ 0
Tactic: have aux2 : (√π : ℂ) ≠ 0 := by rw [ofReal_ne_zero]; positivity
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
⊢ HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
have this : 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))
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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
have refine : (↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
Tactic: refine this.congr_deriv ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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
⊢ (↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
have rw : (↑π : ℂ) ^ (-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]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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 / (↑√π : ℂ)
⊢ (↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
have rw₁ : (↑π : ℂ) ^ (-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]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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 / (↑√π : ℂ)
⊢ (↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
have rw₂ : (↑π : ℂ) ^ (-1 / 2) * (-log (↑π : ℂ) / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
Tactic: rw [mul_assoc, ← mul_div_assoc, mul_neg_one, neg_div, cpow_neg, ← div_eq_inv_mul, aux]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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 / (↑√π : ℂ)
⊢ (↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
have rw₃ : (↑π : ℂ) ^ (-(1 / 2)) * (-log (↑π : ℂ) / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
Tactic: rw [mul_assoc, ← mul_div_assoc, mul_neg_one, neg_div, cpow_neg, ← div_eq_inv_mul, aux]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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 / (↑√π : ℂ)
⊢ (↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
have rw₄ : ((↑π : ℂ) ^ (1 / 2))⁻¹ * (-log (↑π : ℂ) / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
Tactic: rw [mul_assoc, ← mul_div_assoc, mul_neg_one, neg_div, cpow_neg, ← div_eq_inv_mul, aux]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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 / (↑√π : ℂ)
⊢ (↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
have rw₅ : -log (↑π : ℂ) / 2 / (↑π : ℂ) ^ (1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
Tactic: rw [mul_assoc, ← mul_div_assoc, mul_neg_one, neg_div, cpow_neg, ← div_eq_inv_mul, aux]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
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 / (↑√π : ℂ)
⊢ (↑π : ℂ) ^ (-1 / 2) * log (↑π : ℂ) * (-1 / 2) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
have rw₆ : -log (↑π : ℂ) / 2 / (↑√π : ℂ) = -log (↑π : ℂ) / 2 / (↑√π : ℂ)
Tactic: rw [mul_assoc, ← mul_div_assoc, mul_neg_one, neg_div, cpow_neg, ← div_eq_inv_mul, aux]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
⊢ HasDerivAt Gammaℝ (-((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2) 1
have hf : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
⊢ HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
have refine_2 : ∀ (this : HasDerivAt (𝕜 := ℂ) (Gamma ∘ fun (s : ℂ) ↦ s / 2) (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) * (1 / 2)) 1),
  HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
Tactic: have := hasDerivAt_Gamma_one_half.comp 1 (?_ : HasDerivAt (fun s : ℂ ↦ s / 2) (1 / 2) 1)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
refine_2 :
  ∀ (this : HasDerivAt (𝕜 := ℂ) (Gamma ∘ fun (s : ℂ) ↦ s / 2) (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) * (1 / 2)) 1),
    HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
⊢ HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
have refine_1 : HasDerivAt (fun (s : ℂ) ↦ s / 2) (1 / 2) 1
Tactic: have := hasDerivAt_Gamma_one_half.comp 1 (?_ : HasDerivAt (fun s : ℂ ↦ s / 2) (1 / 2) 1)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
this : HasDerivAt (𝕜 := ℂ) (Gamma ∘ fun (s : ℂ) ↦ s / 2) (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) * (1 / 2)) 1
⊢ HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
have refine_2 : ∀ (this : HasDerivAt (𝕜 := ℂ) (Gamma ∘ fun (s : ℂ) ↦ s / 2) (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1),
  HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
Tactic: rwa [mul_one_div] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
⊢ HasDerivAt Gammaℝ (-((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2) 1
have hg : HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
Tactic: have hg : HasDerivAt g (-√π * (γ + 2 * log 2) / 2) 1 := by
    have := hasDerivAt_Gamma_one_half.comp 1 (?_ : HasDerivAt (fun s : ℂ ↦ s / 2) (1 / 2) 1)
    · rwa [mul_one_div] at this
    · exact (hasDerivAt_id _).div_const _
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
hg : HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
⊢ HasDerivAt Gammaℝ (-((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2) 1
have refine : -log (↑π : ℂ) / 2 / (↑√π : ℂ) * Gamma (1 / 2) + f 1 * (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) =
  -((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2
Tactic: refine HasDerivAt.congr_deriv (hf.mul hg) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
hg : HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
⊢ -log (↑π : ℂ) / 2 / (↑√π : ℂ) * Gamma (1 / 2) + (↑π : ℂ) ^ (-1 / 2) * (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) =
    -((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2
have rw : -((↑γ : ℂ) + log (↑(HPow.hPow (α := ℝ) (β := ℕ) 2 2 * π) : ℂ)) / 2 = -((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2
Tactic: rw [Gamma_one_half_eq, aux, div_mul_cancel₀ _ aux2, neg_div _ (1 : ℂ), cpow_neg, aux,
    mul_div_assoc, ← mul_assoc, mul_neg, inv_mul_cancel₀ aux2, neg_one_mul, ← neg_div,
    ← _root_.add_div, ← neg_add, add_comm, add_assoc, ← ofReal_log Real.pi_pos.le, ← ofReal_ofNat,
    ← ofReal_log zero_le_two,
    ← ofReal_mul, ← Nat.cast_ofNat (R := ℝ), ← Real.log_pow, ← ofReal_add,
    ← Real.log_mul (by positivity) (by positivity),
    Nat.cast_ofNat, ofReal_ofNat, ofReal_log (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (hypothesis)
Goal:
n : ℕ
Hn : n ≠ 0
⊢ LT.lt (α := ℚ) 0 (∑ i ∈ Finset.range n, (↑(i + 1) : ℚ)⁻¹)
have Hn₁ : (Finset.range n).Nonempty
Tactic: rw [← Finset.nonempty_range_iff] at Hn
Cleared hypotheses: Hn
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
⊢ padicValRat 2 (harmonic (n + 1)) = -(↑(Nat.log 2 (n + 1)) : ℤ)
have succ : ∀ (ih : padicValRat 2 (harmonic 0) = -(↑(Nat.log 2 0) : ℤ)),
  padicValRat 2 (harmonic (HAdd.hAdd (α := ℕ) 0 1)) = -(↑(Nat.log 2 (HAdd.hAdd (α := ℕ) 0 1)) : ℤ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n, ih
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
succ :
  ∀ (ih : padicValRat 2 (harmonic 0) = -(↑(Nat.log 2 0) : ℤ)),
    padicValRat 2 (harmonic (HAdd.hAdd (α := ℕ) 0 1)) = -(↑(Nat.log 2 (HAdd.hAdd (α := ℕ) 0 1)) : ℤ)
⊢ padicValRat 2 (harmonic (n + 1)) = -(↑(Nat.log 2 (n + 1)) : ℤ)
have succ₁ : ∀ (hn : n ≠ 0), padicValRat 2 (harmonic (n + 1)) = -(↑(Nat.log 2 (n + 1)) : ℤ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
⊢ padicValRat 2 (harmonic (n + 1)) = -(↑(Nat.log 2 (n + 1)) : ℤ)
have succ : padicValRat 2 (harmonic n + (↑(n + 1) : ℚ)⁻¹) = -(↑(Nat.log 2 (n + 1)) : ℤ)
Tactic: rw [harmonic_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
⊢ padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1) : ℚ)⁻¹
have rw : ¬Nat.log 2 n = padicValNat 2 (n + 1)
Tactic: rw [ih, padicValRat.inv, padicValRat.of_nat, Ne, neg_inj, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (hypothesis)
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
⊢ padicValRat 2 (harmonic n + (↑(n + 1) : ℚ)⁻¹) = -(↑(Nat.log 2 (n + 1)) : ℤ)
have key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1) : ℚ)⁻¹
Tactic: have key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹ := by
      rw [ih, padicValRat.inv, padicValRat.of_nat, Ne, neg_inj, Nat.cast_inj]
      exact Nat.log_ne_padicValNat_succ hn
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1) : ℚ)⁻¹
⊢ padicValRat 2 (harmonic n + (↑(n + 1) : ℚ)⁻¹) = -(↑(Nat.log 2 (n + 1)) : ℤ)
have succ : max (Nat.log 2 n) (padicValNat 2 n.succ) = Nat.log 2 (n + 1)
Tactic: rw [padicValRat.add_eq_min (harmonic_succ n ▸ (harmonic_pos n.succ_ne_zero).ne')
        (harmonic_pos hn).ne' (inv_ne_zero (Nat.cast_ne_zero.mpr n.succ_ne_zero)) key, ih,
        padicValRat.inv, padicValRat.of_nat, min_neg_neg, neg_inj, ← Nat.cast_max, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
⊢ padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
have zero : padicValRat 2 (harmonic 0) = -(↑(Nat.log 2 0) : ℤ)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rcases eq_or_ne n 0 with rfl | hn
    · simp
    rw [harmonic_succ]
    have key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹ := by
      rw [ih, padicValRat.inv, padicValRat.of_nat, Ne, neg_inj, Nat.cast_inj]
      exact Nat.log_ne_padicValNat_succ hn
    rw [padicValRat.add_eq_min (harmonic_succ n ▸ (harmonic_pos n.succ_ne_zero).ne')
        (harmonic_pos hn).ne' (inv_ne_zero (Nat.cast_ne_zero.mpr n.succ_ne_zero)) key, ih,
        padicValRat.inv, padicValRat.of_nat, min_neg_neg, neg_inj, ← Nat.cast_max, Nat.cast_inj]
    exact Nat.max_log_padicValNat_succ_eq_log_succ n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
zero : padicValRat 2 (harmonic 0) = -(↑(Nat.log 2 0) : ℤ)
⊢ padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
have succ : ∀ (n : ℕ) (ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)),
  padicValRat 2 (harmonic (n + 1)) = -(↑(Nat.log 2 (n + 1)) : ℤ)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rcases eq_or_ne n 0 with rfl | hn
    · simp
    rw [harmonic_succ]
    have key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹ := by
      rw [ih, padicValRat.inv, padicValRat.of_nat, Ne, neg_inj, Nat.cast_inj]
      exact Nat.log_ne_padicValNat_succ hn
    rw [padicValRat.add_eq_min (harmonic_succ n ▸ (harmonic_pos n.succ_ne_zero).ne')
        (harmonic_pos hn).ne' (inv_ne_zero (Nat.cast_ne_zero.mpr n.succ_ne_zero)) key, ih,
        padicValRat.inv, padicValRat.of_nat, min_neg_neg, neg_inj, ← Nat.cast_max, Nat.cast_inj]
    exact Nat.max_log_padicValNat_succ_eq_log_succ n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ norm (E := ℚ_[2]) (↑(harmonic n) : ℚ_[2]) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
have rw : (↑(padicNorm 2 (harmonic n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
Tactic: rw [Padic.eq_padicNorm, padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne',
    padicValRat_two_harmonic, neg_neg, zpow_natCast, Rat.cast_pow, Rat.cast_natCast, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : (↑(padicNorm 2 (harmonic n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
⊢ norm (E := ℚ_[2]) (↑(harmonic n) : ℚ_[2]) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
have rw₁ : (↑(HPow.hPow (α := ℚ) (↑2 : ℚ) (-padicValRat 2 (harmonic n))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
Tactic: rw [Padic.eq_padicNorm, padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne',
    padicValRat_two_harmonic, neg_neg, zpow_natCast, Rat.cast_pow, Rat.cast_natCast, Nat.cast_ofNat]