-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_eq_integral {s : ℝ} (hs : 0 < s) :
    Gamma s = ∫ x in Ioi 0, exp (-x) * x ^ (s - 1)

Proof state:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ Complex.exp (-↑x) * ↑x ^ (↑s - 1) = Complex.exp (-↑x) * ↑(x ^ (s - 1))

Tactic:
rw [Complex.ofReal_cpow (le_of_lt hx)]

Result:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ Complex.exp (-↑x) * ↑x ^ (↑s - 1) = Complex.exp (-↑x) * ↑x ^ ↑(s - 1)

Proof state:
s : ℝ
hs : 0 < s
this : ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))
cc : ∀ (r : ℝ), ↑r = ↑r
⊢ (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
rw [_root_.integral_ofReal, ← cc, Complex.ofReal_re]

Result:
no goals

Proof state:
s : ℝ
hs : 0 < s
⊢ 0 < (↑s).re

Tactic:
rwa [Complex.ofReal_re]

Result:
no goals

Proof state:
s : ℝ
hs : 0 < s
this : ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))
⊢ (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1)).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
have cc : ∀ r : ℝ, Complex.ofReal r = @RCLike.ofReal ℂ _ r := fun r => rfl

Result:
s : ℝ
hs : 0 < s
this : ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))
cc : ∀ (r : ℝ), ↑r = ↑r
⊢ (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1)).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Proof state:
s : ℝ
hs : 0 < s
⊢ (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1)).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
simp_rw [← Complex.ofReal_one, ← Complex.ofReal_sub]

Result:
s : ℝ
hs : 0 < s
⊢ (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1)).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Proof state:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ Complex.exp (-↑x) * ↑x ^ (↑s - 1) = Complex.exp (-↑x) * ↑x ^ (↑s - 1)

Tactic:
rfl

Result:
no goals

Proof state:
s : ℝ
hs : 0 < s
⊢ (↑s).GammaIntegral.re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
dsimp only [Complex.GammaIntegral]

Result:
s : ℝ
hs : 0 < s
⊢ (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1)).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Proof state:
s : ℝ
hs : 0 < s
this : ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))
cc : ∀ (r : ℝ), ↑r = ↑r
⊢ (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1)).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
conv_lhs => rw [this]; enter [1, 2, x]; rw [cc]

Result:
s : ℝ
hs : 0 < s
this : ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))
cc : ∀ (r : ℝ), ↑r = ↑r
⊢ (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Proof state:
s : ℝ
hs : 0 < s
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Result:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ ↑(s - 1) = ↑(rexp (-x) * x ^ (s - 1))

Proof state:
s : ℝ
hs : 0 < s
⊢ (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1)).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
suffices ∫ x : ℝ in Ioi 0, ↑(exp (-x)) * (x : ℂ) ^ ((s - 1 : ℝ) : ℂ) =
    ∫ x : ℝ in Ioi 0, ((exp (-x) * x ^ (s - 1) : ℝ) : ℂ) by
  have cc : ∀ r : ℝ, Complex.ofReal r = @RCLike.ofReal ℂ _ r := fun r => rfl
  conv_lhs => rw [this]; enter [1, 2, x]; rw [cc]
  rw [_root_.integral_ofReal, ← cc, Complex.ofReal_re]

Result:
s : ℝ
hs : 0 < s
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))

Proof state:
s : ℝ
hs : 0 < s
⊢ Gamma s = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
rw [Gamma, Complex.Gamma_eq_integral (by rwa [Complex.ofReal_re] : 0 < Complex.re s)]

Result:
s : ℝ
hs : 0 < s
⊢ (↑s).GammaIntegral.re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Proof state:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ ↑(s - 1) = ↑(rexp (-x) * x ^ (s - 1))

Tactic:
push_cast

Result:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ Complex.exp (-↑x) * ↑x ^ (↑s - 1) = Complex.exp (-↑x) * ↑(x ^ (s - 1))

Proof state:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ Complex.exp (-↑x) * ↑x ^ (↑s - 1) = Complex.exp (-↑x) * ↑x ^ ↑(s - 1)

Tactic:
push_cast

Result:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ Complex.exp (-↑x) * ↑x ^ (↑s - 1) = Complex.exp (-↑x) * ↑x ^ (↑s - 1)