-- Mathlib/MeasureTheory/Integral/Gamma.lean
theorem integral_rpow_mul_exp_neg_rpow {p q : ℝ} (hp : 0 < p) (hq : - 1 < q) :
    ∫ x in Ioi (0 : ℝ), x ^ q * exp (- x ^ p) = (1 / p) * Gamma ((q + 1) / p)

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, x ^ q * rexp (-x ^ p) = 1 / p * Gamma ((q + 1) / p)

Tactic:
calc
  _ = ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * exp (-x)) := by
    rw [← integral_comp_rpow_Ioi _ (one_div_ne_zero (ne_of_gt hp)),
      abs_eq_self.mpr (le_of_lt (one_div_pos.mpr hp))]
    refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
    rw [← rpow_mul (le_of_lt hx) _ p, one_div_mul_cancel (ne_of_gt hp), rpow_one]
  _ = ∫ (x : ℝ) in Ioi 0, 1 / p * exp (-x) * x ^ (1 / p - 1 + q / p) := by
    simp_rw [smul_eq_mul, mul_assoc]
    refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
    rw [← rpow_mul (le_of_lt hx), div_mul_eq_mul_div, one_mul, rpow_add hx]
    ring_nf
  _ = (1 / p) * Gamma ((q + 1) / p) := by
    rw [Gamma_eq_integral (div_pos (neg_lt_iff_pos_add.mp hq) hp)]
    simp_rw [show 1 / p - 1 + q / p = (q + 1) / p - 1 by field_simp; ring, ← integral_mul_left,
      ← mul_assoc]

Result:
no goals

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ 1 - p + q = q + 1 - p

Tactic:
ring

Result:
no goals

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, 1 / p * (x ^ (1 / p - 1) * ((x ^ (1 / p)) ^ q * rexp (-x))) =
    ∫ (x : ℝ) in Ioi 0, 1 / p * (rexp (-x) * x ^ (1 / p - 1 + q / p))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)

Result:
p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 1 / p * (x✝ ^ (1 / p - 1) * ((x✝ ^ (1 / p)) ^ q * rexp (-x✝))) = 1 / p * (rexp (-x✝) * x✝ ^ (1 / p - 1 + q / p))

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)) =
    ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)

Result:
p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ (1 / p * x✝ ^ (1 / p - 1)) • ((x✝ ^ (1 / p)) ^ q * rexp (-(x✝ ^ (1 / p)) ^ p)) =
    (1 / p * x✝ ^ (1 / p - 1)) • ((x✝ ^ (1 / p)) ^ q * rexp (-x✝))

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ (1 / p * x✝ ^ (1 / p - 1)) • ((x✝ ^ (1 / p)) ^ q * rexp (-(x✝ ^ (1 / p)) ^ p)) =
    (1 / p * x✝ ^ (1 / p - 1)) • ((x✝ ^ (1 / p)) ^ q * rexp (-x✝))

Tactic:
rw [← rpow_mul (le_of_lt hx) _ p, one_div_mul_cancel (ne_of_gt hp), rpow_one]

Result:
no goals

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)) =
    ∫ (x : ℝ) in Ioi 0, 1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p)

Tactic:
simp_rw [smul_eq_mul, mul_assoc]

Result:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, 1 / p * (x ^ (1 / p - 1) * ((x ^ (1 / p)) ^ q * rexp (-x))) =
    ∫ (x : ℝ) in Ioi 0, 1 / p * (rexp (-x) * x ^ (1 / p - 1 + q / p))

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, 1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p) = 1 / p * Gamma ((q + 1) / p)

Tactic:
rw [Gamma_eq_integral (div_pos (neg_lt_iff_pos_add.mp hq) hp)]

Result:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, 1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p) =
    1 / p * ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ ((q + 1) / p - 1)

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 1 / p * (x✝ ^ (1 / p - 1) * ((x✝ ^ (1 / p)) ^ q * rexp (-x✝))) = 1 / p * (rexp (-x✝) * x✝ ^ (1 / p - 1 + q / p))

Tactic:
rw [← rpow_mul (le_of_lt hx), div_mul_eq_mul_div, one_mul, rpow_add hx]

Result:
p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ x✝ ^ (1 / p - 1) * (x✝ ^ (1 / p * q) * rexp (-x✝)) / p = 1 / p * (rexp (-x✝) * (x✝ ^ (1 / p - 1) * x✝ ^ (q / p)))

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ x✝ ^ (1 / p - 1) * (x✝ ^ (1 / p * q) * rexp (-x✝)) / p = 1 / p * (rexp (-x✝) * (x✝ ^ (1 / p - 1) * x✝ ^ (q / p)))

Tactic:
ring_nf

Result:
no goals

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, 1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p) =
    1 / p * ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ ((q + 1) / p - 1)

Tactic:
simp_rw [show 1 / p - 1 + q / p = (q + 1) / p - 1 by field_simp; ring, ← integral_mul_left,
  ← mul_assoc]

Result:
no goals

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, x ^ q * rexp (-x ^ p) =
    ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))

Tactic:
rw [← integral_comp_rpow_Ioi _ (one_div_ne_zero (ne_of_gt hp)),
  abs_eq_self.mpr (le_of_lt (one_div_pos.mpr hp))]

Result:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)) =
    ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))

Proof state:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ 1 / p - 1 + q / p = (q + 1) / p - 1

Tactic:
field_simp

Result:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ 1 - p + q = q + 1 - p