awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
rwa :
  ∀ (this : deriv (fun (x : ℝ) ↦ log (Gamma x)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
rwa₁ :
  ∀
    (this :
      deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
rwa₂ :
  ∀ (this : deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / (↑n ! : ℝ) = -γ + (↑(harmonic n) : ℝ)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
rwa₃ :
  ∀ (this : (-γ + (↑(harmonic n) : ℝ)) * (↑n ! : ℝ) = deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
rwa₄ :
  ∀ (this : (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ)) = deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
    deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
⊢ deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
have rwa₅ : ∀ (this : deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))),
  deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
Tactic: rwa [Function.comp_def, deriv.log (differentiableAt_Gamma (fun m ↦ by linarith))
      (by positivity), Gamma_nat_eq_factorial, div_eq_iff_mul_eq (by positivity),
      mul_comm, Eq.comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (goal)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
⊢ deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))
have suffices : deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
Tactic: suffices deriv (log ∘ Gamma) (n + 1) = -γ + harmonic n by
    rwa [Function.comp_def, deriv.log (differentiableAt_Gamma (fun m ↦ by linarith))
      (by positivity), Gamma_nat_eq_factorial, div_eq_iff_mul_eq (by positivity),
      mul_comm, Eq.comm] at this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
⊢ deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
have hc : ConvexOn ℝ (Ioi 0) f
Tactic: have hc : ConvexOn ℝ (Ioi 0) f := convexOn_log_Gamma
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.GammaDeriv (hypothesis)
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
⊢ deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
have h_rec : ∀ (x : ℝ) (hx : 0 < x), f (x + 1) = f x + log x
Tactic: have h_rec (x : ℝ) (hx : 0 < x) : f (x + 1) = f x + log x := by simp only [f, Function.comp_apply,
      Gamma_add_one hx.ne', log_mul hx.ne' (Gamma_pos_of_pos hx).ne', add_comm]
-- 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
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ f x
have refine_1 : ∀ (m : ℕ), x ≠ -(↑m : ℝ)
Tactic: refine ((differentiableAt_Gamma ?_).log (Gamma_ne_zero ?_))
-- 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
x : ℝ
hx : 0 < x
m : ℕ
⊢ -(↑m : ℝ) < x
have linarith : x ≤ -(↑m : ℝ) → HSub.hSub (α := ℝ) 0 (↑m : ℝ) + (0 - x) + (x - -(↑m : ℝ)) = 0
Tactic: linarith
-- 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
⊢ deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
have hder : ∀ {x : ℝ} (hx : 0 < x), DifferentiableAt ℝ f x
Tactic: have hder {x : ℝ} (hx : 0 < x) : DifferentiableAt ℝ f x := by
    refine ((differentiableAt_Gamma ?_).log (Gamma_ne_zero ?_)) <;>
    exact fun m ↦ ne_of_gt (by linarith)
-- 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
x : ℝ
hx : 0 < x
⊢ deriv f (x + 1) = deriv f x + 1 / x
have rw : deriv (fun (x : ℝ) ↦ f (x + 1)) x = deriv (f + log) x
Tactic: rw [← deriv_comp_add_const, one_div, ← deriv_log,
      ← deriv_add (hder <| by positivity) (differentiableAt_log hx.ne')]
-- 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
x : ℝ
hx : 0 < x
⊢ deriv (fun (x : ℝ) ↦ f (x + 1)) x = deriv (f + log) x
have hL : (fun (x : ℝ) ↦ f (x + 1)) =ᶠ[𝓝 x] f + log
Tactic: apply EventuallyEq.deriv_eq
-- 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
x : ℝ
hx : 0 < x
⊢ (fun (x : ℝ) ↦ f (x + 1)) =ᶠ[𝓝 x] f + log
have h : ∀ (a : ℝ),
  Membership.mem («γ» := Set ℝ)
    {x : ℝ |
      Membership.mem («γ» := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
        Membership.mem («γ» := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ (fun (x : ℝ) ↦ f (x + 1)) x = (f + log) x) x} x}
    a
Tactic: filter_upwards [eventually_gt_nhds hx] using h_rec
-- 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
x : ℝ
hx : 0 < x
h :
  ∀ (a : ℝ),
    Membership.mem («γ» := Set ℝ)
      {x : ℝ |
        Membership.mem («γ» := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
          Membership.mem («γ» := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ (fun (x : ℝ) ↦ f (x + 1)) x = (f + log) x) x} x}
      a
⊢ (fun (x : ℝ) ↦ f (x + 1)) =ᶠ[𝓝 x] f + log
have h₁ : ∀ (a : ℝ), 0 < a → f (a + 1) = (f + log) a
Tactic: filter_upwards [eventually_gt_nhds hx] using h_rec
-- 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
⊢ deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
have hder_rec : ∀ (x : ℝ) (hx : 0 < x), deriv f (x + 1) = deriv f x + 1 / x
Tactic: have hder_rec (x : ℝ) (hx : 0 < x) : deriv f (x + 1) = deriv f x + 1 / x := by
    rw [← deriv_comp_add_const, one_div, ← deriv_log,
      ← deriv_add (hder <| by positivity) (differentiableAt_log hx.ne')]
    apply EventuallyEq.deriv_eq
    filter_upwards [eventually_gt_nhds hx] using h_rec
-- 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
n : ℕ
hn : deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
⊢ deriv f (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) = deriv f 1 + (↑(harmonic (n + 1)) : ℝ)
have succ : deriv f 1 + (↑(harmonic n) : ℝ) + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = deriv f 1 + (↑(harmonic n + (↑(n + 1) : ℚ)⁻¹) : ℝ)
Tactic: rw [cast_succ, hder_rec (n + 1) (by positivity), hn, harmonic_succ]
-- 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
n : ℕ
hn : deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
⊢ deriv f 1 + (↑(harmonic n) : ℝ) + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    deriv f 1 + (↑(harmonic n + (↑(n + 1) : ℚ)⁻¹) : ℝ)
have succ : deriv f 1 + (↑(harmonic n) : ℝ) + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
  deriv f 1 + ((↑(harmonic n) : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹)
Tactic: push_cast
-- 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
n : ℕ
⊢ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
have zero : deriv f (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) = deriv f 1 + (↑(harmonic 0) : ℝ)
Tactic: induction n with
    | zero => simp
    | succ n hn =>
      rw [cast_succ, hder_rec (n + 1) (by positivity), hn, harmonic_succ]
      push_cast
      ring
Cleared hypotheses: 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
n : ℕ
zero : deriv f (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) = deriv f 1 + (↑(harmonic 0) : ℝ)
⊢ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
have succ : ∀ (n : ℕ) (hn : deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)),
  deriv f (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) = deriv f 1 + (↑(harmonic (n + 1)) : ℝ)
Tactic: induction n with
    | zero => simp
    | succ n hn =>
      rw [cast_succ, hder_rec (n + 1) (by positivity), hn, harmonic_succ]
      push_cast
      ring
Cleared hypotheses: n
-- 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
⊢ deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
have hder_nat : ∀ (n : ℕ), deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
Tactic: have hder_nat (n : ℕ) : deriv f (n + 1) = deriv f 1 + harmonic n := by
    induction n with
    | zero => simp
    | succ n hn =>
      rw [cast_succ, hder_rec (n + 1) (by positivity), hn, harmonic_succ]
      push_cast
      ring
-- 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) : ℝ)
this : -deriv f 1 = γ
⊢ deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
have rw : deriv f 1 + (↑(harmonic n) : ℝ) = -γ + (↑(harmonic n) : ℝ)
Tactic: rw [hder_nat n, ← this, neg_neg]
-- 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) : ℝ)
this : -deriv f 1 = γ
rw : deriv f 1 + (↑(harmonic n) : ℝ) = -γ + (↑(harmonic n) : ℝ)
⊢ deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
have rw₁ : deriv f 1 + (↑(harmonic n) : ℝ) = - -deriv f 1 + (↑(harmonic n) : ℝ)
Tactic: rw [hder_nat n, ← this, neg_neg]
-- 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) : ℝ)
this : -deriv f 1 = γ
rw : deriv f 1 + (↑(harmonic n) : ℝ) = -γ + (↑(harmonic n) : ℝ)
rw₁ : deriv f 1 + (↑(harmonic n) : ℝ) = - -deriv f 1 + (↑(harmonic n) : ℝ)
⊢ deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
have rw₂ : deriv f 1 + (↑(harmonic n) : ℝ) = deriv f 1 + (↑(harmonic n) : ℝ)
Tactic: rw [hder_nat n, ← this, neg_neg]
-- 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) : ℝ)
⊢ deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
have suffices : -deriv f 1 = γ
Tactic: suffices -deriv f 1 = γ by rw [hder_nat n, ← this, neg_neg]
-- 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) : ℝ)
n : ℕ
hn : 0 < n
⊢ (↑n : ℝ) < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ (↑n : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ)) = 0
Tactic: linarith
-- 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) : ℝ)
n : ℕ
hn : 0 < n
⊢ log (↑n : ℝ) ≤ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have refine : log (↑n : ℝ) = slope f (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: refine (le_of_eq ?_).trans <| hc.slope_le_deriv (mem_Ioi.mpr <| Nat.cast_pos.mpr hn)
      (by positivity : _ < (_ : ℝ)) (by linarith) (hder <| by positivity)
-- 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) : ℝ)
n : ℕ
hn : 0 < n
⊢ log (↑n : ℝ) = slope f (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw : log (↑n : ℝ) = (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ))
Tactic: rw [slope_def_field, show n + 1 - n = (1 : ℝ) by ring, div_one, h_rec n (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) : ℝ)
n : ℕ
hn : 0 < n
rw : log (↑n : ℝ) = (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ))
⊢ log (↑n : ℝ) = slope f (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw₁ : log (↑n : ℝ) = (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)) / 1
Tactic: rw [slope_def_field, show n + 1 - n = (1 : ℝ) by ring, div_one, h_rec n (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) : ℝ)
n : ℕ
hn : 0 < n
rw : log (↑n : ℝ) = (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ))
rw₁ : log (↑n : ℝ) = (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)) / 1
⊢ log (↑n : ℝ) = slope f (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw₂ : log (↑n : ℝ) = f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)
Tactic: rw [slope_def_field, show n + 1 - n = (1 : ℝ) by ring, div_one, h_rec n (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) : ℝ)
n : ℕ
hn : 0 < n
rw : log (↑n : ℝ) = (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ))
rw₁ : log (↑n : ℝ) = (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)) / 1
rw₂ : log (↑n : ℝ) = f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)
⊢ log (↑n : ℝ) = slope f (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw₃ : log (↑n : ℝ) = f (↑n : ℝ) + log (↑n : ℝ) - f (↑n : ℝ)
Tactic: rw [slope_def_field, show n + 1 - n = (1 : ℝ) by ring, div_one, h_rec n (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) : ℝ)
n : ℕ
hn : 0 < n
rw : log (↑n : ℝ) = (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ))
rw₁ : log (↑n : ℝ) = (f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)) / 1
rw₂ : log (↑n : ℝ) = f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - f (↑n : ℝ)
rw₃ : log (↑n : ℝ) = f (↑n : ℝ) + log (↑n : ℝ) - f (↑n : ℝ)
⊢ log (↑n : ℝ) = slope f (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw₄ : log (↑n : ℝ) = log (↑n : ℝ)
Tactic: rw [slope_def_field, show n + 1 - n = (1 : ℝ) by ring, div_one, h_rec n (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) : ℝ)
⊢ -deriv f 1 = γ
have derivLB : ∀ (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]
-- 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 : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 →
  -1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = 0
Tactic: linarith
-- 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 : ℕ
⊢ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have refine : slope f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2) = 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 ?_)
-- 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 : ℕ
⊢ 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)) /
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 - 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)
⊢ 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)) / 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]