awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hn : n ≠ 0
x : ℕ
h : x ∈ Finset.range n
⊢ s + 1 + (↑x : ℂ) = s + (↑(x + 1) : ℂ)
have e_a : s + 1 + (↑x : ℂ) = s + HAdd.hAdd (α := ℂ) (↑x : ℂ) 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ x = x / (↑n : ℝ) * (↑n : ℝ)
have h : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: rw [div_mul_cancel₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
⊢ s.GammaSeq n = ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
| ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
have h : ∀ (x : ℝ), (↑x : ℂ)
Tactic: enter [1, x, 2, 1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
x : ℝ
| (↑x : ℂ)
have h : (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ)
Tactic: rw [this x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
| ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
have h : ∀ (x : ℝ), (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ)
Tactic: enter [1, x, 2, 1]; rw [this x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
⊢ s.GammaSeq n = ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
have conv_rhs : s.GammaSeq n = ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1)
Tactic: conv_rhs => enter [1, x, 2, 1]; rw [this x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
⊢ s.GammaSeq n = ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1)
have rw : 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 [GammaSeq_eq_betaIntegral_of_re_pos hs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / (↑n : ℝ) * (↑n : ℝ)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
    ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1)
have this₁ : ∫ (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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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))
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
    ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1)
have 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)))
Tactic: rw [betaIntegral, this, real_smul, zero_div, div_self, add_sub_cancel_right,
    ← intervalIntegral.integral_const_mul, ← intervalIntegral.integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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)))
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) s * s.betaIntegral (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
    ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑(x / (↑n : ℝ) * (↑n : ℝ)) : ℂ) ^ (s - 1)
have rw₁ : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: rw [betaIntegral, this, real_smul, zero_div, div_self, add_sub_cancel_right,
    ← intervalIntegral.integral_const_mul, ← intervalIntegral.integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 (α := ℂ)
    (∫ (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)))
have 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)))
Tactic: simp_rw [intervalIntegral.integral_of_le zero_le_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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)))
have 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))
Tactic: refine setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)) =
    (↑(↑n : ℝ) : ℂ) * ((↑((1 - x) ^ n) : ℂ) * (↑(x * (↑n : ℝ)) : ℂ) ^ (s - 1))
have push_cast : HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)) =
  (↑n : ℂ) * ((1 - (↑x : ℂ)) ^ n * ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
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
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)) =
    (↑n : ℂ) * ((1 - (↑x : ℂ)) ^ n * ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1))
have hn' : Ne (α := ℂ) (↑n : ℂ) 0
Tactic: have hn' : (n : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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
have rw : HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1
Tactic: rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 : ℂ)
have conv_lhs : HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1 =
  HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1) * (↑n : ℂ)
Tactic: conv_lhs => rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
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 * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)) =
    (↑n : ℂ) * ((1 - (↑x : ℂ)) ^ n * ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1))
have A : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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)
have rw : ((↑x : ℂ) * (↑(↑n : ℝ) : ℂ)) ^ (s - 1) = (↑x : ℂ) ^ (s - 1) * (↑(↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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)
⊢ ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1) = (↑x : ℂ) ^ (s - 1) * HPow.hPow (α := ℂ) (↑n : ℂ) (s - 1)
have rw₁ : (↑x : ℂ) ^ (s - 1) * (↑(↑n : ℝ) : ℂ) ^ (s - 1) = (↑x : ℂ) ^ (s - 1) * (↑(↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
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 : ℂ)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) s * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)) =
    (↑n : ℂ) * ((1 - (↑x : ℂ)) ^ n * ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1))
have B : ((↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
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 * ((↑x : ℂ) ^ (s - 1) * HPow.hPow (β := ℂ) (1 - (↑x : ℂ)) (↑n : ℂ)) =
    (↑n : ℂ) * ((1 - (↑x : ℂ)) ^ n * ((↑x : ℂ) * (↑n : ℂ)) ^ (s - 1))
have 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)))
Tactic: rw [A, B, cpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 (Gamma s))
have rw : Tendsto (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
  (𝓝 s.GammaIntegral)
Tactic: rw [Gamma_eq_integral hs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
have rw : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) volume 0 (↑n : ℝ)
Tactic: rw [integrable_indicator_iff (measurableSet_Ioc : MeasurableSet (Ioc (_ : ℝ) _)), IntegrableOn,
      Measure.restrict_restrict_of_subset Ioc_subset_Ioi_self, ← IntegrableOn, ←
      intervalIntegrable_iff_integrableOn_Ioc_of_le (by positivity : (0 : ℝ) ≤ n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) volume 0 (↑n : ℝ)
have hf : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) volume 0 (↑n : ℝ)
Tactic: apply IntervalIntegrable.continuousOn_mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
hf : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) volume 0 (↑n : ℝ)
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) volume 0 (↑n : ℝ)
have hg : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ)) (uIcc 0 (↑n : ℝ))
Tactic: apply IntervalIntegrable.continuousOn_mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) volume 0 (↑n : ℝ)
have hf : -1 < (s - 1).re
Tactic: refine intervalIntegral.intervalIntegrable_cpow' ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
⊢ -1 < (s - 1).re
have hf : -1 < s.re - re 1
Tactic: rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
hf : -1 < s.re - re 1
⊢ -1 < (s - 1).re
have hf₁ : -1 < s.re - 1
Tactic: rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
hf : -1 < s.re - re 1
hf₁ : -1 < s.re - 1
⊢ -1 < (s - 1).re
have hf₂ : HSub.hSub (α := ℝ) 0 1 < s.re - 1
Tactic: rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
n : ℕ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ)) (uIcc 0 (↑n : ℝ))
have funProp : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (uIcc 0 (↑n : ℝ)) x → Ne (α := ℝ) (↑n : ℝ) 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 s.GammaIntegral)
have f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
Tactic: have f_ible : ∀ n : ℕ, Integrable (f n) (volume.restrict (Ioi 0)) := by
    intro n
    rw [integrable_indicator_iff (measurableSet_Ioc : MeasurableSet (Ioc (_ : ℝ) _)), IntegrableOn,
      Measure.restrict_restrict_of_subset Ioc_subset_Ioi_self, ← IntegrableOn, ←
      intervalIntegrable_iff_integrableOn_Ioc_of_le (by positivity : (0 : ℝ) ≤ n)]
    apply IntervalIntegrable.continuousOn_mul
    · refine intervalIntegral.intervalIntegrable_cpow' ?_
      rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
    · fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
have hl : EventuallyEq (β := ℂ) atTop (fun (n : ℕ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) fun (n : ℕ) ↦ f n x
Tactic: apply Tendsto.congr'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hl :
  EventuallyEq (β := ℂ) atTop (fun (n : ℕ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) fun (n : ℕ) ↦ f n x
⊢ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
have h : Tendsto (fun (n : ℕ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
  (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
Tactic: apply Tendsto.congr'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ :=
  fun (n : ℕ) ↦ indicator (Ioc 0 (↑n : ℝ)) fun (x : ℝ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)
f_ible : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (f n) (Measure.restrict volume (Ioi 0))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hl :
  EventuallyEq (β := ℂ) atTop (fun (n : ℕ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) fun (n : ℕ) ↦ f n x
h :
  Tendsto (fun (n : ℕ) ↦ (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) atTop
    (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
⊢ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
have f₁ : ℕ → ℂ
Tactic: apply Tendsto.congr'