awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + 1) - log x) atTop (𝓝 0)
h :
  ∀ (n : ℕ) (hn : n ≠ 0),
    ((fun (x : ℝ) ↦ log (x + 1) - log x) ∘ Nat.cast) n = eulerMascheroniSeq' n - eulerMascheroniSeq n
⊢ EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ log (x + 1) - log x) ∘ Nat.cast) fun (n : ℕ) ↦
    eulerMascheroniSeq' n - eulerMascheroniSeq n

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + 1) - log x) atTop (𝓝 0)
n : ℕ
hn : n ≠ 0
⊢ ((fun (x : ℝ) ↦ log (x + 1) - log x) ∘ Nat.cast) n = eulerMascheroniSeq' n - eulerMascheroniSeq n

Tactic:
simp [eulerMascheroniSeq, eulerMascheroniSeq', eq_false_intro hn]

Premises used: Real.eulerMascheroniSeq, Real.eulerMascheroniSeq', eq_false_intro
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
suffices : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + 1) - log x) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)

Tactic:
suffices Tendsto (fun x : ℝ ↦ log (x + 1) - log x) atTop (𝓝 0) by
    apply (this.comp tendsto_natCast_atTop_atTop).congr'
    filter_upwards [eventually_ne_atTop 0] with n hn
    simp [eulerMascheroniSeq, eulerMascheroniSeq', eq_false_intro hn]
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + 1) - log x) atTop (𝓝 0)

Tactic:
tendsto_log_comp_add_sub_log 1

Premises used: Real.tendsto_log_comp_add_sub_log, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log (x + 1) - log x) atTop (𝓝 0)

Tactic:
exact tendsto_log_comp_add_sub_log 1

Premises used: Real.tendsto_log_comp_add_sub_log, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
apply : eulerMascheroniSeq' =ᶠ[atTop] fun (n : ℕ) ↦ (↑(harmonic n) : ℝ) - log (↑n : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(harmonic n) : ℝ) - log (↑n : ℝ)) atTop (𝓝 eulerMascheroniConstant)

Tactic:
apply tendsto_eulerMascheroniSeq'.congr'

Premises used: Real.tendsto_eulerMascheroniSeq', Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
h : ∀ (n : ℕ) (hn : n ≠ 0), eulerMascheroniSeq' n = (↑(harmonic n) : ℝ) - log (↑n : ℝ)
⊢ eulerMascheroniSeq' =ᶠ[atTop] fun (n : ℕ) ↦ (↑(harmonic n) : ℝ) - log (↑n : ℝ)

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
hn : n ≠ 0
h : (if n = 0 then 2 else (↑(harmonic n) : ℝ) - log (↑n : ℝ)) = (↑(harmonic n) : ℝ) - log (↑n : ℝ)
h₁ : (if False then 2 else (↑(harmonic n) : ℝ) - log (↑n : ℝ)) = (↑(harmonic n) : ℝ) - log (↑n : ℝ)
⊢ eulerMascheroniSeq' n = (↑(harmonic n) : ℝ) - log (↑n : ℝ)

Tactic:
simp_rw [eulerMascheroniSeq', hn, if_false]

Premises used: if_false, Real.eulerMascheroniSeq'
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
⊢ eulerMascheroniSeq n < eulerMascheroniConstant

Tactic:
(strictMono_eulerMascheroniSeq (Nat.lt_succ_self n)).trans_le ?_

Premises used: Real.strictMono_eulerMascheroniSeq, Nat.lt_succ_self, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
refine : eulerMascheroniSeq n.succ ≤ eulerMascheroniConstant
⊢ eulerMascheroniSeq n < eulerMascheroniConstant

Tactic:
refine (strictMono_eulerMascheroniSeq (Nat.lt_succ_self n)).trans_le ?_

Premises used: Real.strictMono_eulerMascheroniSeq, Nat.lt_succ_self, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
⊢ eulerMascheroniSeq n.succ ≤ eulerMascheroniConstant

Tactic:
apply strictMono_eulerMascheroniSeq.monotone.ge_of_tendsto tendsto_eulerMascheroniSeq

Premises used: StrictMono.monotone, Monotone.ge_of_tendsto, Real.strictMono_eulerMascheroniSeq, Real.tendsto_eulerMascheroniSeq
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
⊢ eulerMascheroniConstant < eulerMascheroniSeq' n

Tactic:
lt_of_le_of_lt ?_ (strictAnti_eulerMascheroniSeq' (Nat.lt_succ_self n))

Premises used: lt_of_le_of_lt, Nat.lt_succ_self, Real.strictAnti_eulerMascheroniSeq'
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
refine : eulerMascheroniConstant ≤ eulerMascheroniSeq' n.succ
⊢ eulerMascheroniConstant < eulerMascheroniSeq' n

Tactic:
refine lt_of_le_of_lt ?_ (strictAnti_eulerMascheroniSeq' (Nat.lt_succ_self n))

Premises used: lt_of_le_of_lt, Nat.lt_succ_self, Real.strictAnti_eulerMascheroniSeq'
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
n : ℕ
⊢ eulerMascheroniConstant ≤ eulerMascheroniSeq' n.succ

Tactic:
apply strictAnti_eulerMascheroniSeq'.antitone.le_of_tendsto tendsto_eulerMascheroniSeq'

Premises used: Real.tendsto_eulerMascheroniSeq', Real.strictAnti_eulerMascheroniSeq', Antitone.le_of_tendsto, StrictAnti.antitone
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ 1 / 2 < eulerMascheroniConstant

Tactic:
one_half_lt_eulerMascheroniSeq_six.trans (eulerMascheroniSeq_lt_eulerMascheroniConstant _)

Premises used: Real.one_half_lt_eulerMascheroniSeq_six, LT.lt.trans, Real.eulerMascheroniSeq_lt_eulerMascheroniConstant
-- Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni
Goal:
⊢ eulerMascheroniConstant < 2 / 3

Tactic:
(eulerMascheroniConstant_lt_eulerMascheroniSeq' _).trans eulerMascheroniSeq'_six_lt_two_thirds

Premises used: Real.eulerMascheroniConstant_lt_eulerMascheroniSeq', Real.eulerMascheroniSeq'_six_lt_two_thirds, LT.lt.trans
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (fun (x : ℝ) ↦ log (Gamma x)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic 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:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (fun (x : ℝ) ↦ log (Gamma x)) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) / (↑n ! : ℝ) = -γ + (↑(harmonic n) : ℝ)
⊢ Ne (α := ℝ) (↑n ! : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
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) : ℝ))
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (this : deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(harmonic n) : ℝ))),
    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

Premises used: deriv.log, div_eq_iff_mul_eq, Real.differentiableAt_Gamma, Function.comp_def, Eq.comm, mul_comm, Real.Gamma_nat_eq_factorial
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
suffices : deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)
⊢ deriv Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ) * (-γ + (↑(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
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
⊢ ConvexOn ℝ (Ioi 0) f

Tactic:
have hc : ConvexOn ℝ (Ioi 0) f := convexOn_log_Gamma
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
x : ℝ
hx : 0 < x
⊢ f (x + 1) = f x + log x

Tactic:
simp only [f, Function.comp_apply,
      Gamma_add_one hx.ne', log_mul hx.ne' (Gamma_pos_of_pos hx).ne', add_comm]

Premises used: Real.Gamma_pos_of_pos, Real.Gamma_add_one, add_comm, LT.lt.ne', Function.comp_apply, Real.log_mul
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
⊢ ∀ (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]
-- 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
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ f x

Tactic:
((differentiableAt_Gamma ?_).log (Gamma_ne_zero ?_))

Premises used: Real.Gamma_ne_zero, DifferentiableAt.log, Real.differentiableAt_Gamma, Real.log, dite
-- 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
x : ℝ
hx : 0 < x
refine_1 refine_2 : ∀ (m : ℕ), x ≠ -(↑m : ℝ)
⊢ DifferentiableAt ℝ f x

Tactic:
refine ((differentiableAt_Gamma ?_).log (Gamma_ne_zero ?_))

Premises used: Real.Gamma_ne_zero, DifferentiableAt.log, Real.differentiableAt_Gamma
-- 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
x : ℝ
hx : 0 < x
m : ℕ
linarith : x ≤ -(↑m : ℝ) → HSub.hSub (α := ℝ) 0 (↑m : ℝ) + (0 - x) + (x - -(↑m : ℝ)) = 0
⊢ -(↑m : ℝ) < x

Tactic:
linarith
-- 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
x : ℝ
hx : 0 < x
⊢ ∀ (m : ℕ), x ≠ -(↑m : ℝ)

Tactic:
exact fun m ↦ ne_of_gt (by linarith)
-- 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
⊢ ∀ {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)
-- 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
x : ℝ
hx : 0 < x
⊢ 0 < x

Tactic:
positivity
-- 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
x : ℝ
hx : 0 < x
rw : deriv (fun (x : ℝ) ↦ f (x + 1)) x = deriv (f + log) x
⊢ deriv f (x + 1) = deriv f x + 1 / x

Tactic:
rw [← deriv_comp_add_const, one_div, ← deriv_log,
      ← deriv_add (hder <| by positivity) (differentiableAt_log hx.ne')]

Premises used: Real.deriv_log, deriv_comp_add_const, Real.differentiableAt_log, LT.lt.ne', one_div, deriv_add
-- 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
x : ℝ
hx : 0 < x
hL : (fun (x : ℝ) ↦ f (x + 1)) =ᶠ[𝓝 x] f + log
⊢ deriv (fun (x : ℝ) ↦ f (x + 1)) x = deriv (f + log) x

Tactic:
apply EventuallyEq.deriv_eq

Premises used: Filter.EventuallyEq.deriv_eq
-- 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
x : ℝ
hx : 0 < x
⊢ ∀ (a : ℝ), 0 < a → f (a + 1) = (f + log) a

Tactic:
h_rec
-- 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
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
h₁ : ∀ (a : ℝ), 0 < a → f (a + 1) = (f + log) a
⊢ (fun (x : ℝ) ↦ f (x + 1)) =ᶠ[𝓝 x] f + log

Tactic:
filter_upwards [eventually_gt_nhds hx] using h_rec

Premises used: eventually_gt_nhds
-- 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
⊢ ∀ (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
-- 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
⊢ deriv f (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) = deriv f 1 + (↑(harmonic 0) : ℝ)

Tactic:
simp
-- 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
n : ℕ
hn : deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic 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
n : ℕ
hn : deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
succ :
  deriv f 1 + (↑(harmonic n) : ℝ) + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    deriv f 1 + (↑(harmonic n + (↑(n + 1) : ℚ)⁻¹) : ℝ)
⊢ deriv f (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1) = deriv f 1 + (↑(harmonic (n + 1)) : ℝ)

Tactic:
rw [cast_succ, hder_rec (n + 1) (by positivity), hn, harmonic_succ]

Premises used: Nat.cast_succ, Nat.cast, harmonic_succ, HAdd.hAdd, OfNat.ofNat
-- 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
n : ℕ
hn : deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)
succ :
  deriv f 1 + (↑(harmonic n) : ℝ) + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    deriv f 1 + ((↑(harmonic n) : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹)
⊢ deriv f 1 + (↑(harmonic n) : ℝ) + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    deriv f 1 + (↑(harmonic n + (↑(n + 1) : ℚ)⁻¹) : ℝ)

Tactic:
push_cast
-- 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
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) : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 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
n : ℕ
zero : deriv f (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) = deriv f 1 + (↑(harmonic 0) : ℝ)
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)) : ℝ)
⊢ deriv f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = deriv f 1 + (↑(harmonic n) : ℝ)

Tactic:
induction n with
    | zero => simp
    | succ n hn =>
      rw [cast_succ, hder_rec (n + 1) (by positivity), hn, harmonic_succ]
      push_cast
      ring

Premises used: Nat.cast_succ, Nat.cast, harmonic_succ, HAdd.hAdd, Nat.zero, OfNat.ofNat, Nat.succ
-- 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
⊢ ∀ (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
-- 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) : ℝ)
this : -deriv f 1 = γ
rw : deriv f 1 + (↑(harmonic n) : ℝ) = -γ + (↑(harmonic n) : ℝ)
rw₁ : deriv f 1 + (↑(harmonic n) : ℝ) = - -deriv f 1 + (↑(harmonic n) : ℝ)
rw₂ rw₃ : deriv f 1 + (↑(harmonic n) : ℝ) = deriv f 1 + (↑(harmonic n) : ℝ)
⊢ deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)

Tactic:
rw [hder_nat n, ← this, neg_neg]

Premises used: neg_neg
-- 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) : ℝ)
suffices : -deriv f 1 = γ
⊢ deriv (log ∘ Gamma) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = -γ + (↑(harmonic n) : ℝ)

Tactic:
suffices -deriv f 1 = γ by rw [hder_nat n, ← this, neg_neg]
-- 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) : ℝ)
n : ℕ
hn : 0 < 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) : ℝ)
n : ℕ
hn : 0 < n
linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ (↑n : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ)) = 0
⊢ (↑n : ℝ) < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

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) : ℝ)
n : ℕ
hn : 0 < n
refine : log (↑n : ℝ) = slope f (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ log (↑n : ℝ) ≤ deriv f (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)

Premises used: Iff.mpr, Nat.cast_pos, ConvexOn.slope_le_deriv, Set.mem_Ioi, 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) : ℝ)
n : ℕ
hn : 0 < n
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ) = 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) : ℝ)
n : ℕ
hn : 0 < n
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

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) : ℝ)
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 : ℝ)
rw₄ rw₅ : log (↑n : ℝ) = log (↑n : ℝ)
⊢ log (↑n : ℝ) = slope f (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑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]

Premises used: add_sub_cancel_left, Nat.cast, slope_def_field, div_one