awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
e_a : (↑x : ℂ) ^ (s - 1) = ((↑a : ℂ) * (↑(x / a) : ℂ)) ^ (s - 1)
e_a₁ : (↑x : ℂ) ^ (s - 1) = ((↑a : ℂ) * ((↑x : ℂ) / (↑a : ℂ))) ^ (s - 1)
⊢ (↑x : ℂ) ^ (s - 1) = (↑a : ℂ) ^ (s - 1) * (↑(x / a) : ℂ) ^ (s - 1)
have e_a₂ : (↑x : ℂ) ^ (s - 1) = (↑x : ℂ) ^ (s - 1)
Tactic: rw [← mul_cpow_ofReal_nonneg ha.le (div_pos hx.1 ha).le, ofReal_div, mul_div_cancel₀ _ ha']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ 1 - (↑(x / a) : ℂ) = (↑(1 - x / a) : ℂ)
have norm_cast : 1 - x / a = 1 - x / a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = (↑a : ℂ) ^ (t - 1) * (1 - (↑(x / a) : ℂ)) ^ (t - 1)
have e_a : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * (↑(1 - x / a) : ℂ)) ^ (t - 1)
Tactic: rw [(by norm_cast : (1 : ℂ) - ↑(x / a) = ↑(1 - x / a)), ←
      mul_cpow_ofReal_nonneg ha.le (sub_nonneg.mpr <| (div_le_one ha).mpr hx.2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * (↑(1 - x / a) : ℂ)) ^ (t - 1)
have e_a : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * (1 - (↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * (1 - (↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
have e_a : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * 1 - (↑a : ℂ) * ((↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
Tactic: rw [mul_sub, mul_one, mul_div_cancel₀ _ ha']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
e_a : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * 1 - (↑a : ℂ) * ((↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
⊢ ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * (1 - (↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
have e_a₁ : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) - (↑a : ℂ) * ((↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
Tactic: rw [mul_sub, mul_one, mul_div_cancel₀ _ ha']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : (↑a : ℂ) ≠ 0
A : (↑a : ℂ) ^ (s + t - 1) = (↑a : ℂ) * ((↑a : ℂ) ^ (s - 1) * (↑a : ℂ) ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
e_a : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * 1 - (↑a : ℂ) * ((↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
e_a₁ : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) - (↑a : ℂ) * ((↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
⊢ ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) * (1 - (↑x : ℂ) / (↑a : ℂ))) ^ (t - 1)
have e_a₂ : ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1) = ((↑a : ℂ) - (↑x : ℂ)) ^ (t - 1)
Tactic: rw [mul_sub, mul_one, mul_div_cancel₀ _ ha']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
⊢ Gamma s * Gamma t = Gamma (s + t) * s.betaIntegral t
have conv_int : Eq (α := ℂ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (((ContinuousLinearMap.mul ℝ ℂ : (a : ℂ) → ℂ →L[ℝ] ℂ) ((↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1)) :
              ℂ →L[ℝ] ℂ) :
            (a : ℂ) → ℂ)
          ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1)) :
    ℂ)
  (((ContinuousLinearMap.mul ℝ ℂ : (a : ℂ) → ℂ →L[ℝ] ℂ)
          (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
            (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) :
        (a : ℂ) → ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (t - 1)) :
    ℂ)
Tactic: have conv_int := integral_posConvolution
    (GammaIntegral_convergent hs) (GammaIntegral_convergent ht) (ContinuousLinearMap.mul ℝ ℂ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (t - 1))
⊢ Gamma s * Gamma t = Gamma (s + t) * s.betaIntegral t
have hst : 0 < (s + t).re
Tactic: have hst : 0 < re (s + t) := by rw [add_re]; exact add_pos hs ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (t - 1))
hst : 0 < (s + t).re
⊢ Gamma s * Gamma t = Gamma (s + t) * s.betaIntegral t
have rw : Eq (α := ℂ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    ∫ (t_1 : ℝ) in 0..x,
      (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
    (↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s + t - 1) * s.betaIntegral t)
Tactic: rw [Gamma_eq_integral hs, Gamma_eq_integral ht, Gamma_eq_integral hst, GammaIntegral,
    GammaIntegral, GammaIntegral, ← conv_int, ← MeasureTheory.integral_mul_const (betaIntegral _ _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (t - 1))
hst : 0 < (s + t).re
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      (↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s + t - 1) * s.betaIntegral t)
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  ∫ (t_1 : ℝ) in 0..x,
      (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1)) =
    (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s + t - 1) * s.betaIntegral t
Tactic: refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (t - 1))
hst : 0 < (s + t).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ∫ (t_1 : ℝ) in 0..x,
      (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1)) =
    (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s + t - 1) * s.betaIntegral t
have rw : Eq (α := ℂ)
  (∫ (t_1 : ℝ) in 0..x,
    (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1)))
  (∫ (x_1 : ℝ) in 0..x, (↑(rexp (-x)) : ℂ) * ((↑x_1 : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑x_1 : ℂ)) ^ (t - 1)))
Tactic: rw [mul_assoc, ← betaIntegral_scaled s t hx, ← intervalIntegral.integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (t - 1))
hst : 0 < (s + t).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ Eq (α := ℂ)
    (∫ (t_1 : ℝ) in 0..x,
      (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1)))
    (∫ (x_1 : ℝ) in 0..x, (↑(rexp (-x)) : ℂ) * ((↑x_1 : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑x_1 : ℂ)) ^ (t - 1)))
have e_f : ∀ (y : ℝ),
  (↑(rexp (-y)) : ℂ) * (↑y : ℂ) ^ (s - 1) * ((↑(rexp (-(x - y))) : ℂ) * (↑(x - y) : ℂ) ^ (t - 1)) =
    (↑(rexp (-x)) : ℂ) * ((↑y : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1))
Tactic: congr 1 with y : 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (t - 1))
hst : 0 < (s + t).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
⊢ (↑(rexp (-y)) : ℂ) * (↑y : ℂ) ^ (s - 1) * ((↑(rexp (-(x - y))) : ℂ) * (↑(x - y) : ℂ) ^ (t - 1)) =
    (↑(rexp (-x)) : ℂ) * ((↑y : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1))
have e_f : cexp (-(↑y : ℂ)) * (↑y : ℂ) ^ (s - 1) * (cexp (-((↑x : ℂ) - (↑y : ℂ))) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1)) =
  cexp (-(↑x : ℂ)) * ((↑y : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (t - 1))
hst : 0 < (s + t).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
this : cexp (-(↑x : ℂ)) = cexp (-(↑y : ℂ)) * cexp (-((↑x : ℂ) - (↑y : ℂ)))
⊢ cexp (-(↑y : ℂ)) * (↑y : ℂ) ^ (s - 1) * (cexp (-((↑x : ℂ) - (↑y : ℂ))) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1)) =
    cexp (-(↑x : ℂ)) * ((↑y : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1))
have rw : cexp (-(↑y : ℂ)) * (↑y : ℂ) ^ (s - 1) * (cexp (-((↑x : ℂ) - (↑y : ℂ))) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1)) =
  cexp (-(↑y : ℂ)) * cexp (-((↑x : ℂ) - (↑y : ℂ))) * ((↑y : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (t - 1))
hst : 0 < (s + t).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
⊢ cexp (-(↑y : ℂ)) * (↑y : ℂ) ^ (s - 1) * (cexp (-((↑x : ℂ) - (↑y : ℂ))) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1)) =
    cexp (-(↑x : ℂ)) * ((↑y : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1))
have e_f : cexp (-(↑x : ℂ)) = cexp (-(↑y : ℂ)) * cexp (-((↑x : ℂ) - (↑y : ℂ)))
Tactic: suffices Complex.exp (-x) = Complex.exp (-y) * Complex.exp (-(x - y)) by rw [this]; ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (t - 1))
hst : 0 < (s + t).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
⊢ cexp (-(↑x : ℂ)) = cexp (-(↑y : ℂ)) * cexp (-((↑x : ℂ) - (↑y : ℂ)))
have e_f : cexp (-(↑x : ℂ)) = cexp (-(↑y : ℂ) + -((↑x : ℂ) - (↑y : ℂ)))
Tactic: rw [← Complex.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∫ (t_1 : ℝ) in 0..x,
        (↑(rexp (-t_1)) : ℂ) * (↑t_1 : ℂ) ^ (s - 1) * ((↑(rexp (-(x - t_1))) : ℂ) * (↑(x - t_1) : ℂ) ^ (t - 1))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (t - 1))
hst : 0 < (s + t).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
y : ℝ
⊢ cexp (-(↑x : ℂ)) = cexp (-(↑y : ℂ) + -((↑x : ℂ) - (↑y : ℂ)))
have e_f : -(↑x : ℂ) = -(↑y : ℂ) + -((↑x : ℂ) - (↑y : ℂ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have hu' : 0 < (u + 1).re
Tactic: have hu' : 0 < re (u + 1) := by rw [add_re, one_re]; positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have hv' : 0 < (v + 1).re
Tactic: have hv' : 0 < re (v + 1) := by rw [add_re, one_re]; positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
⊢ ContinuousOn F (Icc 0 1)
have refine_1 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x), ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ u) x
Tactic: refine (continuousOn_of_forall_continuousAt fun x hx => ?_).mul
        (continuousOn_of_forall_continuousAt fun x hx => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
refine_1 :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x), ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ u) x
⊢ ContinuousOn F (Icc 0 1)
have refine_2 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x), ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ v) x
Tactic: refine (continuousOn_of_forall_continuousAt fun x hx => ?_).mul
        (continuousOn_of_forall_continuousAt fun x hx => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ u) x
have refine_1 : 0 ≤ (↑x : ℂ).re
Tactic: refine (continuousAt_cpow_const_of_re_pos (Or.inl ?_) hu).comp continuous_ofReal.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 0 ≤ (↑x : ℂ).re
have refine_1 : 0 ≤ x
Tactic: rw [ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ v) x
have refine_2 : 0 ≤ (1 - (↑x : ℂ)).re
Tactic: refine (continuousAt_cpow_const_of_re_pos (Or.inl ?_) hv).comp (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
⊢ 0 ≤ (1 - (↑x : ℂ)).re
have refine_2 : x ≤ 1
Tactic: rw [sub_re, one_re, ofReal_re, sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
have hc : ContinuousOn F (Icc 0 1)
Tactic: have hc : ContinuousOn F (Icc 0 1) := by
    refine (continuousOn_of_forall_continuousAt fun x hx => ?_).mul
        (continuousOn_of_forall_continuousAt fun x hx => ?_)
    · refine (continuousAt_cpow_const_of_re_pos (Or.inl ?_) hu).comp continuous_ofReal.continuousAt
      rw [ofReal_re]; exact hx.1
    · refine (continuousAt_cpow_const_of_re_pos (Or.inl ?_) hv).comp (by fun_prop)
      rw [sub_re, one_re, ofReal_re, sub_nonneg]
      exact hx.2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
have refine_2 : ∀ (this : HasDerivAt (fun (x : ℂ) ↦ id x ^ u) (u * id (↑x : ℂ) ^ (u - 1) * 1) (↑x : ℂ)),
  HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
Tactic: have := @HasDerivAt.cpow_const _ _ _ u (hasDerivAt_id (x : ℂ)) (Or.inl ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
refine_2 :
  ∀ (this : HasDerivAt (fun (x : ℂ) ↦ id x ^ u) (u * id (↑x : ℂ) ^ (u - 1) * 1) (↑x : ℂ)),
    HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
have refine_1 : 0 < (id (↑x : ℂ)).re
Tactic: have := @HasDerivAt.cpow_const _ _ _ u (hasDerivAt_id (x : ℂ)) (Or.inl ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ 0 < (id (↑x : ℂ)).re
have refine_1 : 0 < x
Tactic: rw [id_eq, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ HasDerivAt F (u * ((↑x : ℂ) ^ (u - 1) * (1 - (↑x : ℂ)) ^ v) - v * ((↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ (v - 1))) x
have U : HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
Tactic: have U : HasDerivAt (fun y : ℂ => y ^ u) (u * (x : ℂ) ^ (u - 1)) ↑x := by
      have := @HasDerivAt.cpow_const _ _ _ u (hasDerivAt_id (x : ℂ)) (Or.inl ?_)
      · simp only [id_eq, mul_one] at this
        exact this
      · rw [id_eq, ofReal_re]; exact hx.1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
U : HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ (1 - y) ^ v) (-v * (1 - (↑x : ℂ)) ^ (v - 1)) (↑x : ℂ)
have refine_2 : ∀ (A : HasDerivAt (fun (x : ℂ) ↦ id x ^ v) (v * id (1 - (↑x : ℂ)) ^ (v - 1) * 1) (1 - (↑x : ℂ))),
  HasDerivAt (fun (y : ℂ) ↦ (1 - y) ^ v) (-v * (1 - (↑x : ℂ)) ^ (v - 1)) (↑x : ℂ)
Tactic: have A := @HasDerivAt.cpow_const _ _ _ v (hasDerivAt_id (1 - (x : ℂ))) (Or.inl ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
U : HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)
refine_2 :
  ∀ (A : HasDerivAt (fun (x : ℂ) ↦ id x ^ v) (v * id (1 - (↑x : ℂ)) ^ (v - 1) * 1) (1 - (↑x : ℂ))),
    HasDerivAt (fun (y : ℂ) ↦ (1 - y) ^ v) (-v * (1 - (↑x : ℂ)) ^ (v - 1)) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ (1 - y) ^ v) (-v * (1 - (↑x : ℂ)) ^ (v - 1)) (↑x : ℂ)
have refine_1 : 0 < (id (1 - (↑x : ℂ))).re
Tactic: have A := @HasDerivAt.cpow_const _ _ _ v (hasDerivAt_id (1 - (x : ℂ))) (Or.inl ?_)