awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
this : s = (↑s.re : ℂ)
pos : ∀ (n : ℕ), s.re ≠ -(↑n : ℝ)
⊢ Real.Gamma s.re ≠ 0

Tactic:
refine Real.Gamma_ne_zero fun n => ?_

Premises used: Real.Gamma_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
this : s = (↑s.re : ℂ)
n : ℕ
⊢ s ≠ -(↑n : ℂ)

Tactic:
specialize hs n
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h_im : s.im = 0
this : s = (↑s.re : ℂ)
n : ℕ
hs : s ≠ -(↑n : ℂ)
pos : ∀ (hs : s.re = -(↑n : ℝ)), s = -(↑n : ℂ)
⊢ s.re ≠ -(↑n : ℝ)

Tactic:
contrapose hs
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h_im : s.im = 0
this : s = (↑s.re : ℂ)
n : ℕ
hs : s.re = -(↑n : ℝ)
pos : (↑s.re : ℂ) = -(↑n : ℂ)
pos₁ : (↑s.re : ℂ) = -(↑(↑n : ℝ) : ℂ)
pos₂ : (↑s.re : ℂ) = (↑(-(↑n : ℝ)) : ℂ)
pos₃ pos₄ pos₅ pos₆ : s.re = -(↑n : ℝ)
⊢ s = -(↑n : ℂ)

Tactic:
rwa [this, ← ofReal_natCast, ← ofReal_neg, ofReal_inj]

Premises used: Complex.ofReal_neg, Complex.ofReal_natCast, Complex.ofReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
rw : ∀ (k : ℤ), (↑π : ℂ) * s ≠ (↑k : ℂ) * (↑π : ℂ)
⊢ sin ((↑π : ℂ) * s) ≠ 0

Tactic:
rw [Complex.sin_ne_zero_iff]

Premises used: Complex.sin_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
k : ℤ
apply_fun : ((↑π : ℂ) * s).im ≠ ((↑k : ℂ) * (↑π : ℂ)).im
⊢ (↑π : ℂ) * s ≠ (↑k : ℂ) * (↑π : ℂ)

Tactic:
apply_fun im

Premises used: Complex.im
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
k : ℤ
rw : π * s.im ≠ 0
⊢ ((↑π : ℂ) * s).im ≠ ((↑k : ℂ) * (↑π : ℂ)).im

Tactic:
rw [im_ofReal_mul, ← ofReal_intCast, ← ofReal_mul, ofReal_im]

Premises used: Complex.ofReal_intCast, Complex.im_ofReal_mul, Complex.ofReal_im, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
k : ℤ
⊢ π * s.im ≠ 0

Tactic:
mul_ne_zero Real.pi_pos.ne' h_im

Premises used: Real.pi_pos, LT.lt.ne', mul_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
k : ℤ
⊢ π * s.im ≠ 0

Tactic:
exact mul_ne_zero Real.pi_pos.ne' h_im

Premises used: Real.pi_pos, LT.lt.ne', mul_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
⊢ sin ((↑π : ℂ) * s) ≠ 0

Tactic:
have : sin (↑π * s) ≠ 0 := by
      rw [Complex.sin_ne_zero_iff]
      intro k
      apply_fun im
      rw [im_ofReal_mul, ← ofReal_intCast, ← ofReal_mul, ofReal_im]
      exact mul_ne_zero Real.pi_pos.ne' h_im
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
this : sin ((↑π : ℂ) * s) ≠ 0
⊢ (↑π : ℂ) / sin ((↑π : ℂ) * s) ≠ 0

Tactic:
have A := div_ne_zero (ofReal_ne_zero.mpr Real.pi_pos.ne') this
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
this : sin ((↑π : ℂ) * s) ≠ 0
A : (↑π : ℂ) / sin ((↑π : ℂ) * s) ≠ 0
⊢ Gamma s ≠ 0 ∧ Gamma (1 - s) ≠ 0

Tactic:
rw [← Complex.Gamma_mul_Gamma_one_sub s, mul_ne_zero_iff] at A

Premises used: Complex.Gamma_mul_Gamma_one_sub, mul_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
this : sin ((↑π : ℂ) * s) ≠ 0
A : Gamma s ≠ 0 ∧ Gamma (1 - s) ≠ 0
⊢ Gamma s ≠ 0

Tactic:
A.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
this : sin ((↑π : ℂ) * s) ≠ 0
A : Gamma s ≠ 0 ∧ Gamma (1 - s) ≠ 0
⊢ Gamma s ≠ 0

Tactic:
exact A.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
mp : Gamma s = 0 → ∃ (m : ℕ), s = -(↑m : ℂ)
mpr : (∃ (m : ℕ), s = -(↑m : ℂ)) → Gamma s = 0
⊢ Gamma s = 0 ↔ ∃ (m : ℕ), s = -(↑m : ℂ)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
mp : (∀ (m : ℕ), s ≠ -(↑m : ℂ)) → Gamma s ≠ 0
⊢ Gamma s = 0 → ∃ (m : ℕ), s = -(↑m : ℂ)

Tactic:
contrapose!
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
⊢ (∀ (m : ℕ), s ≠ -(↑m : ℂ)) → Gamma s ≠ 0

Tactic:
Gamma_ne_zero

Premises used: Complex.Gamma_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
⊢ (∀ (m : ℕ), s ≠ -(↑m : ℂ)) → Gamma s ≠ 0

Tactic:
exact Gamma_ne_zero

Premises used: Complex.Gamma_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
⊢ Gamma (-(↑m : ℂ)) = 0

Tactic:
Gamma_neg_nat_eq_zero m

Premises used: Complex.Gamma_neg_nat_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
⊢ Gamma (-(↑m : ℂ)) = 0

Tactic:
exact Gamma_neg_nat_eq_zero m

Premises used: Complex.Gamma_neg_nat_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
⊢ Gamma s ≠ 0

Tactic:
Gamma_ne_zero fun m => ?_

Premises used: Complex.Gamma_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
refine : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ Gamma s ≠ 0

Tactic:
refine Gamma_ne_zero fun m => ?_

Premises used: Complex.Gamma_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
m : ℕ
contrapose! : ∀ (hs : s = -(↑m : ℂ)), s.re ≤ 0
⊢ s ≠ -(↑m : ℂ)

Tactic:
contrapose! hs
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
m : ℕ
hs : s = -(↑m : ℂ)
⊢ s.re ≤ 0

Tactic:
simpa only [hs, neg_re, ← ofReal_natCast, ofReal_re, neg_nonpos] using Nat.cast_nonneg _

Premises used: Nat.cast_nonneg, neg_nonpos, Complex.neg_re, Complex.ofReal_natCast, Complex.ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
this : Tendsto (Complex.ofReal ∘ s.GammaSeq) atTop (𝓝 (Complex.Gamma (↑s : ℂ)))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
(Complex.continuous_re.tendsto (Complex.Gamma ↑s)).comp this

Premises used: Complex.continuous_re, Complex.Gamma, Complex.ofReal, Real.GammaSeq, Continuous.tendsto, Real.Gamma, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
this : Tendsto (Complex.ofReal ∘ s.GammaSeq) atTop (𝓝 (Complex.Gamma (↑s : ℂ)))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
exact (Complex.continuous_re.tendsto (Complex.Gamma ↑s)).comp this

Premises used: Complex.continuous_re, Complex.Gamma, Complex.ofReal, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
suffices : Tendsto (Complex.ofReal ∘ s.GammaSeq) atTop (𝓝 (Complex.Gamma (↑s : ℂ)))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
suffices Tendsto ((↑) ∘ GammaSeq s : ℕ → ℂ) atTop (𝓝 <| Complex.Gamma s) by
    exact (Complex.continuous_re.tendsto (Complex.Gamma ↑s)).comp this
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
⊢ Tendsto (↑s : ℂ).GammaSeq atTop (𝓝 (Complex.Gamma (↑s : ℂ)))

Tactic:
Complex.GammaSeq_tendsto_Gamma s

Premises used: Complex.GammaSeq_tendsto_Gamma, Complex.ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
h : Complex.ofReal ∘ s.GammaSeq = (↑s : ℂ).GammaSeq
⊢ Tendsto (Complex.ofReal ∘ s.GammaSeq) atTop (𝓝 (Complex.Gamma (↑s : ℂ)))

Tactic:
convert! Complex.GammaSeq_tendsto_Gamma s

Premises used: Complex.GammaSeq_tendsto_Gamma, Complex.ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
h : ∀ (n : ℕ), (Complex.ofReal ∘ s.GammaSeq) n = (↑s : ℂ).GammaSeq n
⊢ Complex.ofReal ∘ s.GammaSeq = (↑s : ℂ).GammaSeq

Tactic:
ext1 n
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
n : ℕ
h :
  (↑(HPow.hPow (α := ℝ) (↑n : ℝ) s) : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ))
⊢ (↑(HPow.hPow (α := ℝ) (↑n : ℝ) s * (↑n ! : ℝ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℝ))) : ℂ) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑j : ℂ))

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
n : ℕ
h :
  (↑(↑n : ℝ) : ℂ) ^ (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ))
h₁ h₂ :
  HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ))
⊢ (↑(HPow.hPow (α := ℝ) (↑n : ℝ) s) : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ))

Tactic:
rw [Complex.ofReal_cpow n.cast_nonneg, Complex.ofReal_natCast]

Premises used: Nat.cast_nonneg, Complex.ofReal_cpow, Complex.ofReal_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
simp_rw : Complex.Gamma (↑s : ℂ) * Complex.Gamma (1 - (↑s : ℂ)) = (↑π : ℂ) / Complex.sin ((↑π : ℂ) * (↑s : ℂ))
⊢ Gamma s * Gamma (1 - s) = π / sin (π * s)

Tactic:
simp_rw [← Complex.ofReal_inj, Complex.ofReal_div, Complex.ofReal_sin, Complex.ofReal_mul, ←
    Complex.Gamma_ofReal, Complex.ofReal_sub, Complex.ofReal_one]

Premises used: Complex.ofReal_one, Complex.ofReal_div, Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_sin, Complex.Gamma_ofReal, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
⊢ Complex.Gamma (↑s : ℂ) * Complex.Gamma (1 - (↑s : ℂ)) = (↑π : ℂ) / Complex.sin ((↑π : ℂ) * (↑s : ℂ))

Tactic:
Complex.Gamma_mul_Gamma_one_sub s

Premises used: Complex.ofReal, Complex.Gamma_mul_Gamma_one_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℝ
⊢ Complex.Gamma (↑s : ℂ) * Complex.Gamma (1 - (↑s : ℂ)) = (↑π : ℂ) / Complex.sin ((↑π : ℂ) * (↑s : ℂ))

Tactic:
exact Complex.Gamma_mul_Gamma_one_sub s

Premises used: Complex.ofReal, Complex.Gamma_mul_Gamma_one_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
inl : ∀ (h : s ≠ 0), (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
inr : (Gamma 0)⁻¹ = 0 * (Gamma (HAdd.hAdd (α := ℂ) 0 1))⁻¹
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹

Tactic:
rcases ne_or_eq s 0 with (h | rfl)

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h : s ≠ 0
inl : (Gamma s)⁻¹ = s * (s * Gamma s)⁻¹
inl₁ : (Gamma s)⁻¹ = s * (s⁻¹ * (Gamma s)⁻¹)
inl₂ inl₃ : (Gamma s)⁻¹ = (Gamma s)⁻¹
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹

Tactic:
rw [Gamma_add_one s h, mul_inv, mul_inv_cancel_left₀ h]

Premises used: mul_inv_cancel_left₀, Complex.Gamma_add_one, mul_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
inr : (Gamma 0)⁻¹ = 0 * (Gamma 1)⁻¹
inr₁ : 0⁻¹ = 0 * (Gamma 1)⁻¹
inr₂ : 0 = 0 * (Gamma 1)⁻¹
inr₃ inr₄ : Eq (α := ℂ) 0 0
⊢ (Gamma 0)⁻¹ = 0 * (Gamma (HAdd.hAdd (α := ℂ) 0 1))⁻¹

Tactic:
rw [zero_add, Gamma_zero, inv_zero, zero_mul]

Premises used: inv_zero, MulZeroClass.zero_mul, zero_add, Complex.Gamma_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
rcases : ∀ (n : ℕ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s

Tactic:
rcases exists_nat_gt (-s.re) with ⟨n, hs⟩

Premises used: Complex.re, exists_nat_gt, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : -s.re < (↑0 : ℝ)
⊢ 0 < s.re

Tactic:
rw [Nat.cast_zero, neg_lt_zero] at hs

Premises used: neg_lt_zero, Nat.cast_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
zero : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s

Tactic:
suffices ∀ m : ℕ, s ≠ -↑m from (differentiableAt_Gamma _ this).inv (Gamma_ne_zero this)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
hs : 0 < re (-(↑m : ℂ))
zero : re (-(↑m : ℂ)) ≤ 0
⊢ False

Tactic:
apply hs.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
m : ℕ
hs : 0 < re (-(↑m : ℂ))
⊢ re (-(↑m : ℂ)) ≤ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
ihn : ∀ (s : ℂ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < (↑(n + 1) : ℝ)
succ : DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x * (Gamma (x + 1))⁻¹) s
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s

Tactic:
rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]

Premises used: Complex.one_div_Gamma_eq_self_mul_one_div_Gamma_add_one, funext
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
ihn : ∀ (s : ℂ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < (↑(n + 1) : ℝ)
rwa : -(s.re + re 1) < (↑n : ℝ)
rwa₁ : -(s.re + 1) < (↑n : ℝ)
rwa₂ : -s.re - 1 < (↑n : ℝ)
rwa₃ : -s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₄ rwa₅ rwa₆ rwa₇ : -s.re < (↑n.succ : ℝ)
⊢ -(s + 1).re < (↑n : ℝ)

Tactic:
rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ]

Premises used: Nat.cast_succ, Complex.add_re, neg_add', sub_lt_iff_lt_add, Complex.one_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
ihn : ∀ (s : ℂ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < (↑(n + 1) : ℝ)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) (s + 1)

Tactic:
specialize ihn (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
s : ℂ
hs : -s.re < (↑(n + 1) : ℝ)
ihn : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) (s + 1)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x * (Gamma (x + 1))⁻¹) s

Tactic:
differentiableAt_id.mul (ihn.comp s (f := fun s => s + 1) <|
      differentiableAt_id.add_const (1 : ℂ))

Premises used: DifferentiableAt.mul, DifferentiableAt.add_const, DifferentiableAt.comp, OfNat.ofNat, differentiableAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
n : ℕ
s : ℂ
hs : -s.re < (↑(n + 1) : ℝ)
ihn : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) (s + 1)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x * (Gamma (x + 1))⁻¹) s

Tactic:
exact differentiableAt_id.mul (ihn.comp s (f := fun s => s + 1) <|
      differentiableAt_id.add_const (1 : ℂ))

Premises used: DifferentiableAt.mul, DifferentiableAt.add_const, DifferentiableAt.comp, OfNat.ofNat, differentiableAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hs : -s.re < (↑n : ℝ)
zero : ∀ (s : ℂ) (hs : -s.re < (↑0 : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
succ :
  ∀ (n : ℕ) (ihn : ∀ (s : ℂ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s) (s : ℂ)
    (hs : -s.re < (↑(n + 1) : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s

Tactic:
induction n generalizing s with
  | zero =>
    rw [Nat.cast_zero, neg_lt_zero] at hs
    suffices ∀ m : ℕ, s ≠ -↑m from (differentiableAt_Gamma _ this).inv (Gamma_ne_zero this)
    rintro m rfl
    apply hs.not_ge
    simp
  | succ n ihn =>
    rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]
    specialize ihn (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])
    exact differentiableAt_id.mul (ihn.comp s (f := fun s => s + 1) <|
      differentiableAt_id.add_const (1 : ℂ))

Premises used: Complex.one_div_Gamma_eq_self_mul_one_div_Gamma_add_one, neg_lt_zero, funext, Nat.cast_zero, LT.lt.not_ge, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
rw : u.betaIntegral v = Gamma (u + v) * u.betaIntegral v / Gamma (u + v)
rw₁ rw₂ : u.betaIntegral v = u.betaIntegral v
⊢ u.betaIntegral v = Gamma u * Gamma v / Gamma (u + v)

Tactic:
rw [Gamma_mul_Gamma_eq_betaIntegral hu hv,
      mul_div_cancel_left₀ _ (Gamma_ne_zero_of_re_pos (add_pos hu hv))]

Premises used: mul_div_cancel_left₀, Complex.Gamma_ne_zero_of_re_pos, Complex.Gamma_mul_Gamma_eq_betaIntegral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
⊢ ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹ = ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) / (↑√π : ℂ))⁻¹

Tactic:
congr_arg Inv.inv (congr_fun this s)

Premises used: congr_arg, Inv.inv, congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h : Gamma s * Gamma (s + 1 / 2) = ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹
h₁ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) / (↑√π : ℂ))⁻¹
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ)

Tactic:
convert! congr_arg Inv.inv (congr_fun this s) using 1

Premises used: congr_arg, Inv.inv, congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h : Gamma s * Gamma (s + 1 / 2) = (Gamma s)⁻¹⁻¹ * (Gamma (s + 1 / 2))⁻¹⁻¹
h₁ : Gamma s * Gamma (s + 1 / 2) = Gamma s * (Gamma (s + 1 / 2))⁻¹⁻¹
h₂ h₃ : Gamma s * Gamma (s + 1 / 2) = Gamma s * Gamma (s + 1 / 2)
⊢ Gamma s * Gamma (s + 1 / 2) = ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹

Tactic:
rw [mul_inv, inv_inv, inv_inv]

Premises used: mul_inv, inv_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) * (↑√π : ℂ)⁻¹)⁻¹
h₁ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₂ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    (Gamma (2 * s))⁻¹⁻¹ * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₃ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    Gamma (2 * s) * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₄ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    Gamma (2 * s) * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)
h₅ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (-(2 * s - 1)) * (↑√π : ℂ)
h₆ h₇ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ)
⊢ Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) / (↑√π : ℂ))⁻¹

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

Premises used: neg_sub, mul_inv, Complex.cpow_neg, div_eq_mul_inv, inv_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
suffices :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ)

Tactic:
suffices (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z =>
      (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(√π) by
    convert! congr_arg Inv.inv (congr_fun this s) using 1
    · rw [mul_inv, inv_inv, inv_inv]
    · rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
⊢ AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ

Tactic:
DifferentiableOn.analyticOnNhd ?_ isOpen_univ

Premises used: isOpen_univ, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
refine : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ

Tactic:
refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ

Premises used: isOpen_univ, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ

Tactic:
(differentiable_one_div_Gamma.mul ?_).differentiableOn

Premises used: Complex.differentiable_one_div_Gamma, Differentiable.differentiableOn, Differentiable.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
refine : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (z + 1 / 2))⁻¹
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ

Tactic:
refine (differentiable_one_div_Gamma.mul ?_).differentiableOn

Premises used: Complex.differentiable_one_div_Gamma, Differentiable.differentiableOn, Differentiable.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (z + 1 / 2))⁻¹

Tactic:
differentiable_one_div_Gamma.comp (differentiable_id.add (differentiable_const _))

Premises used: differentiable_const, Complex.differentiable_one_div_Gamma, differentiable_id, Differentiable.comp, Differentiable.add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (z + 1 / 2))⁻¹

Tactic:
exact differentiable_one_div_Gamma.comp (differentiable_id.add (differentiable_const _))

Premises used: differentiable_const, Complex.differentiable_one_div_Gamma, differentiable_id, Differentiable.comp, Differentiable.add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
⊢ AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ

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 _))
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ

Tactic:
DifferentiableOn.analyticOnNhd ?_ isOpen_univ

Premises used: isOpen_univ, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
refine :
  DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
⊢ AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ

Tactic:
refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ

Premises used: isOpen_univ, DifferentiableOn.analyticOnNhd
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ

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

Premises used: DivInvMonoid.div', differentiable_const, Differentiable.differentiableOn, Differentiable.mul