awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ ∫ (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: apply_fun fun x : ℂ => -x at int_eval
Cleared hypotheses: int_eval
-- 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
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)
⊢ ∫ (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₁ : 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
Cleared hypotheses: int_eval
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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)
⊢ ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s =
    (s * ∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s
have 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
Tactic: rw [eq_sub_of_add_eq int_eval, sub_neg_eq_add, neg_sub, add_comm, add_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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
have contrapose! : ∀ (hs : s = 0), s.re ≤ 0
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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
⊢ s.re ≤ 0
have rw : re 0 ≤ 0
Tactic: rw [hs, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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
⊢ s.re ≤ 0
have rw₁ : LE.le (α := ℝ) 0 0
Tactic: rw [hs, zero_re]
-- 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
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)
⊢ (∫ (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
have hn : s ≠ 0
Tactic: have hn : s ≠ 0 := by contrapose! hs; rw [hs, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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
⊢ (∫ (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
have 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
Tactic: simp only [Pi.mul_apply, Function.comp_apply, ofReal_zero, zero_cpow hn, mul_zero, add_zero,
    ← intervalIntegral.integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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
⊢ (∫ (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
have e_a : ∀ (x : ℝ), (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1)) = s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ (s + 1).GammaIntegral = s * s.GammaIntegral
have refine : Tendsto (s + 1).partialGamma atTop (𝓝 (s + 1).GammaIntegral)
Tactic: refine tendsto_nhds_unique ?_ this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s + 1).GammaIntegral)
have hs₁ : 0 < (s + 1).re
Tactic: apply tendsto_partialGamma
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 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
⊢ (s + 1).GammaIntegral = s * s.GammaIntegral
have suffices : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
Tactic: suffices Tendsto (s + 1).partialGamma atTop (𝓝 <| s * GammaIntegral s) by
    refine tendsto_nhds_unique ?_ this
    apply tendsto_partialGamma; rw [add_re, one_re]; linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
have apply : EqOn (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) (s + 1).partialGamma (Ici 0)
Tactic: apply eventuallyEq_of_mem (Ici_mem_atTop (0 : ℝ))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : Membership.mem (γ := Set ℝ) (Ici 0) X
⊢ (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) X = (s + 1).partialGamma X
have rw : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) X =
  s * s.partialGamma X - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s
Tactic: rw [partialGamma_add_one hs (mem_Ici.mp hX)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
have this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
Tactic: have : (fun X : ℝ => s * partialGamma s X - X ^ s * (-X).exp) =ᶠ[atTop]
      (s + 1).partialGamma := by
    apply eventuallyEq_of_mem (Ici_mem_atTop (0 : ℝ))
    intro X hX
    rw [partialGamma_add_one hs (mem_Ici.mp hX)]
    ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
have refine : Tendsto (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) atTop (𝓝 (s * s.GammaIntegral))
Tactic: refine Tendsto.congr' this ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) atTop (𝓝 (s * s.GammaIntegral))
have suffices : Tendsto (β := ℂ) (fun (X : ℝ) ↦ -(↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) atTop (𝓝 0)
Tactic: suffices Tendsto (fun X => -X ^ s * (-X).exp : ℝ → ℂ) atTop (𝓝 0) by
    simpa using Tendsto.add (Tendsto.const_mul s (tendsto_partialGamma hs)) this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (β := ℂ) (fun (X : ℝ) ↦ -(↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) atTop (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖) atTop (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
⊢ EventuallyEq (β := ℝ) atTop (fun (e : ℝ) ↦ ‖-(↑e : ℂ) ^ s * (↑(rexp (-e)) : ℂ)‖) fun (e : ℝ) ↦
    e ^ s.re * rexp (-1 * e)
have refine : EqOn (β := ℝ) (fun (e : ℝ) ↦ ‖-(↑e : ℂ) ^ s * (↑(rexp (-e)) : ℂ)‖) (fun (e : ℝ) ↦ e ^ s.re * rexp (-1 * e)) (Ioi 0)
Tactic: refine eventuallyEq_of_mem (Ioi_mem_atTop 0) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
have rw : ‖-(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
Tactic: rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
      Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : ‖-(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
⊢ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
have rw₁ : ‖(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
Tactic: rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
      Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : ‖-(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₁ : ‖(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
⊢ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
have rw₂ : x ^ s.re * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
Tactic: rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
      Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : ‖-(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₁ : ‖(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₂ : x ^ s.re * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
⊢ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
have rw₃ : x ^ s.re * rexp (-x) = x ^ s.re * rexp (-1 * x)
Tactic: rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
      Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : ‖-(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₁ : ‖(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₂ : x ^ s.re * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₃ : x ^ s.re * rexp (-x) = x ^ s.re * rexp (-1 * x)
⊢ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
have rw₄ : x ^ s.re * rexp (-x) = x ^ s.re * rexp (-(1 * x))
Tactic: rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
      Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : ‖-(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₁ : ‖(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₂ : x ^ s.re * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₃ : x ^ s.re * rexp (-x) = x ^ s.re * rexp (-1 * x)
rw₄ : x ^ s.re * rexp (-x) = x ^ s.re * rexp (-(1 * x))
⊢ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
have rw₅ : x ^ s.re * rexp (-x) = x ^ s.re * rexp (-x)
Tactic: rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
      Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖) atTop (𝓝 0)
have this₁ : EventuallyEq (β := ℝ) atTop (fun (e : ℝ) ↦ ‖-(↑e : ℂ) ^ s * (↑(rexp (-e)) : ℂ)‖) fun (e : ℝ) ↦ e ^ s.re * rexp (-1 * e)
Tactic: have :
      (fun e : ℝ => ‖-(e : ℂ) ^ s * (-e).exp‖) =ᶠ[atTop] fun e : ℝ => e ^ s.re * (-1 * e).exp := by
    refine eventuallyEq_of_mem (Ioi_mem_atTop 0) ?_
    intro x hx; dsimp only
    rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
      Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
h1 : -s.re < (↑0 : ℝ)
⊢ GammaAux 0 s = GammaAux 0 (s + 1) / s
have h1₁ : 0 < s.re
Tactic: simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = (s + 1).GammaIntegral / s
have zero : s.GammaIntegral = s * s.GammaIntegral / s
Tactic: rw [GammaIntegral_add_one h1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = s * s.GammaIntegral / s
have zero : s ≠ 0
Tactic: rw [mul_comm, mul_div_cancel_right₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
h1 : 0 < s.re
⊢ s ≠ 0
have zero : ∀ (h1 : s = 0), s.re ≤ 0
Tactic: contrapose! h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
h1 : s = 0
⊢ s.re ≤ 0
have zero : re 0 ≤ 0
Tactic: rw [h1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
n : ℕ
hn : ∀ (s : ℂ) (h1 : -s.re < (↑n : ℝ)), GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < (↑(n + 1) : ℝ)
⊢ -(s + 1).re < (↑n : ℝ)
have h1₁ : -s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rw [Nat.cast_add, Nat.cast_one] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
hn : ∀ (s : ℂ) (h1 : -s.re < (↑n : ℝ)), GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ -(s.re + 1) < (↑n : ℝ)
have linarith : (↑n : ℝ) ≤ -(s.re + 1) → -s.re - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + ((↑n : ℝ) - -(s.re + 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
n : ℕ
hn : ∀ (s : ℂ) (h1 : -s.re < (↑n : ℝ)), GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < (↑(n + 1) : ℝ)
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s
have hh1 : -(s + 1).re < (↑n : ℝ)
Tactic: have hh1 : -(s + 1).re < n := by
      rw [Nat.cast_add, Nat.cast_one] at h1
      rw [add_re, one_re]; linarith