awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n_1 : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
n : ℕ
rw :
  (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) /
      (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw₁ : (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / 1 = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ slope f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw₂ : f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [slope_def_field, show n + 2 - (n + 1) = (1 : ℝ) by ring, div_one,
      show n + 2 = (n + 1) + (1 : ℝ) by ring, h_rec (n + 1) (by positivity), add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n_1 : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
n : ℕ
rw :
  (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) /
      (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw₁ : (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / 1 = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw₂ : f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ slope f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw₃ : f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [slope_def_field, show n + 2 - (n + 1) = (1 : ℝ) by ring, div_one,
      show n + 2 = (n + 1) + (1 : ℝ) by ring, h_rec (n + 1) (by positivity), add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n_1 : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
n : ℕ
rw :
  (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) /
      (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw₁ : (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / 1 = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw₂ : f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw₃ : f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ slope f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw₄ : f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
  log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [slope_def_field, show n + 2 - (n + 1) = (1 : ℝ) by ring, div_one,
      show n + 2 = (n + 1) + (1 : ℝ) by ring, h_rec (n + 1) (by positivity), add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n_1 : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
n : ℕ
rw :
  (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) /
      (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw₁ : (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / 1 = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw₂ : f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw₃ : f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw₄ :
  f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ slope f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw₅ : log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [slope_def_field, show n + 2 - (n + 1) = (1 : ℝ) by ring, div_one,
      show n + 2 = (n + 1) + (1 : ℝ) by ring, h_rec (n + 1) (by positivity), add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ -deriv f 1 = γ
have derivUB : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: have derivUB (n : ℕ) : deriv f (n + 1) ≤ log (n + 1) := by
    refine (hc.deriv_le_slope (by positivity : (0 : ℝ) < n + 1) (by positivity : (0 : ℝ) < n + 2)
        (by linarith) (hder <| by positivity)).trans (le_of_eq ?_)
    rw [slope_def_field, show n + 2 - (n + 1) = (1 : ℝ) by ring, div_one,
      show n + 2 = (n + 1) + (1 : ℝ) by ring, h_rec (n + 1) (by positivity), add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
derivUB : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ -deriv f 1 = γ
have a : -deriv f 1 ≤ γ
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
derivUB : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
a : -deriv f 1 ≤ γ
⊢ -deriv f 1 = γ
have a₁ : γ ≤ -deriv f 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
derivUB : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ -deriv f 1 ≤ γ
have a : ∀ᶠ (c : ℕ) in atTop, -deriv f 1 ≤ (↑(harmonic c) : ℝ) - log (↑c : ℝ)
Tactic: apply ge_of_tendsto tendsto_harmonic_sub_log
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
derivUB : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ ∀ᶠ (c : ℕ) in atTop, -deriv f 1 ≤ (↑(harmonic c) : ℝ) - log (↑c : ℝ)
have h : ∀ (n : ℕ) (hn : 0 < n), -deriv f 1 ≤ (↑(harmonic n) : ℝ) - log (↑n : ℝ)
Tactic: filter_upwards [eventually_gt_atTop 0] with n hn
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n_1 : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
derivUB : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
n : ℕ
hn : 0 < n
⊢ -deriv f 1 ≤ (↑(harmonic n) : ℝ) - log (↑n : ℝ)
have h : log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [le_sub_iff_add_le', ← sub_eq_add_neg, sub_le_iff_le_add', ← hder_nat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
derivUB : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ γ ≤ -deriv f 1
have a : ∀ᶠ (c : ℕ) in atTop, (↑(harmonic c) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑c : ℝ) 1) ≤ -deriv f 1
Tactic: apply le_of_tendsto tendsto_harmonic_sub_log_add_one
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
derivUB : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ ∀ᶠ (c : ℕ) in atTop, (↑(harmonic c) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑c : ℝ) 1) ≤ -deriv f 1
have a : ∀ (n : ℕ), (↑(harmonic n) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ -deriv f 1
Tactic: filter_upwards with n
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n_1 : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
derivLB : ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
derivUB : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
n : ℕ
⊢ (↑(harmonic n) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ -deriv f 1
have a : deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [sub_le_iff_le_add', ← sub_eq_add_neg, le_sub_iff_add_le', ← hder_nat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n m : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≠ -(↑m : ℝ)
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = -(↑m : ℝ) →
  -1 + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + HSub.hSub (α := ℝ) 0 (↑m : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - -(↑m : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
⊢ γ = -deriv Gamma 1
have rw : γ = -((↑0! : ℝ) * (-γ + (↑(harmonic 0) : ℝ)))
Tactic: rw [show (1 : ℝ) = ↑(0 : ℕ) + 1 by simp, deriv_Gamma_nat 0]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)
have h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
Tactic: have h_diff {s : ℝ} (hs : 0 < s) : DifferentiableAt ℝ Gamma s :=
    differentiableAt_Gamma fun m ↦ ((neg_nonpos.mpr m.cast_nonneg).trans_lt hs).ne'
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)
have h_diff' : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) s
Tactic: have h_diff' {s : ℝ} (hs : 0 < s) : DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s :=
    .comp (g := Gamma) _ (h_diff <| mul_pos two_pos hs) (differentiableAt_id.const_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
⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)
have refine : deriv Gamma (1 / 2) = -√π * (γ + 2 * log 2)
Tactic: refine (h_diff one_half_pos).hasDerivAt.congr_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
⊢ deriv Gamma (1 / 2) = deriv (fun (s : ℝ) ↦ Gamma s * Gamma (s + 1 / 2)) (1 / 2) + √π * γ
have hc : DifferentiableAt ℝ Gamma (1 / 2)
Tactic: 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]
-- 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
hc : DifferentiableAt ℝ Gamma (1 / 2)
⊢ deriv Gamma (1 / 2) = deriv (fun (s : ℝ) ↦ Gamma s * Gamma (s + 1 / 2)) (1 / 2) + √π * γ
have hd : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (s + 1 / 2)) (1 / 2)
Tactic: 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]
-- 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 (1 / 2)
have hc : 0 < 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
⊢ 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) + √π * γ
have rw : deriv (fun (x : ℝ) ↦ Gamma (2 * x) * HPow.hPow (α := ℝ) 2 (1 - 2 * x) * √π) (1 / 2) + √π * γ =
  deriv (fun (s : ℝ) ↦ Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s) * √π) (1 / 2) + √π * γ
Tactic: rw [funext Gamma_mul_Gamma_add_half]
-- 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 : ℝ) ↦ 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) + γ)
have hc : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)
Tactic: rw [mul_comm √π, mul_comm √π, deriv_mul_const, add_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 ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)
have hc : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2)
Tactic: apply DifferentiableAt.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
hc : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)
have hc₁ : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)
Tactic: apply DifferentiableAt.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 hs : 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
⊢ √π * (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)) +
        γ)
have 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)) +
      γ)
Tactic: rw [deriv_fun_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
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)) +
        γ)
⊢ √π * (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)) +
        γ)
have hc : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2)
Tactic: rw [deriv_fun_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
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)
⊢ √π * (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)) +
        γ)
have hd : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)
Tactic: rw [deriv_fun_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
⊢ √π *
      (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) + γ)
have e_a : deriv (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2) = -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 (Gamma ∘ fun (s : ℝ) ↦ 2 * s) (1 / 2) = -2 * γ
have e_a : deriv Gamma 1 * 2 = -2 * γ
Tactic: rw [deriv_comp, deriv_const_mul_id, mul_one_div, div_self two_ne_zero]
-- 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 : deriv Gamma 1 * 2 = -2 * γ
⊢ deriv (Gamma ∘ fun (s : ℝ) ↦ 2 * s) (1 / 2) = -2 * γ
have e_a₁ : DifferentiableAt ℝ Gamma (2 * (1 / 2))
Tactic: rw [deriv_comp, deriv_const_mul_id, mul_one_div, div_self two_ne_zero]
-- 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 : deriv Gamma 1 * 2 = -2 * γ
e_a₁ : DifferentiableAt ℝ Gamma (2 * (1 / 2))
⊢ deriv (Gamma ∘ fun (s : ℝ) ↦ 2 * s) (1 / 2) = -2 * γ
have e_a₂ : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ 2 * s) (1 / 2)
Tactic: rw [deriv_comp, deriv_const_mul_id, mul_one_div, div_self two_ne_zero]
-- 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 * γ
have e_a : 2 * deriv Gamma 1 = -2 * γ
Tactic: rw [mul_comm, hasDerivAt_Gamma_one.deriv, mul_neg, neg_mul]