-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem tendsto_logGammaSeq (hf_conv : ConvexOn ℝ (Ioi 0) f)
    (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y) (hx : 0 < x) :
    Tendsto (logGammaSeq x) atTop (𝓝 <| f x - f 1)

Proof state:
case zero
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
x : ℝ
hx : 0 < x
⊢ ↑0 < x → x ≤ ↑0 + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
rw [Nat.cast_zero, zero_add]

Result:
case zero
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
x : ℝ
hx : 0 < x
⊢ 0 < x → x ≤ 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Proof state:
case refine_1
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
this : ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ ↑⌈x - 1⌉₊ < x

Tactic:
rcases lt_or_le x 1 with ⟨⟩

Result:
case refine_1.inl
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
this : ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
h✝ : x < 1
⊢ ↑⌈x - 1⌉₊ < x

case refine_1.inr
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
this : ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
h✝ : 1 ≤ x
⊢ ↑⌈x - 1⌉₊ < x

Proof state:
case succ
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
hm : ∀ {x : ℝ}, 0 < x → ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
specialize hm ((Nat.cast_nonneg _).trans_lt hy) hy hy'

Result:
case succ
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Proof state:
case zero
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
x : ℝ
hx : 0 < x
⊢ 0 < x → x ≤ 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
exact fun _ hx' => tendsto_logGammaSeq_of_le_one hf_conv (@hf_feq) hx hx'

Result:
no goals

Proof state:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
⊢ ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
intro m

Result:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
m : ℕ
⊢ ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Proof state:
case h.e'_5.h.e'_3
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this✝¹ :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm : Tendsto (fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n)) atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this✝ :
  ((fun x_1 =>
        (fun n => logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)) x_1 +
          (fun b => log (x - 1)) x_1) ∘
      fun a => a + 1) =
    fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n)
this : f x = f (x - 1) + log (x - 1)
⊢ f (x - 1) + log (x - 1) - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_5.h.e'_3
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this✝¹ :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm : Tendsto (fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n)) atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this✝ :
  ((fun x_1 =>
        (fun n => logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)) x_1 +
          (fun b => log (x - 1)) x_1) ∘
      fun a => a + 1) =
    fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n)
this : f (x - 1 + 1) = f (x - 1) + log (x - 1)
⊢ f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0

Tactic:
rw [sub_add_cancel] at this

Result:
case h.e'_5.h.e'_3
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this✝¹ :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm : Tendsto (fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n)) atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this✝ :
  ((fun x_1 =>
        (fun n => logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)) x_1 +
          (fun b => log (x - 1)) x_1) ∘
      fun a => a + 1) =
    fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n)
this : f x = f (x - 1) + log (x - 1)
⊢ f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0

Proof state:
case succ
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
hm : ∀ {x : ℝ}, 0 < x → ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
x : ℝ
hx : 0 < x
⊢ ↑(m + 1) < x → x ≤ ↑(m + 1) + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
intro hy hy'

Result:
case succ
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
hm : ∀ {x : ℝ}, 0 < x → ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
x : ℝ
hx : 0 < x
hy : ↑(m + 1) < x
hy' : x ≤ ↑(m + 1) + 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Proof state:
case succ
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
this :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
replace hm :=
  ((Tendsto.congr' this hm).add (tendsto_const_nhds : Tendsto (fun _ => log (x - 1)) _ _)).comp
    (tendsto_add_atTop_nat 1)

Result:
case succ
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm :
  Tendsto
    ((fun x_1 => logGammaSeq x (x_1 - 1) + x * (log (↑(x_1 - 1) + 1) - log ↑(x_1 - 1)) - log (x - 1) + log (x - 1)) ∘
      fun a => a + 1)
    atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Proof state:
case h.e'_3.h
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this✝ :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm : Tendsto (fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n)) atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this :
  ((fun x_1 =>
        (fun n => logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)) x_1 +
          (fun b => log (x - 1)) x_1) ∘
      fun a => a + 1) =
    fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n)
x✝ : ℕ
⊢ logGammaSeq x x✝ = logGammaSeq x x✝ + x * (log (↑x✝ + 1) - log ↑x✝) - x * (log (↑x✝ + 1) - log ↑x✝)

Tactic:
ring

Result:
no goals