awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (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))]

Premises used: Iff.mpr, le_of_lt, ne_of_gt, MeasureTheory.integral_comp_rpow_Ioi, one_div_pos, abs_eq_self, one_div_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))

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

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    (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))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))

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

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw :
  (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))
rw₁ :
  (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-HPow.hPow (β := ℝ) x 1)) =
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
rw₂ rw₃ :
  (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)) =
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
⊢ (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]

Premises used: le_of_lt, ne_of_gt, Real.rpow_one, one_div_mul_cancel, Real.rpow_mul
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
simp_rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * (x ^ (1 / p - 1) * ((x ^ (1 / p)) ^ q * rexp (-x))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * (rexp (-x) * x ^ (1 / p - 1 + q / p)))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p))

Tactic:
simp_rw [smul_eq_mul, mul_assoc]

Premises used: mul_assoc, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * (x ^ (1 / p - 1) * ((x ^ (1 / p)) ^ q * rexp (-x))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * (rexp (-x) * x ^ (1 / p - 1 + q / p)))

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

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    1 / p * (x ^ (1 / p - 1) * ((x ^ (1 / p)) ^ q * rexp (-x))) = 1 / p * (rexp (-x) * x ^ (1 / p - 1 + q / p))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * (x ^ (1 / p - 1) * ((x ^ (1 / p)) ^ q * rexp (-x))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * (rexp (-x) * x ^ (1 / p - 1 + q / p)))

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

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : x ^ (1 / p - 1) * (x ^ (1 / p * q) * rexp (-x)) / p = 1 / p * (rexp (-x) * (x ^ (1 / p - 1) * x ^ (q / p)))
⊢ 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]

Premises used: le_of_lt, div_mul_eq_mul_div, Real.rpow_add, Real.rpow_mul, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p)) =
    1 / p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-x) * x ^ ((q + 1) / p - 1)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      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)]

Premises used: neg_lt_iff_pos_add, Real.Gamma_eq_integral, Iff.mp, div_pos
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ 1 / p - 1 + q / p = (q + 1) / p - 1

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ ((q + 1) / p - 1)) =
    1 / p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-x) * x ^ ((q + 1) / p - 1)
simp_rw₁ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ ((q + 1) / p - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      1 / p * (rexp (-a) * a ^ ((q + 1) / p - 1)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p)) =
    1 / p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-x) * x ^ ((q + 1) / p - 1)

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

Premises used: MeasureTheory.integral_const_mul, mul_assoc
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
_ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
_₁ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p))
_₂ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p)) =
    1 / p * Gamma ((q + 1) / p)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      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 ring, ← integral_const_mul,
        ← mul_assoc]

Premises used: Set.Ioi, HSub.hSub, HDiv.hDiv, HAdd.hAdd, Real.Gamma, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-b * x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)))

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

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    x ^ q * rexp (-b * x ^ p) = b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-b * x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)))

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

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hx₁ : 0 < b
rw : p ≠ 0
hx₂ hx₃ : 0 ≤ b
rw₁ rw₂ : 0 ≤ b ^ p⁻¹
⊢ x ^ q * rexp (-b * x ^ p) = b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))

Tactic:
rw [mul_rpow _ (le_of_lt hx), mul_rpow _ (le_of_lt hx), ← rpow_mul, ← rpow_mul,
        inv_mul_cancel₀, rpow_one, mul_assoc, ← mul_assoc, ← rpow_add, neg_mul p⁻¹, neg_add_cancel,
        rpow_zero, one_mul, neg_mul]

Premises used: mul_assoc, le_of_lt, Real.mul_rpow, Real.rpow_zero, Real.rpow_one, Inv.inv, neg_add_cancel, Real.rpow_add, neg_mul, Real.rpow_mul, inv_mul_cancel₀, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < b

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ p ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 ≤ b

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 ≤ b ^ p⁻¹

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
rw : 0 < b ^ p⁻¹
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))) =
    (b ^ p⁻¹)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))

Tactic:
rw [integral_comp_mul_left_Ioi (fun x => b ^ (-p⁻¹ * q) * (x ^ q * exp (-x ^ p))) 0,
        mul_zero, smul_eq_mul]

Premises used: HMul.hMul, Real.exp, MulZeroClass.mul_zero, Inv.inv, HPow.hPow, smul_eq_mul, MeasureTheory.integral_comp_mul_left_Ioi, OfNat.ofNat, Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < b ^ p⁻¹

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < b ^ p⁻¹

Tactic:
all_goals positivity
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
rw : b ^ (p⁻¹ * -1 + -p⁻¹ * q) * (1 / p * Gamma ((q + 1) / p)) = b ^ (-(q + 1) / p) * (1 / p * Gamma ((q + 1) / p))
hx : 0 < b
hx₁ : 0 ≤ b
rw₁ : 0 < p
⊢ ((b ^ p⁻¹)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))) =
    b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p)

Tactic:
rw [integral_const_mul, integral_rpow_mul_exp_neg_rpow _ hq, mul_assoc, ← mul_assoc,
        ← rpow_neg_one, ← rpow_mul, ← rpow_add]

Premises used: Real.rpow_neg_one, MeasureTheory.integral_const_mul, integral_rpow_mul_exp_neg_rpow, mul_assoc, Real.rpow_add, Real.rpow_mul
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
e_a : p⁻¹ * -1 + -p⁻¹ * q = -(q + 1) / p
⊢ b ^ (p⁻¹ * -1 + -p⁻¹ * q) * (1 / p * Gamma ((q + 1) / p)) = b ^ (-(q + 1) / p) * (1 / p * Gamma ((q + 1) / p))

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ p⁻¹ * -1 + -p⁻¹ * q = -(q + 1) / p

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < b

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 ≤ b

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < p

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
_ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-b * x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)))
_₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))) =
    (b ^ p⁻¹)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))
_₂ :
  ((b ^ p⁻¹)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))) =
    b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-b * x ^ p)) =
    b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p)

Tactic:
calc
    _ = ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)) := by
      refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
      rw [mul_rpow _ (le_of_lt hx), mul_rpow _ (le_of_lt hx), ← rpow_mul, ← rpow_mul,
        inv_mul_cancel₀, rpow_one, mul_assoc, ← mul_assoc, ← rpow_add, neg_mul p⁻¹, neg_add_cancel,
        rpow_zero, one_mul, neg_mul]
      all_goals positivity
    _ = (b ^ p⁻¹)⁻¹ * ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p)) := by
      rw [integral_comp_mul_left_Ioi (fun x => b ^ (-p⁻¹ * q) * (x ^ q * exp (-x ^ p))) 0,
        mul_zero, smul_eq_mul]
      all_goals positivity
    _ = b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p) := by
      rw [integral_const_mul, integral_rpow_mul_exp_neg_rpow _ hq, mul_assoc, ← mul_assoc,
        ← rpow_neg_one, ← rpow_mul, ← rpow_add]
      · congr; ring
      all_goals positivity

Premises used: Set.Ioi, HMul.hMul, HDiv.hDiv, Inv.inv, HPow.hPow, HAdd.hAdd, Real.Gamma, OfNat.ofNat, Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p : ℝ
hp : 0 < p
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HPow.hPow (β := ℝ) x 0 * rexp (-x ^ p)) =
    1 / p * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)

Tactic:
(integral_rpow_mul_exp_neg_rpow hp neg_one_lt_zero)

Premises used: integral_rpow_mul_exp_neg_rpow, neg_one_lt_zero
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p : ℝ
hp : 0 < p
h :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HPow.hPow (β := ℝ) x 0 * rexp (-x ^ p))
h₁ : Gamma (1 / p + 1) = 1 / p * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p)) =
    Gamma (1 / p + 1)

Tactic:
convert! (integral_rpow_mul_exp_neg_rpow hp neg_one_lt_zero) using 1

Premises used: integral_rpow_mul_exp_neg_rpow, neg_one_lt_zero
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p : ℝ
hp : 0 < p
h :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ 1 * rexp (-x ^ p))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HPow.hPow (β := ℝ) x 0 * rexp (-x ^ p))

Tactic:
simp_rw [rpow_zero, one_mul]

Premises used: Real.rpow_zero, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p : ℝ
hp : 0 < p
h : Gamma (1 / p + 1) = 1 / p * Gamma (1 / p)
h₁ h₂ : 1 / p * Gamma (1 / p) = 1 / p * Gamma (1 / p)
⊢ Gamma (1 / p + 1) = 1 / p * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)

Tactic:
rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp))]

Premises used: ne_of_gt, Real.Gamma_add_one, zero_add, one_div_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HPow.hPow (β := ℝ) x 0 * rexp (-b * x ^ p)) =
    b ^ (-HAdd.hAdd (α := ℝ) 0 1 / p) * (1 / p) * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)

Tactic:
(integral_rpow_mul_exp_neg_mul_rpow hp neg_one_lt_zero hb)

Premises used: integral_rpow_mul_exp_neg_mul_rpow, neg_one_lt_zero
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p b : ℝ
hp : 0 < p
hb : 0 < b
h :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-b * x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HPow.hPow (β := ℝ) x 0 * rexp (-b * x ^ p))
h₁ : b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-HAdd.hAdd (α := ℝ) 0 1 / p) * (1 / p) * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-b * x ^ p)) =
    b ^ (-1 / p) * Gamma (1 / p + 1)

Tactic:
convert! (integral_rpow_mul_exp_neg_mul_rpow hp neg_one_lt_zero hb) using 1

Premises used: integral_rpow_mul_exp_neg_mul_rpow, neg_one_lt_zero
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p b : ℝ
hp : 0 < p
hb : 0 < b
h :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-b * x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 * rexp (-b * x ^ p))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-b * x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HPow.hPow (β := ℝ) x 0 * rexp (-b * x ^ p))

Tactic:
simp_rw [rpow_zero, one_mul]

Premises used: Real.rpow_zero, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p b : ℝ
hp : 0 < p
hb : 0 < b
h : b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-1 / p) * (1 / p) * Gamma (1 / p)
h₁ : b ^ (-1 / p) * (1 / p * Gamma (1 / p)) = b ^ (-1 / p) * (1 / p) * Gamma (1 / p)
h₂ h₃ : b ^ (-1 / p) * (1 / p * Gamma (1 / p)) = b ^ (-1 / p) * (1 / p * Gamma (1 / p))
⊢ b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-HAdd.hAdd (α := ℝ) 0 1 / p) * (1 / p) * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)

Tactic:
rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp)), mul_assoc]

Premises used: mul_assoc, ne_of_gt, Real.Gamma_add_one, zero_add, one_div_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (p_1 : ℝ × ℝ) ↦
      p_1.1 •
        (‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_1‖ ^ q * rexp (-‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_1‖ ^ p)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ ‖x‖ ^ q * rexp (-‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))

Tactic:
rw [← Complex.integral_comp_polarCoord_symm, polarCoord_target]

Premises used: Complex.integral_comp_polarCoord_symm, polarCoord_target