-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem GammaSeq_tendsto_Gamma (s : ℂ) : Tendsto (GammaSeq s) atTop (𝓝 <| Gamma s)

Proof state:
case zero
s : ℂ
hs : 0 < s.re
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
refine Tendsto.congr' ?_ (approx_Gamma_integral_tendsto_Gamma_integral hs)

Result:
case zero
s : ℂ
hs : 0 < s.re
⊢ (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) =ᶠ[atTop] s.GammaSeq

Proof state:
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
rw [Gamma]

Result:
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (GammaAux ⌊1 - s.re⌋₊ s))

Proof state:
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => s.GammaSeq n * (↑n / (↑n + 1 + s))) atTop (𝓝 (GammaAux m (s + 1) / s * 1))
⊢ Tendsto (fun n => ↑n / (↑n + 1 + s)) atTop (𝓝 1)

Tactic:
simp_rw [add_assoc]

Result:
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => s.GammaSeq n * (↑n / (↑n + 1 + s))) atTop (𝓝 (GammaAux m (s + 1) / s * 1))
⊢ Tendsto (fun n => ↑n / (↑n + (1 + s))) atTop (𝓝 1)

Proof state:
case a.inr
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
hs : s.re ≤ 0
⊢ -s.re < ↑⌊1 - s.re⌋₊

Tactic:
refine (Nat.lt_floor_add_one _).trans_le ?_

Result:
case a.inr
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
hs : s.re ≤ 0
⊢ ↑⌊-s.re⌋₊ + 1 ≤ ↑⌊1 - s.re⌋₊

Proof state:
case succ.refine_3
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto ?succ.refine_1 atTop (𝓝 (GammaAux m (s + 1) / s))
⊢ Tendsto s.GammaSeq atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))

case succ.refine_1
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
⊢ ℕ → ℂ

case succ.refine_2
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
n : ℕ
hn : n ≠ 0
⊢ (s + 1).GammaSeq n / s = ?succ.refine_1 n

Tactic:
pick_goal 3

Result:
case succ.refine_2
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
n : ℕ
hn : n ≠ 0
⊢ (s + 1).GammaSeq n / s = ?succ.refine_1 n

case succ.refine_3
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto ?succ.refine_1 atTop (𝓝 (GammaAux m (s + 1) / s))
⊢ Tendsto s.GammaSeq atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))

case succ.refine_1
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
⊢ ℕ → ℂ

Proof state:
case succ.refine_3
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => s.GammaSeq n * (↑n / (↑n + 1 + s))) atTop (𝓝 (GammaAux m (s + 1) / s))
⊢ Tendsto s.GammaSeq atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))

Tactic:
rwa [← mul_one (GammaAux m (s + 1) / s), tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this

Result:
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => s.GammaSeq n * (↑n / (↑n + 1 + s))) atTop (𝓝 (GammaAux m (s + 1) / s * 1))
⊢ Tendsto (fun n => ↑n / (↑n + 1 + s)) atTop (𝓝 1)

Proof state:
case succ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
⊢ Tendsto s.GammaSeq atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))

Tactic:
have := @Tendsto.congr' _ _ _ ?_ _ _
  ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn => ?_)) ((IH _ hs).div_const s)

Result:
case succ.refine_3
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto ?succ.refine_1 atTop (𝓝 (GammaAux m (s + 1) / s))
⊢ Tendsto s.GammaSeq atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))

case succ.refine_1
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
⊢ ℕ → ℂ

case succ.refine_2
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
n : ℕ
hn : n ≠ 0
⊢ (s + 1).GammaSeq n / s = ?succ.refine_1 n

Proof state:
case succ.refine_3
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => ↑n / (↑n + 1 + s) * s.GammaSeq n) atTop (𝓝 (GammaAux m (s + 1) / s))
⊢ Tendsto s.GammaSeq atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))

Tactic:
conv at this => arg 1; intro n; rw [mul_comm]

Result:
case succ.refine_3
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => s.GammaSeq n * (↑n / (↑n + 1 + s))) atTop (𝓝 (GammaAux m (s + 1) / s))
⊢ Tendsto s.GammaSeq atTop (𝓝 ((fun s => GammaAux m (s + 1) / s) s))

Proof state:
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
hs : -↑m < (s + 1).re
this : Tendsto (fun n => s.GammaSeq n * (↑n / (↑n + 1 + s))) atTop (𝓝 (GammaAux m (s + 1) / s * 1))
⊢ Tendsto (fun n => ↑n / (↑n + (1 + s))) atTop (𝓝 1)

Tactic:
exact tendsto_natCast_div_add_atTop (1 + s)

Result:
no goals

Proof state:
case a.inr
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
hs : s.re ≤ 0
⊢ ↑⌊-s.re⌋₊ + 1 ≤ ↑⌊1 - s.re⌋₊

Tactic:
rw [sub_eq_neg_add, Nat.floor_add_one (neg_nonneg.mpr hs), Nat.cast_add_one]

Result:
no goals

Proof state:
case a.inl
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
hs : 0 < s.re
⊢ -s.re < ↑⌊1 - s.re⌋₊

Tactic:
exact (neg_neg_of_pos hs).trans_le (Nat.cast_nonneg _)

Result:
no goals

Proof state:
case zero
s : ℂ
hs : 0 < s.re
⊢ Tendsto s.GammaSeq atTop (𝓝 (GammaAux 0 s))

Tactic:
rw [← Gamma_eq_GammaAux]

Result:
case zero
s : ℂ
hs : 0 < s.re
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

case zero.h1
s : ℂ
hs : 0 < s.re
⊢ -s.re < ↑0

Proof state:
case a
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
⊢ -↑⌊1 - s.re⌋₊ < s.re

Tactic:
rw [neg_lt]

Result:
case a
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
⊢ -s.re < ↑⌊1 - s.re⌋₊

Proof state:
case zero.h1
s : ℂ
hs : 0 < s.re
⊢ -s.re < ↑0

Tactic:
rwa [Nat.cast_zero, neg_lt_zero]

Result:
no goals

Proof state:
s : ℂ
m : ℕ
⊢ -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))

Tactic:
induction' m with m IH generalizing s

Result:
case zero
s : ℂ
⊢ -↑0 < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux 0 s))

case succ
m : ℕ
IH : ∀ (s : ℂ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
s : ℂ
⊢ -↑(m + 1) < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux (m + 1) s))

Proof state:
s : ℂ
⊢ ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))

Tactic:
intro m

Result:
s : ℂ
m : ℕ
⊢ -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))

Proof state:
case zero
s : ℂ
hs : 0 < s.re
⊢ (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) =ᶠ[atTop] s.GammaSeq

Tactic:
refine (eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn => ?_)

Result:
case zero
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
⊢ (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) n = s.GammaSeq n

Proof state:
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (GammaAux ⌊1 - s.re⌋₊ s))

Tactic:
apply this

Result:
case a
s : ℂ
this : ∀ (m : ℕ), -↑m < s.re → Tendsto s.GammaSeq atTop (𝓝 (GammaAux m s))
⊢ -↑⌊1 - s.re⌋₊ < s.re