awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw :
  (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑(rexp (-x)) : ℂ) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑x : ℂ) ^ (s - 1)) : ℂ)
rw₁ :
  (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    HMul.hMul (β := ℂ) (↑(rexp (-x)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑x : ℂ) ^ (s - 1)) : ℂ)
rw₂ :
  (↑(rexp (-x)) : ℂ) * cexp (log (↑x : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    HMul.hMul (β := ℂ) (↑(rexp (-x)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑x : ℂ) ^ (s - 1)) : ℂ)
rw₃ :
  (↑(rexp (-x)) : ℂ) * cexp (log (↑x : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    HMul.hMul (β := ℂ) (↑(rexp (-x)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (log (↑x : ℂ) * (s - 1))) : ℂ)
rw₄ :
  (↑(rexp (-x)) : ℂ) * cexp (log (↑x : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    (↑(rexp (-x)) : ℂ) * cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (log (↑x : ℂ) * (s - 1)))
rw₅ :
  (↑(rexp (-x)) : ℂ) * cexp (log (↑x : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    (↑(rexp (-x)) : ℂ) *
      cexp
        (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log (↑x : ℂ)) : ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) (s - 1) : ℂ))
rw₆ :
  (↑(rexp (-x)) : ℂ) *
      cexp ((↑(Real.log x) : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    (↑(rexp (-x)) : ℂ) *
      cexp
        (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑(Real.log x) : ℂ) : ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) (s - 1) : ℂ))
rw₇ :
  (↑(rexp (-x)) : ℂ) *
      cexp ((↑(Real.log x) : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    (↑(rexp (-x)) : ℂ) * cexp (HMul.hMul (β := ℂ) (↑(Real.log x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (s - 1) : ℂ))
rw₈ :
  (↑(rexp (-x)) : ℂ) *
      cexp ((↑(Real.log x) : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    (↑(rexp (-x)) : ℂ) *
      cexp
        ((↑(Real.log x) : ℂ) *
          HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ))
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
have rw₉ : (↑(rexp (-x)) : ℂ) *
    cexp ((↑(Real.log x) : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
  (↑(rexp (-x)) : ℂ) *
    cexp ((↑(Real.log x) : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ))
Tactic: rw [map_mul, conj_ofReal, cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)),
    cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)), ← exp_conj, map_mul,
    ← ofReal_log (le_of_lt hx), conj_ofReal, map_sub, map_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℝ
⊢ (↑s : ℂ).GammaIntegral =
    (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (s - 1)) :
      ℂ)
have this : ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)
Tactic: have : ∀ r : ℝ, Complex.ofReal r = @RCLike.ofReal ℂ _ r := fun r => rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
this : ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)
| (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-x) * x ^ (s - 1)) :
    ℂ)
have rw : @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
  (↑(rexp (-x) * x ^ (s - 1)) : ℂ)
Tactic: rw [this, ← _root_.integral_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
this : ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ ((↑s : ℂ) - 1)) =
    (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (s - 1)) :
      ℂ)
have conv_rhs : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ ((↑s : ℂ) - 1))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (↑(rexp (-x) * x ^ (s - 1)) : ℂ))
Tactic: conv_rhs => rw [this, ← _root_.integral_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
this : ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ ((↑s : ℂ) - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑(rexp (-x) * x ^ (s - 1)) : ℂ))
have refine : EqOn (β := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ ((↑s : ℂ) - 1))
  (fun (x : ℝ) ↦ (↑(rexp (-x) * x ^ (s - 1)) : ℂ)) (Ioi 0)
Tactic: refine setIntegral_congr_fun measurableSet_Ioi ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
this : ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ ((↑s : ℂ) - 1) = (↑(rexp (-x) * x ^ (s - 1)) : ℂ)
have rw : (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ ((↑s : ℂ) - 1) = (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (↑(s - 1) : ℂ)
Tactic: rw [ofReal_mul, ofReal_cpow (mem_Ioi.mp hx).le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
X : ℝ
hs : 0 < s.re
hX : 0 ≤ X
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) volume 0 X
have rw : IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioc 0 X)
  volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hX]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ -((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)) volume 0 X
have h : ∀ (x : ℝ), -((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) = (-fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s + 1 - 1)) x
Tactic: convert! (Gamma_integrand_intervalIntegrable (s + 1) _ hX).neg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
h : ∀ (x : ℝ), -((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) = (-fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s + 1 - 1)) x
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ -((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)) volume 0 X
have convert! : 0 < (s + 1).re
Tactic: convert! (Gamma_integrand_intervalIntegrable (s + 1) _ hX).neg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
⊢ -((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) = (-fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s + 1 - 1)) x
have h : -(cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ s) = (-fun (x : ℝ) ↦ cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ s) x
Tactic: simp only [ofReal_exp, ofReal_neg, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ 0 < s.re + 1
have linarith : s.re + 1 ≤ 0 → -1 + (0 - s.re) + (s.re + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
⊢ Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
have h : ∀ (x : ℝ), (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1)) = s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) volume 0 Y
have this : Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
  s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
Tactic: have : (fun x => (-x).exp * (s * x ^ (s - 1)) : ℝ → ℂ) =
      (fun x => s * ((-x).exp * x ^ (s - 1)) : ℝ → ℂ) := by ext1; ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) volume 0 Y
have rw : IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
  (Ioc 0 Y) volume
Tactic: rw [this, intervalIntegrable_iff_integrableOn_Ioc_of_le hY]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
    (Ioc 0 Y) volume
have left : AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
  (Measure.restrict volume (Ioc 0 Y))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
left :
  AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace)
    (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))) (Measure.restrict volume (Ioc 0 Y))
⊢ IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
    (Ioc 0 Y) volume
have right : @HasFiniteIntegral _ ℂ _ Real.measurableSpace (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
  (Measure.restrict volume (Ioc 0 Y))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace)
    (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))) (Measure.restrict volume (Ioc 0 Y))
have left : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioc 0 Y)
Tactic: refine (continuousOn_const.mul ?_).aestronglyMeasurable measurableSet_Ioc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioc 0 Y)
have left : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) (Ioc 0 Y)
Tactic: apply (continuous_ofReal.comp continuous_neg.rexp).continuousOn.mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) (Ioc 0 Y)
have left : ∀ x ∈ Ioc 0 Y, ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) x
Tactic: apply continuousOn_of_forall_continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) x
have left : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ x ^ (s - 1)) (↑x : ℂ)
Tactic: refine (?_ : ContinuousAt (fun x : ℂ => x ^ (s - 1)) _).comp continuous_ofReal.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ @HasFiniteIntegral _ ℂ _ Real.measurableSpace (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
    (Measure.restrict volume (Ioc 0 Y))
have right : @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (a : ℝ) ↦ ‖s * ((↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1))‖)
  (Measure.restrict volume (Ioc 0 Y))
Tactic: rw [← hasFiniteIntegral_norm_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (a : ℝ) ↦ ‖s * ((↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1))‖)
    (Measure.restrict volume (Ioc 0 Y))
have right : @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (a : ℝ) ↦ ‖s‖ * (‖(↑(rexp (-a)) : ℂ)‖ * ‖(↑a : ℂ) ^ (s - 1)‖))
  (Measure.restrict volume (Ioc 0 Y))
Tactic: simp_rw [norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (a : ℝ) ↦ ‖s‖ * (‖(↑(rexp (-a)) : ℂ)‖ * ‖(↑a : ℂ) ^ (s - 1)‖))
    (Measure.restrict volume (Ioc 0 Y))
have right : (ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 Y))).EventuallyEq (β := ℝ)
  (fun (x : ℝ) ↦ rexp (-x) * x ^ (s.re - 1)) fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ)‖ * ‖(↑a : ℂ) ^ (s - 1)‖
Tactic: refine (((Real.GammaIntegral_convergent hs).mono_set
    Ioc_subset_Ioi_self).hasFiniteIntegral.congr ?_).const_mul _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 Y))).EventuallyEq (β := ℝ)
    (fun (x : ℝ) ↦ rexp (-x) * x ^ (s.re - 1)) fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ)‖ * ‖(↑a : ℂ) ^ (s - 1)‖
have right : ∀ᵐ (x : ℝ), x ∈ Ioc 0 Y → rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ)‖ * ‖(↑x : ℂ) ^ (s - 1)‖
Tactic: rw [EventuallyEq, ae_restrict_iff']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
right : ∀ᵐ (x : ℝ), x ∈ Ioc 0 Y → rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ)‖ * ‖(↑x : ℂ) ^ (s - 1)‖
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioc 0 Y))).EventuallyEq (β := ℝ)
    (fun (x : ℝ) ↦ rexp (-x) * x ^ (s.re - 1)) fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ)‖ * ‖(↑a : ℂ) ^ (s - 1)‖
have right₁ : MeasurableSet (Ioc 0 Y)
Tactic: rw [EventuallyEq, ae_restrict_iff']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc 0 Y → rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ)‖ * ‖(↑x : ℂ) ^ (s - 1)‖
have right : ∀ (x : ℝ) (hx : x ∈ Ioc 0 Y), rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ)‖ * ‖(↑x : ℂ) ^ (s - 1)‖
Tactic: filter_upwards with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ)‖ * ‖(↑x : ℂ) ^ (s - 1)‖
have right : rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re
Tactic: rw [Complex.norm_of_nonneg (exp_pos _).le, norm_cpow_eq_rpow_re_of_pos hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ (s + 1).partialGamma X = s * s.partialGamma X - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s
have rw : ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s =
  (s * ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s
Tactic: rw [partialGamma, partialGamma, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
⊢ HasDerivAt (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
    (-((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) + (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) x
have d1 : HasDerivAt (fun (y : ℝ) ↦ rexp (-y)) (-rexp (-x)) x
Tactic: have d1 : HasDerivAt (fun y : ℝ => (-y).exp) (-(-x).exp) x := by
      simpa using (hasDerivAt_neg x).exp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun (y : ℝ) ↦ rexp (-y)) (-rexp (-x)) x
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ s) (s * (↑x : ℂ) ^ (s - 1)) x
have refine_2 : ∀ (t : HasDerivAt (fun (x : ℂ) ↦ id x ^ s) (s * id (↑x : ℂ) ^ (s - 1) * 1) (↑x : ℂ)),
  HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ s) (s * (↑x : ℂ) ^ (s - 1)) x
Tactic: have t := @HasDerivAt.cpow_const _ _ _ s (hasDerivAt_id ↑x) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun (y : ℝ) ↦ rexp (-y)) (-rexp (-x)) x
refine_2 :
  ∀ (t : HasDerivAt (fun (x : ℂ) ↦ id x ^ s) (s * id (↑x : ℂ) ^ (s - 1) * 1) (↑x : ℂ)),
    HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ s) (s * (↑x : ℂ) ^ (s - 1)) x
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ s) (s * (↑x : ℂ) ^ (s - 1)) x
have refine_1 : id (↑x : ℂ) ∈ slitPlane
Tactic: have t := @HasDerivAt.cpow_const _ _ _ s (hasDerivAt_id ↑x) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun (y : ℝ) ↦ rexp (-y)) (-rexp (-x)) x
⊢ HasDerivAt (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
    (-((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) + (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) x
have d2 : HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ s) (s * (↑x : ℂ) ^ (s - 1)) x
Tactic: have d2 : HasDerivAt (fun y : ℝ => (y : ℂ) ^ s) (s * x ^ (s - 1)) x := by
      have t := @HasDerivAt.cpow_const _ _ _ s (hasDerivAt_id ↑x) ?_
      · simpa only [mul_one] using t.comp_ofReal
      · exact ofReal_mem_slitPlane.2 hx.1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s =
    (s * ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s
have F_der_I : ∀ x ∈ Ioo 0 X,
  HasDerivAt (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
    (-((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) + (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) x
Tactic: have F_der_I : ∀ x : ℝ, x ∈ Ioo 0 X → HasDerivAt (fun x => (-x).exp * x ^ s : ℝ → ℂ)
      (-((-x).exp * x ^ s) + (-x).exp * (s * x ^ (s - 1))) x := by
    intro x hx
    have d1 : HasDerivAt (fun y : ℝ => (-y).exp) (-(-x).exp) x := by
      simpa using (hasDerivAt_neg x).exp
    have d2 : HasDerivAt (fun y : ℝ => (y : ℂ) ^ s) (s * x ^ (s - 1)) x := by
      have t := @HasDerivAt.cpow_const _ _ _ s (hasDerivAt_id ↑x) ?_
      · simpa only [mul_one] using t.comp_ofReal
      · exact ofReal_mem_slitPlane.2 hx.1
    simpa only [ofReal_neg, neg_mul] using d1.ofReal_comp.mul d2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) + (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) x
⊢ ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s =
    (s * ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s
have cont : Continuous (HMul.hMul (α := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) fun (x : ℝ) ↦ (↑x : ℂ) ^ s)
Tactic: have cont := (continuous_ofReal.comp continuous_neg.rexp).mul (continuous_ofReal_cpow_const hs)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) + (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) x
cont : Continuous (HMul.hMul (α := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) fun (x : ℝ) ↦ (↑x : ℂ) ^ s)
⊢ ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s =
    (s * ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s
have der_ible : IntervalIntegrable (ε := ℂ)
  (fun (x : ℝ) ↦ -((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) + (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) volume 0 X
Tactic: have der_ible :=
    (Gamma_integrand_deriv_integrable_A hs hX).add (Gamma_integrand_deriv_integrable_B hs hX)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) + (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) x
cont : Continuous (HMul.hMul (α := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) fun (x : ℝ) ↦ (↑x : ℂ) ^ s)
der_ible :
  IntervalIntegrable (ε := ℂ)
    (fun (x : ℝ) ↦ -((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) + (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) volume 0 X
⊢ ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s =
    (s * ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s
have int_eval : ∫ (y : ℝ) in 0..X, -((↑(rexp (-y)) : ℂ) * (↑y : ℂ) ^ s) + (↑(rexp (-y)) : ℂ) * (s * (↑y : ℂ) ^ (s - 1)) =
  HMul.hMul (α := ℝ → ℂ) (β := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) X -
    HMul.hMul (α := ℝ → ℂ) (β := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) 0
Tactic: have int_eval := integral_eq_sub_of_hasDerivAt_of_le hX cont.continuousOn F_der_I der_ible