awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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) : ℝ)
⊢ ∀ (n : ℕ) (hn : 0 < n), log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
have derivLB (n : ℕ) (hn : 0 < n) : log n ≤ deriv f (n + 1) := by
    refine (le_of_eq ?_).trans <| hc.slope_le_deriv (mem_Ioi.mpr <| Nat.cast_pos.mpr hn)
      (by positivity : _ < (_ : ℝ)) (by linarith) (hder <| by positivity)
    rw [slope_def_field, show n + 1 - n = (1 : ℝ) by ring, div_one, h_rec n (by positivity),
      add_sub_cancel_left]
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ℕ
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ℕ
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ℕ
linarith :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 →
    -1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 0
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ℕ
refine : slope f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
refine (hc.deriv_le_slope (by positivity : (0 : ℝ) < n + 1) (by positivity : (0 : ℝ) < n + 2)
        (by linarith) (hder <| by positivity)).trans (le_of_eq ?_)

Premises used: ConvexOn.deriv_le_slope, LE.le.trans, le_of_eq
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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)
rw₅ rw₆ : log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ slope f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) = 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]

Premises used: add_sub_cancel_left, Nat.cast, slope_def_field, HAdd.hAdd, OfNat.ofNat, div_one
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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)
⊢ ∀ (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]
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 ≤ γ
a₁ : γ ≤ -deriv f 1
⊢ -deriv f 1 = γ

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ∀ᶠ (c : ℕ) in atTop, -deriv f 1 ≤ (↑(harmonic c) : ℝ) - log (↑c : ℝ)
⊢ -deriv f 1 ≤ γ

Tactic:
apply ge_of_tendsto tendsto_harmonic_sub_log

Premises used: ge_of_tendsto, Real.tendsto_harmonic_sub_log
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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)
h : ∀ (n : ℕ) (hn : 0 < n), -deriv f 1 ≤ (↑(harmonic n) : ℝ) - log (↑n : ℝ)
⊢ ∀ᶠ (c : ℕ) in atTop, -deriv f 1 ≤ (↑(harmonic c) : ℝ) - log (↑c : ℝ)

Tactic:
filter_upwards [eventually_gt_atTop 0] with n hn

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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
h : log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ -deriv f 1 ≤ (↑(harmonic n) : ℝ) - log (↑n : ℝ)

Tactic:
rw [le_sub_iff_add_le', ← sub_eq_add_neg, sub_le_iff_le_add', ← hder_nat]

Premises used: sub_eq_add_neg, le_sub_iff_add_le', sub_le_iff_le_add'
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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
⊢ log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
derivLB n hn
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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
⊢ log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
exact derivLB n hn
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ∀ᶠ (c : ℕ) in atTop, (↑(harmonic c) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑c : ℝ) 1) ≤ -deriv f 1
⊢ γ ≤ -deriv f 1

Tactic:
apply le_of_tendsto tendsto_harmonic_sub_log_add_one

Premises used: le_of_tendsto, Real.tendsto_harmonic_sub_log_add_one
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ∀ (n : ℕ), (↑(harmonic n) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ -deriv f 1
⊢ ∀ᶠ (c : ℕ) in atTop, (↑(harmonic c) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑c : ℝ) 1) ≤ -deriv f 1

Tactic:
filter_upwards with n
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ℕ
a : deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ (↑(harmonic n) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ -deriv f 1

Tactic:
rw [sub_le_iff_le_add', ← sub_eq_add_neg, le_sub_iff_add_le', ← hder_nat]

Premises used: sub_eq_add_neg, le_sub_iff_add_le', sub_le_iff_le_add'
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ℕ
⊢ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
derivUB n
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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 : ℕ
⊢ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
exact derivUB n
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n m : ℕ
linarith :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = -(↑m : ℝ) →
    -1 + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + HSub.hSub (α := ℝ) 0 (↑m : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - -(↑m : ℝ)) = 0
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≠ -(↑m : ℝ)

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
⊢ 1 = HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
rw : γ = -((↑0! : ℝ) * (-γ + (↑(harmonic 0) : ℝ)))
⊢ γ = -deriv Gamma 1

Tactic:
rw [show (1 : ℝ) = ↑(0 : ℕ) + 1 by simp, deriv_Gamma_nat 0]

Premises used: Real.deriv_Gamma_nat, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
⊢ γ = -((↑0! : ℝ) * (-γ + (↑(harmonic 0) : ℝ)))

Tactic:
simp
-- 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, Real.hasDerivAt_Gamma_nat, Nat.cast_one, one_mul, mul_neg
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
⊢ ∀ {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'
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
h_diff : ∀ {s : ℝ} (hs : 0 < s), DifferentiableAt ℝ Gamma s
⊢ ∀ {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 _)
-- 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 Gamma (-√π * (γ + 2 * log 2)) (1 / 2)

Tactic:
(h_diff one_half_pos).hasDerivAt.congr_deriv ?_

Premises used: DifferentiableAt.hasDerivAt, one_half_pos, HasDerivAt.congr_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
refine : deriv Gamma (1 / 2) = -√π * (γ + 2 * log 2)
⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)

Tactic:
refine (h_diff one_half_pos).hasDerivAt.congr_deriv ?_

Premises used: DifferentiableAt.hasDerivAt, one_half_pos, HasDerivAt.congr_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
⊢ 1 / 2 + 1 / 2 = 1

Tactic:
norm_num
-- 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
hc : DifferentiableAt ℝ Gamma (1 / 2)
hd : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (s + 1 / 2)) (1 / 2)
⊢ deriv Gamma (1 / 2) = deriv (fun (s : ℝ) ↦ Gamma 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]

Premises used: add_neg_cancel, deriv_fun_mul, add_assoc, Real.Gamma_one, Real.Gamma_one_half_eq, deriv_comp_add_const, MulZeroClass.mul_zero, Real.eulerMascheroniConstant_eq_neg_deriv, mul_add, mul_one, add_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
hc : 0 < 1 / 2
⊢ DifferentiableAt ℝ Gamma (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
⊢ 0 < 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
⊢ 0 < 1 / 2 + 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 (s + 1 / 2)) (1 / 2)

Tactic:
exact ((h_diff (by simp)).hasDerivAt.comp_add_const).differentiableAt

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.differentiableAt, HasDerivAt.comp_add_const
-- 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 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) + √π * γ
⊢ 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) + √π * γ

Tactic:
rw [funext Gamma_mul_Gamma_add_half]

Premises used: Real.Gamma_mul_Gamma_add_half, funext
-- 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
hc : DifferentiableAt ℝ (F := ℝ) (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) + √π * γ =
    √π * (deriv (fun (s : ℝ) ↦ Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2) + γ)

Tactic:
rw [mul_comm √π, mul_comm √π, deriv_mul_const, add_mul]

Premises used: add_mul, deriv_mul_const, Real.pi, mul_comm, Real.sqrt
-- 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
hc : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s)) (1 / 2)
hc₁ : DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)

Tactic:
apply DifferentiableAt.mul

Premises used: DifferentiableAt.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
hs : 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
⊢ 0 < 2 * (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:
exact .comp (g := Gamma) _ (by apply h_diff; simp) -- s = 1
        (differentiableAt_id.const_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
⊢ DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ 1 - 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
⊢ DifferentiableAt ℝ (F := ℝ) (fun (s : ℝ) ↦ HPow.hPow (α := ℝ) 2 (1 - 2 * s)) (1 / 2)

Tactic:
exact (differentiableAt_const _).rpow (by fun_prop) two_ne_zero

Premises used: two_ne_zero, DifferentiableAt.rpow, differentiableAt_const