awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
⊢ 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 ℝ ℂ)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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))
⊢ 0 < s.re + t.re

Tactic:
add_pos hs ht

Premises used: add_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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))
⊢ 0 < s.re + t.re

Tactic:
exact add_pos hs ht

Premises used: add_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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))
⊢ 0 < (s + t).re

Tactic:
have hst : 0 < re (s + t) := by rw [add_re]; exact add_pos hs ht
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
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)
⊢ Gamma s * Gamma t = Gamma (s + t) * 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 _ _)]

Premises used: Complex.GammaIntegral, Complex.betaIntegral, Complex.Gamma_eq_integral, MeasureTheory.integral_mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)

Tactic:
setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
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
⊢ 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:
refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
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)))
⊢ ∫ (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:
rw [mul_assoc, ← betaIntegral_scaled s t hx, ← intervalIntegral.integral_const_mul]

Premises used: Complex.betaIntegral_scaled, mul_assoc, intervalIntegral.integral_const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
e_f :
  ∀ (y : ℝ),
    (↑(rexp (-y)) : ℂ) * (↑y : ℂ) ^ (s - 1) * ((↑(rexp (-(x - y))) : ℂ) * (↑(x - y) : ℂ) ^ (t - 1)) =
      (↑(rexp (-x)) : ℂ) * ((↑y : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1))
⊢ 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:
congr 1 with y : 1
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℝ
e_f :
  cexp (-(↑y : ℂ)) * (↑y : ℂ) ^ (s - 1) * (cexp (-((↑x : ℂ) - (↑y : ℂ))) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1)) =
    cexp (-(↑x : ℂ)) * ((↑y : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1))
⊢ (↑(rexp (-y)) : ℂ) * (↑y : ℂ) ^ (s - 1) * ((↑(rexp (-(x - y))) : ℂ) * (↑(x - y) : ℂ) ^ (t - 1)) =
    (↑(rexp (-x)) : ℂ) * ((↑y : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1))

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)))
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))
⊢ cexp (-(↑y : ℂ)) * (↑y : ℂ) ^ (s - 1) * (cexp (-((↑x : ℂ) - (↑y : ℂ))) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1)) =
    cexp (-(↑x : ℂ)) * ((↑y : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1))

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 (-(↑y : ℂ)) * cexp (-((↑x : ℂ) - (↑y : ℂ))) * ((↑y : ℂ) ^ (s - 1) * ((↑x : ℂ) - (↑y : ℂ)) ^ (t - 1))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℝ
e_f : 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))

Tactic:
suffices Complex.exp (-x) = Complex.exp (-y) * Complex.exp (-(x - y)) by rw [this]; ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℝ
e_f : cexp (-(↑x : ℂ)) = cexp (-(↑y : ℂ) + -((↑x : ℂ) - (↑y : ℂ)))
⊢ cexp (-(↑x : ℂ)) = cexp (-(↑y : ℂ)) * cexp (-((↑x : ℂ) - (↑y : ℂ)))

Tactic:
rw [← Complex.exp_add]

Premises used: Complex.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℝ
e_f : -(↑x : ℂ) = -(↑y : ℂ) + -((↑x : ℂ) - (↑y : ℂ))
⊢ cexp (-(↑x : ℂ)) = cexp (-(↑y : ℂ) + -((↑x : ℂ) - (↑y : ℂ)))

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℝ
⊢ -(↑x : ℂ) = -(↑y : ℂ) + -((↑x : ℂ) - (↑y : ℂ))

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
⊢ 0 < u.re + 1

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
⊢ 0 < (u + 1).re

Tactic:
have hu' : 0 < re (u + 1) := by rw [add_re, one_re]; positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
⊢ 0 < v.re + 1

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun (x : ℝ) ↦ (↑x : ℂ) ^ u * (1 - (↑x : ℂ)) ^ v
hu' : 0 < (u + 1).re
⊢ 0 < (v + 1).re

Tactic:
have hv' : 0 < re (v + 1) := by rw [add_re, one_re]; positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)

Tactic:
(continuousOn_of_forall_continuousAt fun x hx => ?_).mul
        (continuousOn_of_forall_continuousAt fun x hx => ?_)

Premises used: continuousOn_of_forall_continuousAt, ContinuousOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
refine_2 :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x), ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ v) x
⊢ ContinuousOn F (Icc 0 1)

Tactic:
refine (continuousOn_of_forall_continuousAt fun x hx => ?_).mul
        (continuousOn_of_forall_continuousAt fun x hx => ?_)

Premises used: continuousOn_of_forall_continuousAt, ContinuousOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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

Tactic:
(continuousAt_cpow_const_of_re_pos (Or.inl ?_) hu).comp continuous_ofReal.continuousAt

Premises used: Complex.continuousAt_cpow_const_of_re_pos, Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
refine_1 : 0 ≤ (↑x : ℂ).re
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ u) x

Tactic:
refine (continuousAt_cpow_const_of_re_pos (Or.inl ?_) hu).comp continuous_ofReal.continuousAt

Premises used: Complex.continuousAt_cpow_const_of_re_pos, Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
refine_1 : 0 ≤ x
⊢ 0 ≤ (↑x : ℂ).re

Tactic:
rw [ofReal_re]

Premises used: Complex.ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
refine_2 : 0 ≤ (1 - (↑x : ℂ)).re
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (1 - (↑x : ℂ)) ^ v) x

Tactic:
refine (continuousAt_cpow_const_of_re_pos (Or.inl ?_) hv).comp (by fun_prop)

Premises used: Complex.continuousAt_cpow_const_of_re_pos, ContinuousAt.comp, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
refine_2 : x ≤ 1
⊢ 0 ≤ (1 - (↑x : ℂ)).re

Tactic:
rw [sub_re, one_re, ofReal_re, sub_nonneg]

Premises used: Complex.sub_re, Complex.ofReal_re, Complex.one_re, sub_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
⊢ x ≤ 1

Tactic:
hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
⊢ x ≤ 1

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)

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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)
refine_1 : 0 < (id (↑x : ℂ)).re
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ u) (u * (↑x : ℂ) ^ (u - 1)) (↑x : ℂ)

Tactic:
have := @HasDerivAt.cpow_const _ _ _ u (hasDerivAt_id (x : ℂ)) (Or.inl ?_)