-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem Gamma_mul_Gamma_add_half (s : ℂ) :
    Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * (2 : ℂ) ^ (1 - 2 * s) * ↑(√π)

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
⊢ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π

Tactic:
refine AnalyticOnNhd.eq_of_frequently_eq h1 h2 (h3.frequently ?_)

Result:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
⊢ ∃ᶠ (x : ℝ) in 𝓝[≠] 1, (Gamma ↑x)⁻¹ * (Gamma (↑x + 1 / 2))⁻¹ = (Gamma (2 * ↑x))⁻¹ * 2 ^ (2 * ↑x - 1) / ↑√π

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)

Tactic:
rw [tendsto_nhdsWithin_iff]

Result:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝 1) ∧ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, ↑n ∈ {1}ᶜ

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1)

Tactic:
apply Differentiable.mul

Result:
case ha
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ fun y => (Gamma (2 * y))⁻¹

case hb
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ fun y => 2 ^ (2 * y - 1)

Proof state:
case hb
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
t : ℂ
⊢ DifferentiableAt ℂ (fun y => 2 * y - 1) t

Tactic:
exact DifferentiableAt.sub_const (differentiableAt_id.const_mul _) _

Result:
no goals

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝 1) ∧ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, ↑n ∈ {1}ᶜ

Tactic:
constructor

Result:
case left
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝 1)

case right
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, ↑n ∈ {1}ᶜ

Proof state:
s : ℂ
⊢ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π

Tactic:
have h1 : AnalyticOnNhd ℂ (fun z : ℂ => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ := by
  refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
  refine (differentiable_one_div_Gamma.mul ?_).differentiableOn
  exact differentiable_one_div_Gamma.comp (differentiable_id.add (differentiable_const _))

Result:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π

Proof state:
case left
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝 1)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt

Result:
no goals

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ ↑2 = 2

Tactic:
norm_cast

Result:
no goals

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ DifferentiableOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ

Tactic:
refine (Differentiable.mul ?_ (differentiable_const _)).differentiableOn

Result:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1)

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ 2 * ↑t = ↑(2 * t)

Tactic:
norm_num

Result:
no goals

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
⊢ ∃ᶠ (x : ℝ) in 𝓝[≠] 1, (Gamma ↑x)⁻¹ * (Gamma (↑x + 1 / 2))⁻¹ = (Gamma (2 * ↑x))⁻¹ * 2 ^ (2 * ↑x - 1) / ↑√π

Tactic:
refine ((Eventually.filter_mono nhdsWithin_le_nhds) ?_).frequently

Result:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
⊢ ∀ᶠ (x : ℝ) in 𝓝 1, (Gamma ↑x)⁻¹ * (Gamma (↑x + 1 / 2))⁻¹ = (Gamma (2 * ↑x))⁻¹ * 2 ^ (2 * ↑x - 1) / ↑√π

Proof state:
case h.e'_2
s : ℂ
this : (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma s * Gamma (s + 1 / 2) = ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹

Tactic:
rw [mul_inv, inv_inv, inv_inv]

Result:
no goals

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
⊢ ∀ᶠ (x : ℝ) in 𝓝 1, (Gamma ↑x)⁻¹ * (Gamma (↑x + 1 / 2))⁻¹ = (Gamma (2 * ↑x))⁻¹ * 2 ^ (2 * ↑x - 1) / ↑√π

Tactic:
refine (eventually_gt_nhds zero_lt_one).mp (Eventually.of_forall fun t ht => ?_)

Result:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (Gamma ↑t)⁻¹ * (Gamma (↑t + 1 / 2))⁻¹ = (Gamma (2 * ↑t))⁻¹ * 2 ^ (2 * ↑t - 1) / ↑√π

Proof state:
case right
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, ↑n ∈ {1}ᶜ

Tactic:
exact eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ofReal_ne_one.mpr ht)

Result:
no goals

Proof state:
case h.e'_3
s : ℂ
this : (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π = ((Gamma (2 * s))⁻¹ * 2 ^ (2 * s - 1) / ↑√π)⁻¹

Tactic:
rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]

Result:
no goals

Proof state:
s : ℂ
⊢ AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ

Tactic:
refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ

Result:
s : ℂ
⊢ DifferentiableOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ

Proof state:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ

Tactic:
refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ

Result:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ DifferentiableOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ