awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f (↑m : ℝ) = f 1 + log (↑(m - 1)! : ℝ)
A : LT.lt (α := ℝ) 0 (↑m : ℝ)
⊢ m = m.pred + 1

Tactic:
exact (Nat.succ_pred_eq_of_pos hm).symm

Premises used: Nat.succ_pred_eq_of_pos, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
⊢ f (x + (↑0 : ℝ)) = f x + ∑ m ∈ Finset.range 0, log (x + (↑m : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
push_cast : x + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = x + (↑n : ℝ) + 1
⊢ x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
⊢ x + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = x + (↑n : ℝ) + 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
⊢ x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1

Tactic:
have : x + n.succ = x + n + 1 := by push_cast; ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
this : x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1
succ :
  f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ)) + log (x + (↑n : ℝ)) =
    f x + ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))
succ₁ : 0 < x + (↑n : ℝ)
⊢ f (x + (↑(n + 1) : ℝ)) = f x + ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))

Tactic:
rw [this, hf_feq, hn]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
this : x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1
succ :
  f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ)) + log (x + (↑n : ℝ)) =
    f x + (log (x + (↑n : ℝ)) + ∑ x_1 ∈ Finset.range n, log (x + (↑x_1 : ℝ)))
⊢ f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ)) + log (x + (↑n : ℝ)) =
    f x + ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))

Tactic:
rw [Finset.range_add_one, Finset.sum_insert Finset.notMem_range_self]

Premises used: Finset.range_add_one, Finset.notMem_range_self, Finset.sum_insert
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
this : x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1
⊢ f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ)) + log (x + (↑n : ℝ)) =
    f x + (log (x + (↑n : ℝ)) + ∑ x_1 ∈ Finset.range n, log (x + (↑x_1 : ℝ)))

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))
this : x + (↑n.succ : ℝ) = x + (↑n : ℝ) + 1
linarith : x + (↑n : ℝ) ≤ 0 → HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (0 - x) + (x + (↑n : ℝ) - 0) = 0
⊢ 0 < x + (↑n : ℝ)

Tactic:
linarith [(Nat.cast_nonneg n : 0 ≤ (n : ℝ))]

Premises used: Nat.cast_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
zero : f (x + (↑0 : ℝ)) = f x + ∑ m ∈ Finset.range 0, log (x + (↑m : ℝ))
succ :
  ∀ (n : ℕ) (hn : f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))),
    f (x + (↑(n + 1) : ℝ)) = f x + ∑ m ∈ Finset.range (n + 1), log (x + (↑m : ℝ))
⊢ f (x + (↑n : ℝ)) = f x + ∑ m ∈ Finset.range n, log (x + (↑m : ℝ))

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    have : x + n.succ = x + n + 1 := by push_cast; ring
    rw [this, hf_feq, hn]
    · rw [Finset.range_add_one, Finset.sum_insert Finset.notMem_range_self]
      abel
    · linarith [(Nat.cast_nonneg n : 0 ≤ (n : ℝ))]

Premises used: Nat.cast_nonneg, Finset.range_add_one, Finset.notMem_range_self, Finset.sum_insert
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have hn' : 0 < (n : ℝ) := Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * (f (↑n : ℝ) + log (↑n : ℝ))
⊢ f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
rw [hf_feq hn']
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * (f (↑n : ℝ) + log (↑n : ℝ))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
have : f n + x * log n = (1 - x) * f n + x * f (n + 1) := by rw [hf_feq hn']; ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ (↑n : ℝ) + x = (1 - x) * (↑n : ℝ) + x * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw :
  f ((1 - x) * (↑n : ℝ) + x * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤
    (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ f ((↑n : ℝ) + x) ≤ f (↑n : ℝ) + x * log (↑n : ℝ)

Tactic:
rw [this, (by ring : (n : ℝ) + x = (1 - x) * n + x * (n + 1))]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
linarith :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 0 → -1 + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - 0) = 0
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
linarith : 1 - x < 0 → x - 1 + (1 - x - 0) = 0
⊢ 0 ≤ 1 - x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
linarith : 1 - x + x < 1 → 1 - x + x - 1 = 0
linarith₁ : 1 < 1 - x + x → 1 - (1 - x + x) = 0
⊢ 1 - x + x = 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : f (↑n : ℝ) + x * log (↑n : ℝ) = (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ f ((1 - x) * (↑n : ℝ) + x * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤
    (1 - x) * f (↑n : ℝ) + x * f (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
simpa only [smul_eq_mul] using
    hf_conv.2 hn' (by linarith : 0 < (n + 1 : ℝ)) (by linarith : 0 ≤ 1 - x) hx.le (by linarith)

Premises used: LT.lt.le, And.right, smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
rw : 1 < n
⊢ 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1

Tactic:
rw [← Nat.cast_one, sub_pos, Nat.cast_lt]

Premises used: sub_pos, Nat.cast_lt, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
⊢ 1 < n

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
⊢ 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1

Tactic:
have npos : 0 < (n : ℝ) - 1 := by rw [← Nat.cast_one, sub_pos, Nat.cast_lt]; lia
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
linarith : (↑n : ℝ) + x ≤ 0 → -1 + (0 - x) + (0 - HSub.hSub (α := ℝ) (↑n : ℝ) 1) + ((↑n : ℝ) + x - 0) = 0
⊢ 0 < (↑n : ℝ) + x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
linarith : (↑n : ℝ) ≤ HSub.hSub (α := ℝ) (↑n : ℝ) 1 → -1 + ((↑n : ℝ) - HSub.hSub (α := ℝ) (↑n : ℝ) 1) = 0
⊢ HSub.hSub (α := ℝ) (↑n : ℝ) 1 < (↑n : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
linarith : (↑n : ℝ) + x ≤ (↑n : ℝ) → 0 - x + ((↑n : ℝ) + x - (↑n : ℝ)) = 0
⊢ (↑n : ℝ) < (↑n : ℝ) + x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ (f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) / ((↑n : ℝ) - HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤
    (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / ((↑n : ℝ) + x - (↑n : ℝ))

Tactic:
have c :=
    (convexOn_iff_slope_mono_adjacent.mp <| hf_conv).2 npos (by linarith : 0 < (n : ℝ) + x)
      (by linarith : (n : ℝ) - 1 < (n : ℝ)) (by linarith)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c :
  (f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) / ((↑n : ℝ) - HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤
    (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / ((↑n : ℝ) + x - (↑n : ℝ))
⊢ f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x

Tactic:
rw [add_sub_cancel_left, sub_sub_cancel, div_one] at c

Premises used: add_sub_cancel_left, sub_sub_cancel, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
rw : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) + log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ)
rw₁ : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1 + 1) = f (↑n : ℝ)
rw₂ rw₃ : f (↑n : ℝ) = f (↑n : ℝ)
⊢ f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)

Tactic:
rw [eq_sub_iff_add_eq, ← hf_feq npos, sub_add_cancel]

Premises used: eq_sub_iff_add_eq, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
⊢ f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)

Tactic:
have : f (↑n - 1) = f n - log (↑n - 1) := by
    rw [eq_sub_iff_add_eq, ← hf_feq npos, sub_add_cancel]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
npos : 0 < HSub.hSub (α := ℝ) (↑n : ℝ) 1
c : f (↑n : ℝ) - f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x
this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)
rwa :
  ∀ (c : f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)) ≤ (f ((↑n : ℝ) + x) - f (↑n : ℝ)) / x)
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₁ :
  ∀ (c : (f (↑n : ℝ) - (f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1))) * x ≤ f ((↑n : ℝ) + x) - f (↑n : ℝ))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₂ :
  ∀ (c : log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) * x ≤ f ((↑n : ℝ) + x) - f (↑n : ℝ))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₃ :
  ∀ (c : log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) * x + f (↑n : ℝ) ≤ f ((↑n : ℝ) + x))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₄ :
  ∀ (c : x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) + f (↑n : ℝ) ≤ f ((↑n : ℝ) + x))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (c : f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x))
    (this : f (HSub.hSub (α := ℝ) (↑n : ℝ) 1) = f (↑n : ℝ) - log (HSub.hSub (α := ℝ) (↑n : ℝ) 1)),
    f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)
⊢ f (↑n : ℝ) + x * log (HSub.hSub (α := ℝ) (↑n : ℝ) 1) ≤ f ((↑n : ℝ) + x)

Tactic:
rwa [this, le_div_iff₀ hx, sub_sub_cancel, le_sub_iff_add_le, mul_comm _ x, add_comm] at c

Premises used: add_comm, sub_sub_cancel, mul_comm, le_sub_iff_add_le, le_div_iff₀
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
rw :
  x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) - (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
      log x -
    (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
| x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) - ∑ m ∈ Finset.range (n + 1 + 1), log (x + (↑m : ℝ)) + log x -
    (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))

Tactic:
rw [Finset.sum_range_succ', Nat.cast_zero, add_zero]

Premises used: Nat.cast_zero, add_zero, Finset.sum_range_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
conv_rhs :
  (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) -
          (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
⊢ (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) - ∑ m ∈ Finset.range (n + 1 + 1), log (x + (↑m : ℝ)) + log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))

Tactic:
conv_rhs => rw [Finset.sum_range_succ', Nat.cast_zero, add_zero]

Premises used: Nat.cast_zero, add_zero, Finset.sum_range_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
rw :
  (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + (log (↑(n + 1) : ℝ) + log (↑n ! : ℝ)) -
          (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
hx : Ne (α := ℝ) (↑(n + 1) : ℝ) 0
hy : Ne (α := ℝ) (↑n ! : ℝ) 0
⊢ (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + log (↑((n + 1) * n !) : ℝ) -
          (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))

Tactic:
rw [Nat.cast_mul, log_mul]

Premises used: Nat.cast_mul, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
hx : n + 1 ≠ 0
⊢ Ne (α := ℝ) (↑(n + 1) : ℝ) 0

Tactic:
rw [Nat.cast_ne_zero]

Premises used: Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
Nat.succ_ne_zero n

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
exact Nat.succ_ne_zero n

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
hy : n ! ≠ 0
⊢ Ne (α := ℝ) (↑n ! : ℝ) 0

Tactic:
rw [Nat.cast_ne_zero]

Premises used: Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
⊢ n ! ≠ 0

Tactic:
Nat.factorial_ne_zero n

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
⊢ n ! ≠ 0

Tactic:
exact Nat.factorial_ne_zero n

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
a : ∀ m ∈ Finset.range (n + 1), x + 1 + (↑m : ℝ) = x + (↑(m + 1) : ℝ)
⊢ Eq (α := ℝ) (∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)))
    (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)))

Tactic:
congr! 2 with m
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n m : ℕ
h : m ∈ Finset.range (n + 1)
a : x + 1 + (↑m : ℝ) = x + HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ x + 1 + (↑m : ℝ) = x + (↑(m + 1) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n m : ℕ
h : m ∈ Finset.range (n + 1)
⊢ x + 1 + (↑m : ℝ) = x + HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
⊢ Eq (α := ℝ) (∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)))
    (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)))

Tactic:
have :
    ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) =
      ∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1)) := by
    congr! 2 with m
    push_cast
    abel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
this :
  Eq (α := ℝ) (∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)))
    (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)))
rw :
  (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + log (↑n ! : ℝ)) -
          (∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))
⊢ (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (↑(n + 1) : ℝ) + (log (↑(n + 1) : ℝ) + log (↑n ! : ℝ)) -
          (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))

Tactic:
rw [← this, Nat.cast_add_one n]

Premises used: Nat.cast_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
n : ℕ
this :
  Eq (α := ℝ) (∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)))
    (∑ k ∈ Finset.range (n + 1), log (x + (↑(k + 1) : ℝ)))
⊢ (x + 1) * log (↑n : ℝ) + log (↑n ! : ℝ) - ∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) =
    x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + log (↑n ! : ℝ)) -
          (∑ m ∈ Finset.range (n + 1), log (x + 1 + (↑m : ℝ)) + log x) +
        log x -
      (x + 1) * (log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
rw :
  f ((↑(n + 1) : ℝ) + x) ≤
    f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + (x * log (↑n : ℝ) + log (↑n ! : ℝ))
⊢ f x ≤ f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + logGammaSeq x n

Tactic:
rw [logGammaSeq, ← add_sub_assoc, le_sub_iff_add_le, ← f_add_nat_eq (@hf_feq) hx, add_comm x]

Premises used: add_sub_assoc, Real.BohrMollerup.logGammaSeq, add_comm, Real.BohrMollerup.f_add_nat_eq, le_sub_iff_add_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f ((↑(n + 1) : ℝ) + x) ≤
    f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + (x * log (↑n : ℝ) + log (↑n ! : ℝ))

Tactic:
(f_add_nat_le hf_conv (@hf_feq) (Nat.add_one_ne_zero n) hx hx').trans (le_of_eq ?_)

Premises used: Nat.add_one_ne_zero, Real.BohrMollerup.f_add_nat_le, LE.le.trans, le_of_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
refine :
  f (↑(n + 1) : ℝ) + x * log (↑(n + 1) : ℝ) =
    f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + (x * log (↑n : ℝ) + log (↑n ! : ℝ))
⊢ f ((↑(n + 1) : ℝ) + x) ≤
    f 1 + x * log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - x * log (↑n : ℝ) + (x * log (↑n : ℝ) + log (↑n ! : ℝ))

Tactic:
refine (f_add_nat_le hf_conv (@hf_feq) (Nat.add_one_ne_zero n) hx hx').trans (le_of_eq ?_)

Premises used: Nat.add_one_ne_zero, Real.BohrMollerup.f_add_nat_le, LE.le.trans, le_of_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
lia