-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem logGammaSeq_add_one (x : ℝ) (n : ℕ) :
    logGammaSeq (x + 1) n = logGammaSeq x (n + 1) + log x - (x + 1) * (log (n + 1) - log n)

Proof state:
case a.h.e'_1
x : ℝ
n m : ℕ
a✝ : m ∈ Finset.range (n + 1)
⊢ x + 1 + ↑m = x + (↑m + 1)

Tactic:
abel

Result:
no goals

Proof state:
case hx
x : ℝ
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
exact Nat.succ_ne_zero n

Result:
no goals

Proof state:
case hy
x : ℝ
n : ℕ
⊢ ↑n ! ≠ 0

Tactic:
rw [Nat.cast_ne_zero]

Result:
case hy
x : ℝ
n : ℕ
⊢ n ! ≠ 0

Proof state:
case hx
x : ℝ
n : ℕ
⊢ ↑(n + 1) ≠ 0

Tactic:
rw [Nat.cast_ne_zero]

Result:
case hx
x : ℝ
n : ℕ
⊢ n + 1 ≠ 0

Proof state:
x : ℝ
n : ℕ
this : ∑ 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 ↑(n + 1) + (log ↑(n + 1) + log ↑n !) - (∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1)) + log x) + log x -
      (x + 1) * (log (↑n + 1) - log ↑n)

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

Result:
x : ℝ
n : ℕ
this : ∑ 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 (↑n + 1) + (log (↑n + 1) + log ↑n !) - (∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) + log x) + log x -
      (x + 1) * (log (↑n + 1) - log ↑n)

Proof state:
x : ℝ
n : ℕ
this : ∑ 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 (↑n + 1) + (log (↑n + 1) + log ↑n !) - (∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) + log x) + log x -
      (x + 1) * (log (↑n + 1) - log ↑n)

Tactic:
ring

Result:
no goals

Proof state:
case a.h.e'_1
x : ℝ
n m : ℕ
a✝ : m ∈ Finset.range (n + 1)
⊢ x + 1 + ↑m = x + ↑(m + 1)

Tactic:
push_cast

Result:
case a.h.e'_1
x : ℝ
n m : ℕ
a✝ : m ∈ Finset.range (n + 1)
⊢ x + 1 + ↑m = x + (↑m + 1)

Proof state:
x : ℝ
n : ℕ
⊢ logGammaSeq (x + 1) n = logGammaSeq x (n + 1) + log x - (x + 1) * (log (↑n + 1) - log ↑n)

Tactic:
dsimp only [Nat.factorial_succ, logGammaSeq]

Result:
x : ℝ
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 (↑n + 1) - log ↑n)

Proof state:
x : ℝ
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 (↑n + 1) - log ↑n)

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

Result:
x : ℝ
n : ℕ
this : ∑ 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 ↑(n + 1) + (log ↑(n + 1) + log ↑n !) - (∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1)) + log x) + log x -
      (x + 1) * (log (↑n + 1) - log ↑n)

Proof state:
x : ℝ
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 (↑n + 1) - log ↑n)

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

Result:
x : ℝ
n : ℕ
⊢ (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 (↑n + 1) - log ↑n)

Proof state:
x : ℝ
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 (↑n + 1) - log ↑n)

case hx
x : ℝ
n : ℕ
⊢ ↑(n + 1) ≠ 0

case hy
x : ℝ
n : ℕ
⊢ ↑n ! ≠ 0

Tactic:
rotate_left

Result:
case hx
x : ℝ
n : ℕ
⊢ ↑(n + 1) ≠ 0

case hy
x : ℝ
n : ℕ
⊢ ↑n ! ≠ 0

x : ℝ
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 (↑n + 1) - log ↑n)

Proof state:
case hy
x : ℝ
n : ℕ
⊢ n ! ≠ 0

Tactic:
exact Nat.factorial_ne_zero n

Result:
no goals

Proof state:
x : ℝ
n : ℕ
⊢ (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 (↑n + 1) - log ↑n)

Tactic:
rw [Nat.cast_mul, log_mul]

Result:
x : ℝ
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 (↑n + 1) - log ↑n)

case hx
x : ℝ
n : ℕ
⊢ ↑(n + 1) ≠ 0

case hy
x : ℝ
n : ℕ
⊢ ↑n ! ≠ 0

Proof state:
x : ℝ
n : ℕ
⊢ ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = ∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1))

Tactic:
congr! 2 with m

Result:
case a.h.e'_1
x : ℝ
n m : ℕ
a✝ : m ∈ Finset.range (n + 1)
⊢ x + 1 + ↑m = x + ↑(m + 1)