awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
h :
  Eq (α := Set ℝ) (Ioi (-1))
    (preimage (β := ℝ)
      (⇑(HAdd.hAdd (α := ℝ →ᵃ[ℝ] ℝ) (LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2)))
            (AffineMap.const ℝ ℝ (1 / 2))) :
        (a : ℝ) → ℝ)
      (Ioi 0))
h₁ :
  Eq (α := ℝ → ℝ) (fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2)))
    ((log ∘ Γ) ∘
      (⇑(HAdd.hAdd (α := ℝ →ᵃ[ℝ] ℝ) (LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2)))
            (AffineMap.const ℝ ℝ (1 / 2))) :
        (a : ℝ) → ℝ))
⊢ ConvexOn ℝ (β := ℝ) (Ioi (-1)) fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2))

Tactic:
convert!
      convexOn_log_Gamma.comp_affineMap
        ((DistribSMul.toLinearMap ℝ ℝ (1 / 2 : ℝ)).toAffineMap +
          AffineMap.const ℝ ℝ (1 / 2 : ℝ)) using 1

Premises used: Real, DistribSMul.toLinearMap, HDiv.hDiv, LinearMap.toAffineMap, Real.convexOn_log_Gamma, HAdd.hAdd, AffineMap.const, ConvexOn.comp_affineMap, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
h :
  Eq (α := Set ℝ) (Ioi (-1))
    (preimage (β := ℝ) (fun (x : ℝ) ↦ 1 / 2 * x) (preimage (β := ℝ) (fun (x : ℝ) ↦ x + 1 / 2) (Ioi 0)))
h₁ : Eq (α := Set ℝ) (Ioi (-1)) ((fun (x : ℝ) ↦ 1 / 2 * x) ⁻¹' Ioi (0 - 1 / 2))
h₂ : Eq (α := Set ℝ) (Ioi (-1)) ((fun (x : ℝ) ↦ 1 / 2 * x) ⁻¹' Ioi (-(1 / 2)))
h₃ : Ioi (-1) = Ioi (-(1 / 2) / (1 / 2))
h₄ : Ioi (-1) = Ioi (-(1 / 2 / (1 / 2)))
h₅ h₆ : Eq (α := Set ℝ) (Ioi (-1)) (Ioi (-1))
⊢ Eq (α := Set ℝ) (Ioi (-1)) (preimage (β := ℝ) ((fun (x : ℝ) ↦ x + 1 / 2) ∘ fun (x : ℝ) ↦ 1 / 2 * x) (Ioi 0))

Tactic:
rw [preimage_comp, preimage_add_const_Ioi, zero_sub,
        preimage_const_mul_Ioi₀ (_ : ℝ) one_half_pos, neg_div, div_self (@one_half_pos ℝ _).ne']

Premises used: Set.preimage_const_mul_Ioi₀, neg_div, Set.preimage_comp, LT.lt.ne', Set.preimage_add_const_Ioi, one_half_pos, div_self, zero_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
h :
  ∀ (x : ℝ),
    log (Γ (x / 2 + 1 / 2)) =
      ((log ∘ Γ) ∘
          (⇑(HAdd.hAdd (α := ℝ →ᵃ[ℝ] ℝ) (LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2)))
                (AffineMap.const ℝ ℝ (1 / 2))) :
            (a : ℝ) → ℝ))
        x
⊢ Eq (α := ℝ → ℝ) (fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2)))
    ((log ∘ Γ) ∘
      (⇑(HAdd.hAdd (α := ℝ →ᵃ[ℝ] ℝ) (LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2)))
            (AffineMap.const ℝ ℝ (1 / 2))) :
        (a : ℝ) → ℝ))

Tactic:
ext1 x
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
x : ℝ
h : log (Γ (x / 2 + 1 / 2)) = log (Γ (1 / 2 * x + 1 / 2))
h₁ : log (Γ (x / 2 + 1 / 2)) = log (Γ (x * (1 / 2) + 1 / 2))
h₂ h₃ : log (Γ (x / 2 + 1 / 2)) = log (Γ (x / 2 + 1 / 2))
⊢ log (Γ (x / 2 + 1 / 2)) = log (Γ ((1 / 2) • x + 1 / 2))

Tactic:
rw [smul_eq_mul, mul_comm, mul_one_div]

Premises used: mul_one_div, mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
⊢ ConvexOn ℝ (β := ℝ) (Ioi 0) fun (s : ℝ) ↦ s * log 2

Tactic:
simpa only [mul_comm _ (log _)] using
      (convexOn_id (convex_Ioi (0 : ℝ))).smul (log_pos one_lt_two).le

Premises used: ConvexOn.smul, convexOn_id, Real.log_pos, LT.lt.le, Real.log, mul_comm, one_lt_two, OfNat.ofNat, convex_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : 0 < s
⊢ s.doublingGamma = Γ s

Tactic:
eq_Gamma_of_log_convex doublingGamma_log_convex_Ioi
      (fun {y} hy => doublingGamma_add_one y hy.ne') (fun {y} hy => ?_) doublingGamma_one hs

Premises used: Real.doublingGamma_log_convex_Ioi, LT.lt.ne', Real.doublingGamma_add_one, Real.doublingGamma_one, Real.eq_Gamma_of_log_convex
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : 0 < s
eq_Gamma_of_log_convex : ∀ {y : ℝ} (hy : 0 < y), 0 < y.doublingGamma
⊢ s.doublingGamma = Γ s

Tactic:
refine
    eq_Gamma_of_log_convex doublingGamma_log_convex_Ioi
      (fun {y} hy => doublingGamma_add_one y hy.ne') (fun {y} hy => ?_) doublingGamma_one hs

Premises used: Real.doublingGamma_log_convex_Ioi, LT.lt.ne', Real.doublingGamma_add_one, Real.doublingGamma_one, Real.eq_Gamma_of_log_convex
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : 0 < s
y : ℝ
hy : 0 < y
⊢ 0 < y.doublingGamma

Tactic:
apply_rules [mul_pos, Gamma_pos_of_pos, add_pos, inv_pos_of_pos, rpow_pos_of_pos, two_pos,
    one_pos, sqrt_pos_of_pos pi_pos]

Premises used: Real.Gamma_pos_of_pos, Real.rpow_pos_of_pos, add_pos, two_pos, Real.pi_pos, inv_pos_of_pos, mul_pos, Real.sqrt_pos_of_pos, one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : 0 < s
⊢ 1 - 2 * s = -(2 * s - 1)

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : 0 < s
rw :
  Γ s * Γ (s + 1 / 2) =
    Γ s * Γ (s + 1 / 2) * HPow.hPow (α := ℝ) 2 (2 * s - 1) / √π * (HPow.hPow (α := ℝ) 2 (2 * s - 1))⁻¹ * √π
⊢ Γ s * Γ (s + 1 / 2) = Γ (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s) * √π

Tactic:
rw [← doublingGamma_eq_Gamma (mul_pos two_pos hs), doublingGamma,
    mul_div_cancel_left₀ _ (two_ne_zero' ℝ), (by abel : 1 - 2 * s = -(2 * s - 1)),
    rpow_neg zero_le_two]

Premises used: Real, Real.doublingGamma_eq_Gamma, two_pos, mul_div_cancel_left₀, mul_pos, two_ne_zero', zero_le_two, Real.rpow_neg, Real.doublingGamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Goal:
s : ℝ
hs : 0 < s
⊢ Γ s * Γ (s + 1 / 2) =
    Γ s * Γ (s + 1 / 2) * HPow.hPow (α := ℝ) 2 (2 * s - 1) / √π * (HPow.hPow (α := ℝ) 2 (2 * s - 1))⁻¹ * √π

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ s.Gammaℝ = (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2)

Tactic:
rfl

Premises used: Complex.Gammaℝ, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ s.Gammaℂ = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s

Tactic:
rfl

Premises used: Complex.Gammaℂ, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : s ≠ 0
rw :
  (↑π : ℂ) ^ (-(s / 2)) * (↑π : ℂ)⁻¹ * (s / 2 * Gamma (s / 2)) = (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * s / 2 / (↑π : ℂ)
⊢ (s + 2).Gammaℝ = s.Gammaℝ * s / 2 / (↑π : ℂ)

Tactic:
rw [Gammaℝ_def, Gammaℝ_def, neg_div, add_div, neg_add, div_self two_ne_zero,
    Gamma_add_one _ (div_ne_zero hs two_ne_zero),
    cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), cpow_neg_one]

Premises used: Iff.mpr, Complex.Gammaℝ_def, neg_div, Complex.Gamma_add_one, Complex.cpow_neg_one, Complex.ofReal_ne_zero, neg_add, div_ne_zero, two_ne_zero, Complex.cpow_add, div_self, Real.pi_ne_zero, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : s ≠ 0
⊢ (↑π : ℂ) ^ (-(s / 2)) * (↑π : ℂ)⁻¹ * (s / 2 * Gamma (s / 2)) = (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * s / 2 / (↑π : ℂ)

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : s ≠ 0
rw :
  2 * ((2 * (↑π : ℂ)) ^ (-s) * (2 * (↑π : ℂ))⁻¹) * (s * Gamma s) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * s / 2 / (↑π : ℂ)
⊢ (s + 1).Gammaℂ = s.Gammaℂ * s / 2 / (↑π : ℂ)

Tactic:
rw [Gammaℂ_def, Gammaℂ_def, Gamma_add_one _ hs, neg_add,
    cpow_add _ _ (mul_ne_zero two_ne_zero (ofReal_ne_zero.mpr pi_ne_zero)), cpow_neg_one]

Premises used: Iff.mpr, Complex.Gamma_add_one, Complex.cpow_neg_one, Complex.ofReal_ne_zero, neg_add, Complex.Gammaℂ_def, two_ne_zero, Complex.cpow_add, mul_ne_zero, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : s ≠ 0
⊢ 2 * ((2 * (↑π : ℂ)) ^ (-s) * (2 * (↑π : ℂ))⁻¹) * (s * Gamma s) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * s / 2 / (↑π : ℂ)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : 0 < s.re
ha : (↑π : ℂ) ^ (-s / 2) ≠ 0
hb : Gamma (s / 2) ≠ 0
⊢ s.Gammaℝ ≠ 0

Tactic:
apply mul_ne_zero

Premises used: mul_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : 0 < s.re
⊢ (↑π : ℂ) ^ (-s / 2) ≠ 0

Tactic:
simp [pi_ne_zero]

Premises used: Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : 0 < s.re
hb : 0 < (s / 2).re
⊢ Gamma (s / 2) ≠ 0

Tactic:
apply Gamma_ne_zero_of_re_pos

Premises used: Complex.Gamma_ne_zero_of_re_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : 0 < s.re
hb : 0 < s.re / 2
⊢ 0 < (s / 2).re

Tactic:
rw [div_ofNat_re]

Premises used: Complex.div_ofNat_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : 0 < s.re
⊢ 0 < s.re / 2

Tactic:
div_pos hs two_pos

Premises used: two_pos, div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : 0 < s.re
⊢ 0 < s.re / 2

Tactic:
exact div_pos hs two_pos

Premises used: two_pos, div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ s.Gammaℝ = 0 ↔ ∃ (n : ℕ), s = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)

Tactic:
simp [Gammaℝ_def, Complex.Gamma_eq_zero_iff, pi_ne_zero, div_eq_iff (two_ne_zero' ℂ), mul_comm]

Premises used: Complex.Gammaℝ_def, two_ne_zero', div_eq_iff, mul_comm, Complex, Complex.Gamma_eq_zero_iff, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
rw : (↑π : ℂ) ^ (-1 / 2) * (↑π : ℂ) ^ (1 / 2) = 1
⊢ Gammaℝ 1 = 1

Tactic:
rw [Gammaℝ_def, Complex.Gamma_one_half_eq]

Premises used: Complex.Gammaℝ_def, Complex.Gamma_one_half_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
⊢ (↑π : ℂ) ^ (-1 / 2) * (↑π : ℂ) ^ (1 / 2) = 1

Tactic:
simp [neg_div, cpow_neg, pi_ne_zero]

Premises used: neg_div, Complex.cpow_neg, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
rw : 2 * (2 * (↑π : ℂ))⁻¹ * 1 = 1 / (↑π : ℂ)
⊢ Gammaℂ 1 = 1 / (↑π : ℂ)

Tactic:
rw [Gammaℂ_def, cpow_neg_one, Complex.Gamma_one]

Premises used: Complex.cpow_neg_one, Complex.Gamma_one, Complex.Gammaℂ_def
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
⊢ 2 * (2 * (↑π : ℂ))⁻¹ * 1 = 1 / (↑π : ℂ)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
h : ∀ (s : ℂ), s.Gammaℝ⁻¹
| Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ s.Gammaℝ⁻¹

Tactic:
enter [2, s]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
h : ((↑π : ℂ) ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹
| s.Gammaℝ⁻¹

Tactic:
rw [Gammaℝ, mul_inv]

Premises used: Complex.Gammaℝ, mul_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
h : ∀ (s : ℂ), ((↑π : ℂ) ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹
| Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ s.Gammaℝ⁻¹

Tactic:
enter [2, s]; rw [Gammaℝ, mul_inv]

Premises used: Complex.Gammaℝ, mul_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
conv : Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ ((↑π : ℂ) ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ s.Gammaℝ⁻¹

Tactic:
conv => enter [2, s]; rw [Gammaℝ, mul_inv]

Premises used: Complex.Gammaℝ, mul_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ (↑π : ℂ) ^ (-s / 2) ≠ 0

Tactic:
simp [pi_ne_zero]

Premises used: Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
refine_1 : ∀ (s : ℂ), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)) s
refine_2 : Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ (Gamma (s / 2))⁻¹
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ ((↑π : ℂ) ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹

Tactic:
refine Differentiable.mul (fun s ↦ .inv ?_ (by simp [pi_ne_zero])) ?_

Premises used: DifferentiableAt.inv, Differentiable.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)) s

Tactic:
((differentiableAt_id.neg.div_const (2 : ℂ)).const_cpow ?_)

Premises used: DifferentiableAt.const_cpow, DifferentiableAt.div_const, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
refine_1 : (↑π : ℂ) ≠ 0 ∨ -s / 2 ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)) s

Tactic:
refine ((differentiableAt_id.neg.div_const (2 : ℂ)).const_cpow ?_)

Premises used: DifferentiableAt.const_cpow, DifferentiableAt.div_const, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ (↑π : ℂ) ≠ 0 ∨ -s / 2 ≠ 0

Tactic:
Or.inl (ofReal_ne_zero.mpr pi_ne_zero)

Premises used: Iff.mpr, Complex.ofReal_ne_zero, Or.inl, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ (↑π : ℂ) ≠ 0 ∨ -s / 2 ≠ 0

Tactic:
exact Or.inl (ofReal_ne_zero.mpr pi_ne_zero)

Premises used: Iff.mpr, Complex.ofReal_ne_zero, Or.inl, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ (Gamma (s / 2))⁻¹

Tactic:
differentiable_one_div_Gamma.comp (differentiable_id.div_const _)

Premises used: Complex.differentiable_one_div_Gamma, Differentiable.div_const, Differentiable.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ (Gamma (s / 2))⁻¹

Tactic:
exact differentiable_one_div_Gamma.comp (differentiable_id.div_const _)

Premises used: Complex.differentiable_one_div_Gamma, Differentiable.div_const, Differentiable.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
⊢ Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)

Tactic:
tendsto_self_mul_Gamma_nhds_zero.comp ?_

Premises used: Complex.tendsto_self_mul_Gamma_nhds_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
refine : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2) (𝓝[≠] 0) (𝓝[≠] 0)
⊢ Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)

Tactic:
refine tendsto_self_mul_Gamma_nhds_zero.comp ?_

Premises used: Complex.tendsto_self_mul_Gamma_nhds_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
⊢ 𝓝 0 = 𝓝 (0 / 2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
rw : Tendsto (fun (z : ℂ) ↦ z / 2) (𝓝[≠] 0) (𝓝 (0 / 2)) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, Membership.mem (γ := Set ℂ) {0}ᶜ (n / 2)
⊢ Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2) (𝓝[≠] 0) (𝓝[≠] 0)

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

Premises used: tendsto_nhdsWithin_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
⊢ Tendsto (fun (z : ℂ) ↦ z / 2) (𝓝[≠] 0) (𝓝 (0 / 2)) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, Membership.mem (γ := Set ℂ) {0}ᶜ (n / 2)

Tactic:
⟨(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⟩

Premises used: Filter.tendsto_id, div_ne_zero, Filter.Tendsto.div_const, Filter.eventually_of_mem, two_ne_zero, nhdsWithin_le_nhds, self_mem_nhdsWithin, And.intro, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
⊢ Tendsto (fun (z : ℂ) ↦ z / 2) (𝓝[≠] 0) (𝓝 (0 / 2)) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, Membership.mem (γ := Set ℂ) {0}ᶜ (n / 2)

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⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
⊢ Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)

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⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ 𝓝 2 = 𝓝 (2 * (↑π : ℂ) ^ (-0 / 2))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
rw : Tendsto (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 (2 * (↑π : ℂ) ^ (-0 / 2)))
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)

Tactic:
rw [(by simp : 𝓝 2 = 𝓝 (2 * (π : ℂ) ^ (-(0 : ℂ) / 2)))]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 (2 * (↑π : ℂ) ^ (-0 / 2)))

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

Premises used: nhdsWithin_le_nhds, ContinuousAt.tendsto, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
refine : ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) 0
⊢ Tendsto (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 (2 * (↑π : ℂ) ^ (-0 / 2)))

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

Premises used: nhdsWithin_le_nhds, ContinuousAt.tendsto, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
funProp funProp₁ : Ne (α := ℂ) 2 0
⊢ ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ -s / 2) 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) 0

Tactic:
exact continuousAt_const.mul ((continuousAt_const_cpow (ofReal_ne_zero.mpr pi_ne_zero)).comp
      (by fun_prop))

Premises used: continuousAt_const_cpow, Iff.mpr, Complex.ofReal_ne_zero, continuousAt_const, ContinuousAt.mul, ContinuousAt.comp, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) (𝓝[≠] 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
      (by fun_prop))
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (β := ℂ) (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
h₁ : ∀ (z : ℂ), z * z.Gammaℝ = 2 * (↑π : ℂ) ^ (-z / 2) * (z / 2 * Gamma (z / 2))
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)

Tactic:
convert! mul_one (2 : ℂ) ▸ (h'.mul h) using 2 with z
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ((↑π : ℂ) ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
rw :
  (↑π : ℂ) ^ (-s / 2 + -(s + 1) / 2) *
      (Gamma (2 * (s / 2)) * HPow.hPow (α := ℂ) 2 (1 - 2 * (s / 2)) * (↑π : ℂ) ^ HDiv.hDiv (α := ℂ) 1 2) =
    HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s
⊢ (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) =
    HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s

Tactic:
rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
      sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]

Premises used: Iff.mpr, Complex.ofReal_cpow, Complex.ofReal_ne_zero, Real.pi_pos, LT.lt.le, Complex.ofReal_one, Complex.cpow_add, Complex.ofReal_div, Complex.Gamma_mul_Gamma_add_half, Complex.ofReal_ofNat, Real.sqrt_eq_rpow, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ (↑π : ℂ) ^ (-s / 2 + -(s + 1) / 2) *
      (Gamma (2 * (s / 2)) * HPow.hPow (α := ℂ) 2 (1 - 2 * (s / 2)) * (↑π : ℂ) ^ HDiv.hDiv (α := ℂ) 1 2) =
    HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
rw :
  2 * HPow.hPow (α := ℂ) 2 (-s) * (↑π : ℂ) ^ (-1 / 2 - s + 1 / 2) * Gamma s =
    2 * (HPow.hPow (α := ℂ) 2 (-s) * (↑π : ℂ) ^ (-s)) * Gamma s
⊢ HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s =
    2 * ((↑2 : ℂ) ^ (-s) * (↑π : ℂ) ^ (-s)) * Gamma s

Tactic:
rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
      ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]

Premises used: Iff.mpr, sub_eq_add_neg, Complex.ofReal_ne_zero, two_ne_zero, Complex.cpow_one, Complex.cpow_add, Complex.ofReal_ofNat, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ 2 * HPow.hPow (α := ℂ) 2 (-s) * (↑π : ℂ) ^ (-1 / 2 - s + 1 / 2) * Gamma s =
    2 * (HPow.hPow (α := ℂ) 2 (-s) * (↑π : ℂ) ^ (-s)) * Gamma s

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
rw : 2 * ((↑2 : ℂ) * (↑π : ℂ)) ^ (-s) * Gamma s = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
rw₁ rw₂ : 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
⊢ 2 * ((↑2 : ℂ) ^ (-s) * (↑π : ℂ) ^ (-s)) * Gamma s = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s

Tactic:
rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]

Premises used: two_pos, Real.pi_pos, LT.lt.le, Complex.mul_cpow_ofReal_nonneg, Complex.ofReal_ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
_ :
  (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ((↑π : ℂ) ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2))
_₁ :
  (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) =
    HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s
_₂ :
  HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s =
    2 * ((↑2 : ℂ) ^ (-s) * (↑π : ℂ) ^ (-s)) * Gamma s
_₃ : 2 * ((↑2 : ℂ) ^ (-s) * (↑π : ℂ) ^ (-s)) * Gamma s = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
⊢ (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ((↑π : ℂ) ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s

Tactic:
calc
  _ = (π ^ (-s / 2) * π ^ (-(s + 1) / 2)) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) := by ring_nf
  _ = 2 ^ (1 - s) * (π ^ (-1 / 2 - s) * π ^ (1 / 2 : ℂ)) * Gamma s := by
    rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
      sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
    ring_nf
  _ = 2 * ((2 : ℝ) ^ (-s) * π ^ (-s)) * Gamma s := by
    rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
      ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]
    ring_nf
  _ = 2 * (2 * π) ^ (-s) * Gamma s := by
    rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]

Premises used: Real.pi, HMul.hMul, HSub.hSub, Complex.Gamma, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ (↑π : ℂ) ^ (-(1 - s) / 2) * Gamma ((1 - s) / 2) * ((↑π : ℂ) ^ (-(1 + s) / 2) * Gamma ((1 + s) / 2)) =
    (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
rw :
  (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * ((↑π : ℂ) / sin ((↑π : ℂ) * ((1 - s) / 2))) =
    (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * (↑π : ℂ) / sin ((↑π : ℂ) / 2 - (↑π : ℂ) * s / 2)
⊢ (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2)) =
    (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * HPow.hPow (β := ℂ) (↑π : ℂ) 1 /
      sin ((↑π : ℂ) / 2 - (↑π : ℂ) * s / 2)

Tactic:
rw [Complex.Gamma_mul_Gamma_one_sub, cpow_one]

Premises used: Complex.cpow_one, Complex.Gamma_mul_Gamma_one_sub