awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
rw :
  HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
rw₁ :
  HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) s * HDiv.hDiv (α := ℂ) (↑n ! : ℂ) (∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)))
rw₂ rw₃ :
  HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℂ))
⊢ s.GammaSeq n = HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)

Tactic:
rw [GammaSeq, betaIntegral_eval_nat_add_one_right hs n, ← mul_div_assoc]

Premises used: mul_div_assoc, Complex.GammaSeq, Complex.betaIntegral_eval_nat_add_one_right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
rw :
  HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) /
    ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s)
| (s + 1).GammaSeq n / s

Tactic:
rw [GammaSeq, Finset.prod_range_succ, div_div]

Premises used: Finset.prod_range_succ, Complex.GammaSeq, div_div
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
conv_lhs :
  HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) /
      ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s) =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n
⊢ (s + 1).GammaSeq n / s = (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n

Tactic:
conv_lhs => rw [GammaSeq, Finset.prod_range_succ, div_div]

Premises used: Finset.prod_range_succ, Complex.GammaSeq, div_div
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
rw :
  (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) /
    ((∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ))) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s)
| (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n

Tactic:
rw [GammaSeq, Finset.prod_range_succ', Nat.cast_zero, add_zero, div_mul_div_comm, ← mul_assoc,
      ← mul_assoc, mul_comm _ (Finset.prod _ _)]

Premises used: Finset.prod_range_succ', div_mul_div_comm, mul_assoc, Finset.prod, mul_comm, Complex.GammaSeq, Nat.cast_zero, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
conv_rhs :
  HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) /
      ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s) =
    (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) /
      ((∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ))) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) /
      ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s) =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n

Tactic:
conv_rhs =>
    rw [GammaSeq, Finset.prod_range_succ', Nat.cast_zero, add_zero, div_mul_div_comm, ← mul_assoc,
      ← mul_assoc, mul_comm _ (Finset.prod _ _)]

Premises used: Finset.prod_range_succ', div_mul_div_comm, mul_assoc, Finset.prod, mul_comm, Complex.GammaSeq, Nat.cast_zero, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
e_a : HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
e_a₁ : Eq (α := ℂ) (∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) (∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ)))
e_a₂ : s + 1 + (↑n : ℂ) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) * (↑n ! : ℂ) /
      ((∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) * (s + 1 + (↑n : ℂ)) * s) =
    (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n ! : ℂ) /
      ((∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ))) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s)

Tactic:
congr 3
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
e_a : HPow.hPow (α := ℂ) (↑n : ℂ) s * HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1 = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
e_a₁ : HPow.hPow (α := ℂ) (↑n : ℂ) s * (↑n : ℂ) = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
e_a₂ e_a₃ : (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s + 1) = (↑n : ℂ) * HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
rw [cpow_add _ _ (Nat.cast_ne_zero.mpr hn), cpow_one, mul_comm]

Premises used: Iff.mpr, Complex.cpow_one, Complex.cpow_add, mul_comm, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ Finset.range n = Finset.range n

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
e_a : ∀ x ∈ Finset.range n, s + 1 + (↑x : ℂ) = s + (↑(x + 1) : ℂ)
⊢ Eq (α := ℂ) (∏ x ∈ Finset.range n, (s + 1 + (↑x : ℂ))) (∏ k ∈ Finset.range n, (s + (↑(k + 1) : ℂ)))

Tactic:
refine Finset.prod_congr (by rfl) fun x _ => ?_

Premises used: Finset.prod_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
x : ℕ
h : x ∈ Finset.range n
e_a : s + 1 + (↑x : ℂ) = s + HAdd.hAdd (α := ℂ) (↑x : ℂ) 1
⊢ s + 1 + (↑x : ℂ) = s + (↑(x + 1) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
x : ℕ
h : x ∈ Finset.range n
⊢ s + 1 + (↑x : ℂ) = s + HAdd.hAdd (α := ℂ) (↑x : ℂ) 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ s + 1 + (↑n : ℂ) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
x : ℝ
h : Ne (α := ℝ) (↑n : ℝ) 0
⊢ x = x / (↑n : ℝ) * (↑n : ℝ)

Tactic:
rw [div_mul_cancel₀]

Premises used: div_mul_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
Nat.cast_ne_zero.mpr hn

Premises used: Iff.mpr, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
exact Nat.cast_ne_zero.mpr hn

Premises used: Iff.mpr, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
⊢ ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)

Tactic:
have : ∀ x : ℝ, x = x / n * n := by intro x; rw [div_mul_cancel₀]; exact Nat.cast_ne_zero.mpr hn
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
h : ∀ (x : ℝ), (↑x : ℂ)
| ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)

Tactic:
enter [1, x, 2, 1]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
x : ℝ
h : (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ)
| (↑x : ℂ)

Tactic:
rw [this x]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
h : ∀ (x : ℝ), (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ)
| ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)

Tactic:
enter [1, x, 2, 1]; rw [this x]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
conv_rhs :
  s.GammaSeq n = ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1)
⊢ s.GammaSeq n = ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)

Tactic:
conv_rhs => enter [1, x, 2, 1]; rw [this x]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
rw :
  HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
    ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1)
⊢ s.GammaSeq n = ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1)

Tactic:
rw [GammaSeq_eq_betaIntegral_of_re_pos hs]

Premises used: Complex.GammaSeq_eq_betaIntegral_of_re_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
⊢ ∫ (x : ℝ) in 0..(↑n : ℝ), (fun (x : ℝ) ↦ (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1)) (x / (↑n : ℝ)) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (fun (x : ℝ) ↦ (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1)) x)

Tactic:
have := intervalIntegral.integral_comp_div (a := 0) (b := n)
    (fun x => ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1) : ℝ → ℂ) (Nat.cast_ne_zero.mpr hn)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
rw :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)))
    (∫ (x : ℝ) in 0..1, (↑(↑n : ℝ) : ℂ) * ((↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1)))
rw₁ : Ne (α := ℝ) (↑n : ℝ) 0
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
    ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1)

Tactic:
rw [betaIntegral, this, real_smul, zero_div, div_self, add_sub_cancel_right,
    ← intervalIntegral.integral_const_mul, ← intervalIntegral.integral_const_mul]

Premises used: Complex.real_smul, zero_div, Complex.betaIntegral, add_sub_cancel_right, div_self, intervalIntegral.integral_const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
Nat.cast_ne_zero.mpr hn

Premises used: Iff.mpr, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
exact Nat.cast_ne_zero.mpr hn

Premises used: Iff.mpr, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
simp_rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑(↑n : ℝ) : ℂ) * ((↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1)))
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in 0..1,
      HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)))
    (∫ (x : ℝ) in 0..1, (↑(↑n : ℝ) : ℂ) * ((↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1)))

Tactic:
simp_rw [intervalIntegral.integral_of_le zero_le_one]

Premises used: zero_le_one, intervalIntegral.integral_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑(↑n : ℝ) : ℂ) * ((↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1)))

Tactic:
setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)) =
      (↑(↑n : ℝ) : ℂ) * ((↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑(↑n : ℝ) : ℂ) * ((↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1)))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
push_cast :
  HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)) =
    (↑n : ℂ) * ((1 - (↑x : ℂ)) ^ n * ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1))
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)) =
    (↑(↑n : ℝ) : ℂ) * ((↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
have hn' : (n : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr hn
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hn' : Ne (α := ℂ) (↑n : ℂ) 0
⊢ s = s - 1 + 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hn' : Ne (α := ℂ) (↑n : ℂ) 0
rw : HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1
| HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']

Premises used: Complex.cpow_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hn' : Ne (α := ℂ) (↑n : ℂ) 0
conv_lhs :
  HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1 =
    HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * (↑n : ℂ)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) s = HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * (↑n : ℂ)

Tactic:
conv_lhs => rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']

Premises used: Complex.cpow_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hn' : Ne (α := ℂ) (↑n : ℂ) 0
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1 =
    HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * (↑n : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hn' : Ne (α := ℂ) (↑n : ℂ) 0
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) s = HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * (↑n : ℂ)

Tactic:
have A : (n : ℂ) ^ s = (n : ℂ) ^ (s - 1) * n := by
    conv_lhs => rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']
    simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hn' : Ne (α := ℂ) (↑n : ℂ) 0
A : HPow.hPow (α := ℂ) (↑n : ℂ) s = HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * (↑n : ℂ)
rw : ((↑x : ℂ) * (↑(↑n : ℝ) : ℂ)) ^ (s - 1) = (↑x : ℂ) ^ (s - 1) * (↑(↑n : ℝ) : ℂ) ^ (s - 1)
rw₁ rw₂ : (↑x : ℂ) ^ (s - 1) * (↑(↑n : ℝ) : ℂ) ^ (s - 1) = (↑x : ℂ) ^ (s - 1) * (↑(↑n : ℝ) : ℂ) ^ (s - 1)
⊢ ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1) = (↑x : ℂ) ^ (s - 1) * HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1)

Tactic:
rw [← ofReal_natCast,
      mul_cpow_ofReal_nonneg hx.1.le (Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)).le]

Premises used: Iff.mpr, Nat.cast_pos, LT.lt.le, Complex.mul_cpow_ofReal_nonneg, Nat.pos_of_ne_zero, And.left, Complex.ofReal_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hn' : Ne (α := ℂ) (↑n : ℂ) 0
A : HPow.hPow (α := ℂ) (↑n : ℂ) s = HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * (↑n : ℂ)
⊢ ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1) = (↑x : ℂ) ^ (s - 1) * HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1)

Tactic:
have B : ((x : ℂ) * ↑n) ^ (s - 1) = (x : ℂ) ^ (s - 1) * (n : ℂ) ^ (s - 1) := by
    rw [← ofReal_natCast,
      mul_cpow_ofReal_nonneg hx.1.le (Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)).le]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hn' : Ne (α := ℂ) (↑n : ℂ) 0
A : HPow.hPow (α := ℂ) (↑n : ℂ) s = HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * (↑n : ℂ)
B : ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1) = (↑x : ℂ) ^ (s - 1) * HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1)
rw :
  HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * (↑n : ℂ) * ((↑x : ℂ) ^ (s - 1) * (1 - (↑x : ℂ)) ^ n) =
    (↑n : ℂ) * ((1 - (↑x : ℂ)) ^ n * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1)))
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)) =
    (↑n : ℂ) * ((1 - (↑x : ℂ)) ^ n * ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1))

Tactic:
rw [A, B, cpow_natCast]

Premises used: Complex.cpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this_1 : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
this :
  ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1) =
    HSMul.hSMul (α := ℝ) (β := ℂ) (↑n : ℝ)
      (∫ (x : ℝ) in HDiv.hDiv (α := ℝ) 0 (↑n : ℝ)..HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ),
        (↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hn' : Ne (α := ℂ) (↑n : ℂ) 0
A : HPow.hPow (α := ℂ) (↑n : ℂ) s = HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * (↑n : ℂ)
B : ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1) = (↑x : ℂ) ^ (s - 1) * HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * (↑n : ℂ) * ((↑x : ℂ) ^ (s - 1) * (1 - (↑x : ℂ)) ^ n) =
    (↑n : ℂ) * ((1 - (↑x : ℂ)) ^ n * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1)))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : 0 < s.re
rw :
  Tendsto (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 s.GammaIntegral)
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 (Gamma s))

Tactic:
rw [Gamma_eq_integral hs]

Premises used: Complex.Gamma_eq_integral