-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem GammaIntegral_add_one {s : ℂ} (hs : 0 < s.re) :
    GammaIntegral (s + 1) = s * GammaIntegral s

Proof state:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : X ∈ Ici 0
⊢ (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) X = (s + 1).partialGamma X

Tactic:
rw [partialGamma_add_one hs (mem_Ici.mp hX)]

Result:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : X ∈ Ici 0
⊢ (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) X = s * s.partialGamma X - ↑(rexp (-X)) * ↑X ^ s

Proof state:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) atTop (𝓝 (s * s.GammaIntegral))

Tactic:
suffices Tendsto (fun X => -X ^ s * (-X).exp : ℝ → ℂ) atTop (𝓝 0) by
  simpa using Tendsto.add (Tendsto.const_mul s (tendsto_partialGamma hs)) this

Result:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (fun X => -↑X ^ s * ↑(rexp (-X))) atTop (𝓝 0)

Proof state:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : x ∈ Ioi 0
⊢ ‖-↑x ^ s * ↑(rexp (-x))‖ = x ^ s.re * rexp (-1 * x)

Tactic:
rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
  Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]

Result:
no goals

Proof state:
s : ℂ
hs : 0 < s.re
this✝ : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
this : (fun e => ‖-↑e ^ s * ↑(rexp (-e))‖) =ᶠ[atTop] fun e => e ^ s.re * rexp (-1 * e)
⊢ Tendsto (fun x => ‖-↑x ^ s * ↑(rexp (-x))‖) atTop (𝓝 0)

Tactic:
exact (tendsto_congr' this).mpr (tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero _ _ zero_lt_one)

Result:
no goals

Proof state:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))

Tactic:
have : (fun X : ℝ => s * partialGamma s X - X ^ s * (-X).exp) =ᶠ[atTop]
    (s + 1).partialGamma := by
  apply eventuallyEq_of_mem (Ici_mem_atTop (0 : ℝ))
  intro X hX
  rw [partialGamma_add_one hs (mem_Ici.mp hX)]
  ring_nf

Result:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))

Proof state:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s + 1).GammaIntegral)

Tactic:
apply tendsto_partialGamma

Result:
case hs
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 0 < (s + 1).re

Proof state:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ (fun e => ‖-↑e ^ s * ↑(rexp (-e))‖) =ᶠ[atTop] fun e => e ^ s.re * rexp (-1 * e)

Tactic:
refine eventuallyEq_of_mem (Ioi_mem_atTop 0) ?_

Result:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ EqOn (fun e => ‖-↑e ^ s * ↑(rexp (-e))‖) (fun e => e ^ s.re * rexp (-1 * e)) (Ioi 0)

Proof state:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : X ∈ Ici 0
⊢ (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) X = s * s.partialGamma X - ↑(rexp (-X)) * ↑X ^ s

Tactic:
ring_nf

Result:
no goals

Proof state:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (fun X => -↑X ^ s * ↑(rexp (-X))) atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Result:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (fun x => ‖-↑x ^ s * ↑(rexp (-x))‖) atTop (𝓝 0)

Proof state:
s : ℂ
hs : 0 < s.re
⊢ EqOn (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) (s + 1).partialGamma (Ici 0)

Tactic:
intro X hX

Result:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : X ∈ Ici 0
⊢ (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) X = (s + 1).partialGamma X

Proof state:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (fun x => ‖-↑x ^ s * ↑(rexp (-x))‖) atTop (𝓝 0)

Tactic:
have :
    (fun e : ℝ => ‖-(e : ℂ) ^ s * (-e).exp‖) =ᶠ[atTop] fun e : ℝ => e ^ s.re * (-1 * e).exp := by
  refine eventuallyEq_of_mem (Ioi_mem_atTop 0) ?_
  intro x hx; dsimp only
  rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
    Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]

Result:
s : ℂ
hs : 0 < s.re
this✝ : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
this : (fun e => ‖-↑e ^ s * ↑(rexp (-e))‖) =ᶠ[atTop] fun e => e ^ s.re * rexp (-1 * e)
⊢ Tendsto (fun x => ‖-↑x ^ s * ↑(rexp (-x))‖) atTop (𝓝 0)

Proof state:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ (s + 1).GammaIntegral = s * s.GammaIntegral

Tactic:
refine tendsto_nhds_unique ?_ this

Result:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s + 1).GammaIntegral)

Proof state:
case hs
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 0 < s.re + 1

Tactic:
linarith

Result:
no goals

Proof state:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ EqOn (fun e => ‖-↑e ^ s * ↑(rexp (-e))‖) (fun e => e ^ s.re * rexp (-1 * e)) (Ioi 0)

Tactic:
intro x hx

Result:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun e => ‖-↑e ^ s * ↑(rexp (-e))‖) x = (fun e => e ^ s.re * rexp (-1 * e)) x

Proof state:
s : ℂ
hs : 0 < s.re
this✝ : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
this : Tendsto (fun X => -↑X ^ s * ↑(rexp (-X))) atTop (𝓝 0)
⊢ Tendsto (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) atTop (𝓝 (s * s.GammaIntegral))

Tactic:
simpa using Tendsto.add (Tendsto.const_mul s (tendsto_partialGamma hs)) this

Result:
no goals

Proof state:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))

Tactic:
refine Tendsto.congr' this ?_

Result:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) atTop (𝓝 (s * s.GammaIntegral))

Proof state:
case hs
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 0 < (s + 1).re

Tactic:
rw [add_re, one_re]

Result:
case hs
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 0 < s.re + 1

Proof state:
s : ℂ
hs : 0 < s.re
⊢ (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma

Tactic:
apply eventuallyEq_of_mem (Ici_mem_atTop (0 : ℝ))

Result:
s : ℂ
hs : 0 < s.re
⊢ EqOn (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) (s + 1).partialGamma (Ici 0)

Proof state:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun e => ‖-↑e ^ s * ↑(rexp (-e))‖) x = (fun e => e ^ s.re * rexp (-1 * e)) x

Tactic:
dsimp only

Result:
s : ℂ
hs : 0 < s.re
this : (fun X => s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : x ∈ Ioi 0
⊢ ‖-↑x ^ s * ↑(rexp (-x))‖ = x ^ s.re * rexp (-1 * x)

Proof state:
s : ℂ
hs : 0 < s.re
⊢ (s + 1).GammaIntegral = s * s.GammaIntegral

Tactic:
suffices Tendsto (s + 1).partialGamma atTop (𝓝 <| s * GammaIntegral s) by
  refine tendsto_nhds_unique ?_ this
  apply tendsto_partialGamma; rw [add_re, one_re]; linarith

Result:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))