awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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 : ℂ)

Tactic:
exact continuousAt_cpow_const <| ofReal_mem_slitPlane.2 hx.1

Premises used: Iff.mpr, And.left, Complex.ofReal_mem_slitPlane, continuousAt_cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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 :
  @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (a : ℝ) ↦ ‖s * ((↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1))‖)
    (Measure.restrict volume (Ioc 0 Y))
⊢ @HasFiniteIntegral _ ℂ _ Real.measurableSpace (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
    (Measure.restrict volume (Ioc 0 Y))

Tactic:
rw [← hasFiniteIntegral_norm_iff]

Premises used: MeasureTheory.hasFiniteIntegral_norm_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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 :
  @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (a : ℝ) ↦ ‖s‖ * (‖(↑(rexp (-a)) : ℂ)‖ * ‖(↑a : ℂ) ^ (s - 1)‖))
    (Measure.restrict volume (Ioc 0 Y))
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (a : ℝ) ↦ ‖s * ((↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1))‖)
    (Measure.restrict volume (Ioc 0 Y))

Tactic:
simp_rw [norm_mul]

Premises used: norm_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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))

Tactic:
(((Real.GammaIntegral_convergent hs).mono_set
    Ioc_subset_Ioi_self).hasFiniteIntegral.congr ?_).const_mul _

Premises used: Real.GammaIntegral_convergent, Set.Ioc_subset_Ioi_self, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.HasFiniteIntegral.const_mul, MeasureTheory.HasFiniteIntegral.congr, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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 :
  (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)‖
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (a : ℝ) ↦ ‖s‖ * (‖(↑(rexp (-a)) : ℂ)‖ * ‖(↑a : ℂ) ^ (s - 1)‖))
    (Measure.restrict volume (Ioc 0 Y))

Tactic:
refine (((Real.GammaIntegral_convergent hs).mono_set
    Ioc_subset_Ioi_self).hasFiniteIntegral.congr ?_).const_mul _

Premises used: Real.GammaIntegral_convergent, Set.Ioc_subset_Ioi_self, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.HasFiniteIntegral.const_mul, MeasureTheory.HasFiniteIntegral.congr, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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)‖
right₁ : MeasurableSet (Ioc 0 Y)
⊢ (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:
rw [EventuallyEq, ae_restrict_iff']

Premises used: Filter.EventuallyEq, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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 : ℝ) (hx : x ∈ Ioc 0 Y), rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ)‖ * ‖(↑x : ℂ) ^ (s - 1)‖
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc 0 Y → rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ)‖ * ‖(↑x : ℂ) ^ (s - 1)‖

Tactic:
filter_upwards with x hx
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
right : rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re
⊢ rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ)‖ * ‖(↑x : ℂ) ^ (s - 1)‖

Tactic:
rw [Complex.norm_of_nonneg (exp_pos _).le, norm_cpow_eq_rpow_re_of_pos hx.1]

Premises used: LT.lt.le, Complex.norm_of_nonneg, And.left, Complex.norm_cpow_eq_rpow_re_of_pos, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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).re

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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))
⊢ MeasurableSet (Ioc 0 Y)

Tactic:
measurableSet_Ioc

Premises used: measurableSet_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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))
⊢ MeasurableSet (Ioc 0 Y)

Tactic:
exact measurableSet_Ioc

Premises used: measurableSet_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
rw :
  ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s =
    (s * ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s
⊢ (s + 1).partialGamma X = s * s.partialGamma X - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s

Tactic:
rw [partialGamma, partialGamma, add_sub_cancel_right]

Premises used: add_sub_cancel_right, Complex.partialGamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
⊢ HasDerivAt (fun (y : ℝ) ↦ rexp (-y)) (-rexp (-x)) x

Tactic:
simpa using (hasDerivAt_neg x).exp

Premises used: HasDerivAt.exp, hasDerivAt_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
refine_1 : id (↑x : ℂ) ∈ slitPlane
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ s) (s * (↑x : ℂ) ^ (s - 1)) x

Tactic:
have t := @HasDerivAt.cpow_const _ _ _ s (hasDerivAt_id ↑x) ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
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:
simpa only [mul_one] using t.comp_ofReal

Premises used: HasDerivAt.comp_ofReal, mul_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
⊢ id (↑x : ℂ) ∈ slitPlane

Tactic:
ofReal_mem_slitPlane.2 hx.1

Premises used: Iff.mpr, Set.Mem, And.left, Complex.ofReal_mem_slitPlane
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
⊢ id (↑x : ℂ) ∈ slitPlane

Tactic:
exact ofReal_mem_slitPlane.2 hx.1

Premises used: Iff.mpr, And.left, Complex.ofReal_mem_slitPlane
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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

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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
d2 : HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ s) (s * (↑x : ℂ) ^ (s - 1)) x
⊢ HasDerivAt (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
    (-((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) + (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) x

Tactic:
simpa only [ofReal_neg, neg_mul] using d1.ofReal_comp.mul d2

Premises used: Complex.ofReal_neg, HasDerivAt.ofReal_comp, HasDerivAt.mul, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ ∀ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
⊢ 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)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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)
⊢ 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)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
⊢ ∫ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
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
⊢ -∫ (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:
apply_fun fun x : ℂ => -x at int_eval

Premises used: Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
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)
⊢ HAdd.hAdd (α := ℂ) (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (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:
rw [intervalIntegral.integral_add (Gamma_integrand_deriv_integrable_A hs hX)
      (Gamma_integrand_deriv_integrable_B hs hX),
    intervalIntegral.integral_neg, neg_add, neg_neg] at int_eval

Premises used: neg_add, neg_neg, _private.0.Complex.Gamma_integrand_deriv_integrable_A, intervalIntegral.integral_add, _private.0.Complex.Gamma_integrand_deriv_integrable_B, intervalIntegral.integral_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
int_eval :
  HAdd.hAdd (α := ℂ) (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (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)
rw :
  (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) +
        HMul.hMul (α := ℝ → ℂ) (β := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) 0 -
      HMul.hMul (α := ℝ → ℂ) (β := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) X =
    (s * ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) - (↑(rexp (-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

Tactic:
rw [eq_sub_of_add_eq int_eval, sub_neg_eq_add, neg_sub, add_comm, add_sub]

Premises used: neg_sub, eq_sub_of_add_eq, add_sub, add_comm, sub_neg_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
int_eval :
  HAdd.hAdd (α := ℂ) (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (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)
contrapose! : ∀ (hs : s = 0), s.re ≤ 0
⊢ s ≠ 0

Tactic:
contrapose! hs
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
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
int_eval :
  HAdd.hAdd (α := ℂ) (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (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)
hs : s = 0
rw : re 0 ≤ 0
rw₁ rw₂ : LE.le (α := ℝ) 0 0
⊢ s.re ≤ 0

Tactic:
rw [hs, zero_re]

Premises used: Complex.zero_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
int_eval :
  HAdd.hAdd (α := ℂ) (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (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)
⊢ s ≠ 0

Tactic:
have hn : s ≠ 0 := by contrapose! hs; rw [hs, zero_re]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
int_eval :
  HAdd.hAdd (α := ℂ) (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (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)
hn : s ≠ 0
simp :
  (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s =
    (∫ (x : ℝ) in 0..X, s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s
⊢ (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) +
        HMul.hMul (α := ℝ → ℂ) (β := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) 0 -
      HMul.hMul (α := ℝ → ℂ) (β := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) X =
    (s * ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s

Tactic:
simp only [Pi.mul_apply, Function.comp_apply, ofReal_zero, zero_cpow hn, mul_zero, add_zero,
    ← intervalIntegral.integral_const_mul]

Premises used: Pi.mul_apply, MulZeroClass.mul_zero, Complex.zero_cpow, Complex.ofReal_zero, Function.comp_apply, add_zero, intervalIntegral.integral_const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
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
int_eval :
  HAdd.hAdd (α := ℂ) (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (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)
hn : s ≠ 0
e_a : ∀ (x : ℝ), (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1)) = s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s =
    (∫ (x : ℝ) in 0..X, s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s

Tactic:
congr with x