-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem partialGamma_add_one {s : ℂ} (hs : 0 < s.re) {X : ℝ} (hX : 0 ≤ X) :
    partialGamma (s + 1) X = s * partialGamma s X - (-X).exp * X ^ s

Proof state:
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 fun x => (ofReal ∘ fun y => rexp (-y)) 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)) =
    -((ofReal ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal ∘ fun y => rexp (-y)) 0 * ↑0 ^ 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 [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

Result:
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 fun x => (ofReal ∘ fun y => rexp (-y)) x * ↑x ^ s
der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -((ofReal ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)
⊢ ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s =
    (s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s

Proof state:
case e_a.e_f.h
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 fun x => (ofReal ∘ fun y => rexp (-y)) x * ↑x ^ s
der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -((ofReal ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)
t : ∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1)) = s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)
x✝ : ℝ
⊢ s * ↑(rexp (-x✝)) * ↑x✝ ^ (s - 1) = s * (↑(rexp (-x✝)) * ↑x✝ ^ (s - 1))

Tactic:
ring

Result:
no goals

Proof state:
case e_a.e_f
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 fun x => (ofReal ∘ fun y => rexp (-y)) x * ↑x ^ s
der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -((ofReal ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)
t : ∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1)) = s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)
⊢ (fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))

Tactic:
ext1

Result:
case e_a.e_f.h
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 fun x => (ofReal ∘ fun y => rexp (-y)) x * ↑x ^ s
der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -((ofReal ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)
t : ∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1)) = s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)
x✝ : ℝ
⊢ s * ↑(rexp (-x✝)) * ↑x✝ ^ (s - 1) = s * (↑(rexp (-x✝)) * ↑x✝ ^ (s - 1))

Proof state:
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 fun x => (ofReal ∘ fun y => rexp (-y)) x * ↑x ^ s
der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -((ofReal ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)
t : ∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1)) = s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)
⊢ s ≠ 0

Tactic:
contrapose! hs

Result:
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 fun x => (ofReal ∘ fun y => rexp (-y)) x * ↑x ^ s
der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -((ofReal ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)
t : ∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1)) = s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)
hs : s = 0
⊢ s.re ≤ 0

Proof state:
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 fun x => (ofReal ∘ fun y => rexp (-y)) x * ↑x ^ s
der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -((ofReal ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)
t : ∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1)) = s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)
⊢ (∫ (x : ℝ) in 0 ..X, s * ↑(rexp (-x)) * ↑x ^ (s - 1)) - (ofReal ∘ fun y => rexp (-y)) X * ↑X ^ s =
    (∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1))) - ↑(rexp (-X)) * ↑X ^ s

Tactic:
congr 2

Result:
case e_a.e_f
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 fun x => (ofReal ∘ fun y => rexp (-y)) x * ↑x ^ s
der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -((ofReal ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)
t : ∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1)) = s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)
⊢ (fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))