-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
lemma Gammaℝ_residue_zero : Tendsto (fun s ↦ s * Gammaℝ s) (𝓝[≠] 0) (𝓝 2)

Proof state:
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun s => s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)

Tactic:
have h' : Tendsto (fun s : ℂ ↦ 2 * (π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2) := by
  rw [(by simp : 𝓝 2 = 𝓝 (2 * (π : ℂ) ^ (-(0 : ℂ) / 2)))]
  refine Tendsto.mono_left (ContinuousAt.tendsto ?_) nhdsWithin_le_nhds
  exact continuousAt_const.mul ((continuousAt_const_cpow (ofReal_ne_zero.mpr pi_ne_zero)).comp
    (continuousAt_id.neg.div_const _))

Result:
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (fun s => 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
⊢ Tendsto (fun s => s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)

Proof state:
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun s => 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)

Tactic:
rw [(by simp : 𝓝 2 = 𝓝 (2 * (π : ℂ) ^ (-(0 : ℂ) / 2)))]

Result:
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun s => 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 (2 * ↑π ^ (-0 / 2)))

Proof state:
⊢ Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)

Tactic:
refine tendsto_self_mul_Gamma_nhds_zero.comp ?_

Result:
⊢ Tendsto (fun z => z / 2) (𝓝[≠] 0) (𝓝[≠] 0)

Proof state:
⊢ Tendsto (fun z => z / 2) (𝓝[≠] 0) (𝓝[≠] 0)

Tactic:
rw [tendsto_nhdsWithin_iff, (by simp : 𝓝 (0 : ℂ) = 𝓝 (0 / 2))]

Result:
⊢ Tendsto (fun z => z / 2) (𝓝[≠] 0) (𝓝 (0 / 2)) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, n / 2 ∈ {0}ᶜ

Proof state:
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ ContinuousAt (fun s => 2 * ↑π ^ (-s / 2)) 0

Tactic:
exact continuousAt_const.mul ((continuousAt_const_cpow (ofReal_ne_zero.mpr pi_ne_zero)).comp
  (continuousAt_id.neg.div_const _))

Result:
no goals

Proof state:
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (fun s => 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
⊢ Tendsto (fun s => s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)

Tactic:
convert mul_one (2 : ℂ) ▸ (h'.mul h) using 2 with z

Result:
case h.e'_3.h
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (fun s => 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
z : ℂ
⊢ z * z.Gammaℝ = 2 * ↑π ^ (-z / 2) * (z / 2 * Gamma (z / 2))

Proof state:
⊢ 𝓝 0 = 𝓝 (0 / 2)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3.h
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (fun s => 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
z : ℂ
⊢ z * (↑π ^ (-z / 2) * Gamma (z / 2)) = 2 * ↑π ^ (-z / 2) * (z / 2 * Gamma (z / 2))

Tactic:
ring_nf

Result:
no goals

Proof state:
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ 𝓝 2 = 𝓝 (2 * ↑π ^ (-0 / 2))

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3.h
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (fun s => 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
z : ℂ
⊢ z * z.Gammaℝ = 2 * ↑π ^ (-z / 2) * (z / 2 * Gamma (z / 2))

Tactic:
rw [Gammaℝ]

Result:
case h.e'_3.h
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (fun s => 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
z : ℂ
⊢ z * (↑π ^ (-z / 2) * Gamma (z / 2)) = 2 * ↑π ^ (-z / 2) * (z / 2 * Gamma (z / 2))

Proof state:
⊢ Tendsto (fun z => z / 2) (𝓝[≠] 0) (𝓝 (0 / 2)) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, n / 2 ∈ {0}ᶜ

Tactic:
exact ⟨(tendsto_id.div_const _).mono_left nhdsWithin_le_nhds,
  eventually_of_mem self_mem_nhdsWithin fun x hx ↦ div_ne_zero hx two_ne_zero⟩

Result:
no goals

Proof state:
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun s => 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 (2 * ↑π ^ (-0 / 2)))

Tactic:
refine Tendsto.mono_left (ContinuousAt.tendsto ?_) nhdsWithin_le_nhds

Result:
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ ContinuousAt (fun s => 2 * ↑π ^ (-s / 2)) 0

Proof state:
⊢ Tendsto (fun s => s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)

Tactic:
have h : Tendsto (fun z : ℂ ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1) := by
  refine tendsto_self_mul_Gamma_nhds_zero.comp ?_
  rw [tendsto_nhdsWithin_iff, (by simp : 𝓝 (0 : ℂ) = 𝓝 (0 / 2))]
  exact ⟨(tendsto_id.div_const _).mono_left nhdsWithin_le_nhds,
    eventually_of_mem self_mem_nhdsWithin fun x hx ↦ div_ne_zero hx two_ne_zero⟩

Result:
h : Tendsto (fun z => z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun s => s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)